1.1 --- a/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy Tue May 23 07:56:29 2023 +0200
1.2 +++ b/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy Tue May 23 08:34:53 2023 +0200
1.3 @@ -77,12 +77,12 @@
1.4 (*reminder for Template.show ----------------------------------------------------------------\*)
1.5 val ((_, _, _), (_, pbl_id as ["univariate_calculus", "Optimisation"], _)) =
1.6 References.for_eval_model (thy_id, probl_id, meth_id) spec_ref o_ref
1.7 + val {model = model_patt, where_ = where_ctree, where_rls, ...} =
1.8 + Problem.from_store ctxt pbl_id;
1.9
1.10 val (_, env_eval) = Pre_Conds.sep_variants_envs_OLD model_patt probl
1.11 - (*------------------- must be completed first ---^^^^^*)
1.12 + (*------------------- must be completed first -----------------^^^^^*)
1.13
1.14 - val {model = model_patt, where_ = where_ctree, where_rls, ...} =
1.15 - Problem.from_store ctxt pbl_id;
1.16 val _ =
1.17 case I_Model.is_complete_OLD ctxt model_patt where_rls where_ctree probl of
1.18 NONE => writeln "I_Model.is_complete_OLD --> NONE"
2.1 --- a/test/Tools/isac/Interpret/li-tool.sml Tue May 23 07:56:29 2023 +0200
2.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Tue May 23 08:34:53 2023 +0200
2.3 @@ -46,7 +46,7 @@
2.4 val thy' = get_obj g_domID pt p;
2.5 val thy = ThyC.get_theory @{context} thy';
2.6 val prog_rls = LItool.get_simplifier (pt, pos)
2.7 -val (is as Pstate {env, ...}, ctxt, sc) = init_pstate prog_rls ctxt itms mI;
2.8 +val (is as Pstate {env, ...}, ctxt, sc) = init_pstate ctxt (I_Model.OLD_to_TEST itms) mI;
2.9 val ini = implicit_take @{context} sc env;
2.10 "----- fun implicit_take, args:"; val (Prog sc) = sc;
2.11 "----- fun get_first_argument, args:"; val (y, h $ body) = (thy, sc);
2.12 @@ -245,7 +245,7 @@
2.13 (*+*)val ctxt = get_ctxt pt''''' p''''';
2.14 (*+*)val prog_rls = get_simplifier (pt''''', p''''');
2.15 "~~~~~ fun init_pstate , args:"; val (prog_rls, thy, itms, metID) = (prog_rls, ThyC.get_theory @{context} thy, meth, metID);
2.16 -val (Pstate st, ctxt, Prog _) = init_pstate prog_rls ctxt itms metID;
2.17 +val (Pstate st, ctxt, Prog _) = init_pstate ctxt (I_Model.OLD_to_TEST itms) metID;
2.18 if pstate2str st =
2.19 "([\"\n(l_l, L)\", \"\n(q_q, q_0)\", \"\n(fun_var, x)\", \"\n(b_b, dy)\", \"\n(r_b, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\", \"\n(vs, [c, c_2, c_3, c_4])\", \"\n(id_der, y)\"], [], erls_IntegrierenUndK.., NONE, \n??.empty, ORundef, false, true)"
2.20 then () else error "init_pstate changed for Biegelinie";
3.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Tue May 23 07:56:29 2023 +0200
3.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Tue May 23 08:34:53 2023 +0200
3.3 @@ -121,7 +121,7 @@
3.4 val (tac as Model_Problem (*[''makeFunctionTo'', ''"equation'']*), (pt, p as ([2, 1], Pbl))) =
3.5 (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
3.6 (* ERROR for a long time -----vvvvvvvvvvvvvvvvvvvvvvvv.. (should be evaluated!) *)
3.7 - val (tac as Substitute ["x = (argument_in lhs (NTH 1 [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]))"], (pt, p as ([2, 1, 1], Frm))) =
3.8 + val (tac as Substitute ["x = 0"], (pt, p as ([2, 1, 1], Frm))) =
3.9 (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me';
3.10
3.11 if p = ([2, 1, 1], Frm) andalso (Calc.current_formula (pt, p) |> UnparseC.term @{context}) =
4.1 --- a/test/Tools/isac/Test_Isac_Short.thy Tue May 23 07:56:29 2023 +0200
4.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Tue May 23 08:34:53 2023 +0200
4.3 @@ -362,6 +362,7 @@
4.4 ML_file "Knowledge/biegelinie-4.sml"
4.5 ML \<open>
4.6 \<close> ML \<open>
4.7 +\<close> ML \<open>
4.8 \<close>
4.9 ML_file "Knowledge/algein.sml"
4.10 ML \<open>