1361 then let val (po,p_) = p |
1361 then let val (po,p_) = p |
1362 val po' = case p_ of Frm => po | Res => lev_on po |
1362 val po' = case p_ of Frm => po | Res => lev_on po |
1363 (*WN.12.03: noticed, that pos is also updated in assy !?! |
1363 (*WN.12.03: noticed, that pos is also updated in assy !?! |
1364 instead take p' from Assoc ?????????????????????????????*) |
1364 instead take p' from Assoc ?????????????????????????????*) |
1365 val (p'',c'',f'',pt'') = |
1365 val (p'',c'',f'',pt'') = |
1366 generate1 thy m (ScrState is, e_ctxt) (po',p_) pt; |
1366 generate1 thy m (ScrState is, ctxt) (po',p_) pt; |
1367 (*val _=tracing("### locate_gen, aft g1: p''="^(pos'2str p''));*) |
1367 (*val _=tracing("### locate_gen, aft g1: p''="^(pos'2str p''));*) |
1368 (*drop the intermediate steps !*) |
1368 (*drop the intermediate steps !*) |
1369 in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end |
1369 in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end |
1370 else Steps (ScrState is, ss)) |
1370 else Steps (ScrState is, ss)) |
1371 |
1371 |
1380 Assoc (iss as (is as (_,_,_,_,_,bb), |
1380 Assoc (iss as (is as (_,_,_,_,_,bb), |
1381 ss as ((m',f',pt',p',c')::_))) => |
1381 ss as ((m',f',pt',p',c')::_))) => |
1382 ((*tracing"4### locate_gen Assoc after Fini";*) |
1382 ((*tracing"4### locate_gen Assoc after Fini";*) |
1383 if rew_only ss |
1383 if rew_only ss |
1384 then let val(p'',c'',f'',pt'') = |
1384 then let val(p'',c'',f'',pt'') = |
1385 generate1 thy m (ScrState is, e_ctxt) p' pt; |
1385 generate1 thy m (ScrState is, ctxt) p' pt; |
1386 (*drop the intermediate steps !*) |
1386 (*drop the intermediate steps !*) |
1387 in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end |
1387 in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end |
1388 else NotLocatable) |
1388 else NotLocatable) |
1389 | _ => ((*tracing ("#### locate_gen: after Fini");*) |
1389 | _ => ((*tracing ("#### locate_gen: after Fini");*) |
1390 NotLocatable)) |
1390 NotLocatable)) |
1391 end |
1391 end |
1392 | locate_gen _ m _ (sc,_) (is, ctxt) = |
1392 | locate_gen _ m _ (sc,_) (is, _) = |
1393 error ("locate_gen: wrong arguments,\n tac= "^(tac_2str m)^ |
1393 error ("locate_gen: wrong arguments,\n tac= "^(tac_2str m)^ |
1394 ",\n scr= "^(scr2str sc)^",\n istate= "^(istate2str is)); |
1394 ",\n scr= "^(scr2str sc)^",\n istate= "^(istate2str is)); |
1395 |
1395 |
1396 |
1396 |
1397 |
1397 |
1775 Skip (v,_) => (*finished*) |
1775 Skip (v,_) => (*finished*) |
1776 (case par_pbl_det pt p of |
1776 (case par_pbl_det pt p of |
1777 (true, p', _) => |
1777 (true, p', _) => |
1778 let val (_,pblID,_) = get_obj g_spec pt p'; |
1778 let val (_,pblID,_) = get_obj g_spec pt p'; |
1779 in (Check_Postcond' (pblID, (v, [(*8.6.03 NO asms???*)])), |
1779 in (Check_Postcond' (pblID, (v, [(*8.6.03 NO asms???*)])), |
1780 (e_istate, ctxt), (v,s)) end |
1780 (e_istate, e_ctxt), (v,s)) end |
1781 | (_,p',rls') => (End_Detail' (e_term,[])(*8.6.03*), (e_istate, e_ctxt), (v,s))) |
1781 | (_,p',rls') => (End_Detail' (e_term,[])(*8.6.03*), (e_istate, e_ctxt), (v,s))) |
1782 | Napp _ => (Empty_Tac_, (e_istate, e_ctxt), (e_term, Sundef)) (*helpless*) |
1782 | Napp _ => (Empty_Tac_, (e_istate, e_ctxt), (e_term, Sundef)) (*helpless*) |
1783 | Appy (m', scrst as (_,_,_,v,_,_)) => (m', (ScrState scrst, e_ctxt), |
1783 | Appy (m', scrst as (_,_,_,v,_,_)) => (m', (ScrState scrst, e_ctxt), |
1784 (v, Sundef))) (*next stac*) |
1784 (v, Sundef))) (*next stac*) |
1785 |
1785 |