
diff -r dd386fd3ec5e -r f7795240462a test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy
--- a/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy	Fri Feb 24 16:14:28 2023 +0100
+++ b/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy	Mon Feb 27 09:45:29 2023 +0100
@@ -34,7 +34,7 @@
 \<close> ML \<open>
 \<close> ML \<open> (** preliminary handling of References **)
 \<close> ML \<open> (* assumption:  we read the Specfication as a whole *)
-(*/-------------------- state of src/../preliminary at that time  -----------------------------\*)
+(*/-------------------- state of src/../preliminary.sml at that time  -------------------------\*)
 fun re_eval_all ((*dummyarg*)) = ("re_eval_all if new_thy"; ((*dummyarg*)))
 fun re_eval_pbl ((*dummyarg*)) = ("re_eval_pbl"; ((*dummyarg*)))
 fun re_eval_met ((*dummyarg*)) = ("re_eval_met"; ((*dummyarg*)))
@@ -61,7 +61,7 @@
 \<close> ML \<open>
 \<close> ML \<open>
 \<close> ML \<open>
-(*\-------------------- state of src/../preliminary at that time  -----------------------------/*)
+(*\-------------------- state of src/../preliminary.sml at that time  -------------------------/*)
 \<close> ML \<open> (*\<longrightarrow> test/../calculation.sml*)
 "----------- build Outer_Syntax Example_TEST ---------------------------------------------------";
 "----------- build Outer_Syntax Example_TEST ---------------------------------------------------";
@@ -94,18 +94,12 @@
                 | _ => the_data thy
 \<close> ML \<open>
                   (*let*)
-                    val ctree = the_data thy
                     val {origin = (_, o_ref, _), spec = spec_ref, ctxt, ...} =
-                      Ctree.get_obj I ctree [(*Pos will become variable*)] |> Ctree.rep_specify_data
+                      Ctree.get_obj I state [(*Pos will become variable*)] |> Ctree.rep_specify_data
                     val thy_id' = References.for_parse thy_id (#1 spec_ref) (#1 o_ref)
-                    val (model, where_) = Model_Pattern.parse_pos ctxt model_input (*+check syntax*)
+                    val (model, where_) = Model_Pattern.parse_pos_TEST ctxt model_input (*+check syntax*)
 \<close> ML \<open>
-\<close> ML \<open>
-(*Specify.check_input \<longrightarrow> specify.sml*)
-fun check_input _ = 123
-\<close> ML \<open>
-\<close> ML \<open>
-\<close> ML \<open>
+(model, where_) (*GOON*)
 \<close> ML \<open>
 (**)
                     val _ = re_eval References.empty References.empty;
@@ -115,6 +109,8 @@
                       (example_id, (model_input, (thy_id, probl_id, meth_id))) (the_data thy)
             (*end*)
 \<close> ML \<open>
+(*POSTPONED Specify.check_input \<longrightarrow> specify.sml*)
+fun check_input _ = 123
 \<close> ML \<open>
 \<close> ML \<open>
 \<close> ML \<open>
@@ -142,15 +138,16 @@
                 | _ =>
                   let
                     val {origin = (_, o_ref, _), spec = spec_ref, ctxt, ...} =
-                      Ctree.get_obj I (the_data thy) [] |> Ctree.rep_specify_data
+                      Ctree.get_obj I state [] |> Ctree.rep_specify_data
                     val thy_id' = References.for_parse thy_id (#1 spec_ref) (#1 o_ref)
-                    val (model, where_) = Model_Pattern.parse_pos ctxt model_input
+                    val (model, where_) = Model_Pattern.parse_pos_TEST ctxt model_input
 (**)
                     val _ = re_eval References.empty References.empty
 (**)
-              in Preliminary.update_state_TEST thy
+                  in
+                    Preliminary.update_state_TEST thy
                       (example_id, (model_input, (thy_id, probl_id, meth_id))) (the_data thy)
-               end
+                  end
           in set_data state thy end)));
 \<close> ML \<open>
 \<close> ML \<open> (*Example_TEST below*)
@@ -180,7 +177,13 @@
 text \<open>
   Check complete \<open>Model\<close>, infer empty \<open>References\<close> from data hidden in "Diff_App-No.123a"
 \<close>
-Example_TEST "Diff_App-No.123a" (*complete Model, empty References*)
+(*
+Example: no syntax check of terms, OK.
+Example_TEST: proper syntax check of terms with Model_Pattern.parse_pos,
+  but with parse_pos_TEST ERROR Malformed YXML: unbalanced element "input"
+*)
+(**)Example
+(** )Example_TEST( **) "Diff_App-No.123a" (*complete Model, empty References*)
   Specification:
     Model:
       Given: \<open>Constants [r = 7]\<close>




