1.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Mon Sep 25 08:39:43 2023 +0200
1.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Tue Sep 26 15:57:12 2023 +0200
1.3 @@ -40,18 +40,23 @@
1.4 LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)) ist_ctxt ptp;
1.5 "~~~~~ fun begin_end_prog , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (ist, ctxt), (pt, pos as (p, _)))
1.6 = ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, ptp);
1.7 - val {model, ...} = MethodC.from_store ctxt mI;
1.8 - val (itms, oris, probl) = case get_obj I pt p of
1.9 - PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
1.10 - | _ => error "begin_end_prog Apply_Method': uncovered case get_obj"
1.11 - val itms = if itms <> [] then itms else I_Model.complete oris probl [] model
1.12 + val (itms, oris, probl, o_spec, spec) = case get_obj I pt p of
1.13 + PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ...}
1.14 + => (itms, oris, probl, o_spec, spec)
1.15 + | _ => raise ERROR ""
1.16 + val (_, pI', _) = References.select_input o_spec spec
1.17 + val {model = pbl_patt, ...} = Problem.from_store ctxt pI';
1.18 + val {model = met_patt, ...} = MethodC.from_store ctxt mI;
1.19 + val (_, itms) = I_Model.s_make_complete oris
1.20 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_patt, met_patt)
1.21 +
1.22 val thy' = get_obj g_domID pt p;
1.23 val thy = Know_Store.get_via_last_thy thy';
1.24
1.25 (*THIS HERE---vvvvvvvvvvvvvvvvvvvvvvvvvvvvvv---MUST BE FROM A PREVIOUS TEST: EXPECT ["Test", "squ-equ-test-subpbl1"]*)
1.26 (*if*) mI = ["Biegelinien", "ausBelastung"] (*else*);
1.27 val (is, env, ctxt, prog) = case
1.28 - LItool.init_pstate ctxt (I_Model.OLD_to_TEST itms) mI of
1.29 + LItool.init_pstate ctxt itms mI of
1.30 (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
1.31 | _ => error "begin_end_prog Apply_Method': uncovered case init_pstate"
1.32