1.1 --- a/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy	Fri Feb 24 16:14:28 2023 +0100
     1.2 +++ b/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy	Mon Feb 27 09:45:29 2023 +0100
     1.3 @@ -34,7 +34,7 @@
     1.4  \<close> ML \<open>
     1.5  \<close> ML \<open> (** preliminary handling of References **)
     1.6  \<close> ML \<open> (* assumption:  we read the Specfication as a whole *)
     1.7 -(*/-------------------- state of src/../preliminary at that time  -----------------------------\*)
     1.8 +(*/-------------------- state of src/../preliminary.sml at that time  -------------------------\*)
     1.9  fun re_eval_all ((*dummyarg*)) = ("re_eval_all if new_thy"; ((*dummyarg*)))
    1.10  fun re_eval_pbl ((*dummyarg*)) = ("re_eval_pbl"; ((*dummyarg*)))
    1.11  fun re_eval_met ((*dummyarg*)) = ("re_eval_met"; ((*dummyarg*)))
    1.12 @@ -61,7 +61,7 @@
    1.13  \<close> ML \<open>
    1.14  \<close> ML \<open>
    1.15  \<close> ML \<open>
    1.16 -(*\-------------------- state of src/../preliminary at that time  -----------------------------/*)
    1.17 +(*\-------------------- state of src/../preliminary.sml at that time  -------------------------/*)
    1.18  \<close> ML \<open> (*\<longrightarrow> test/../calculation.sml*)
    1.19  "----------- build Outer_Syntax Example_TEST ---------------------------------------------------";
    1.20  "----------- build Outer_Syntax Example_TEST ---------------------------------------------------";
    1.21 @@ -94,18 +94,12 @@
    1.22                  | _ => the_data thy
    1.23  \<close> ML \<open>
    1.24                    (*let*)
    1.25 -                    val ctree = the_data thy
    1.26                      val {origin = (_, o_ref, _), spec = spec_ref, ctxt, ...} =
    1.27 -                      Ctree.get_obj I ctree [(*Pos will become variable*)] |> Ctree.rep_specify_data
    1.28 +                      Ctree.get_obj I state [(*Pos will become variable*)] |> Ctree.rep_specify_data
    1.29                      val thy_id' = References.for_parse thy_id (#1 spec_ref) (#1 o_ref)
    1.30 -                    val (model, where_) = Model_Pattern.parse_pos ctxt model_input (*+check syntax*)
    1.31 +                    val (model, where_) = Model_Pattern.parse_pos_TEST ctxt model_input (*+check syntax*)
    1.32  \<close> ML \<open>
    1.33 -\<close> ML \<open>
    1.34 -(*Specify.check_input \<longrightarrow> specify.sml*)
    1.35 -fun check_input _ = 123
    1.36 -\<close> ML \<open>
    1.37 -\<close> ML \<open>
    1.38 -\<close> ML \<open>
    1.39 +(model, where_) (*GOON*)
    1.40  \<close> ML \<open>
    1.41  (**)
    1.42                      val _ = re_eval References.empty References.empty;
    1.43 @@ -115,6 +109,8 @@
    1.44                        (example_id, (model_input, (thy_id, probl_id, meth_id))) (the_data thy)
    1.45              (*end*)
    1.46  \<close> ML \<open>
    1.47 +(*POSTPONED Specify.check_input \<longrightarrow> specify.sml*)
    1.48 +fun check_input _ = 123
    1.49  \<close> ML \<open>
    1.50  \<close> ML \<open>
    1.51  \<close> ML \<open>
    1.52 @@ -142,15 +138,16 @@
    1.53                  | _ =>
    1.54                    let
    1.55                      val {origin = (_, o_ref, _), spec = spec_ref, ctxt, ...} =
    1.56 -                      Ctree.get_obj I (the_data thy) [] |> Ctree.rep_specify_data
    1.57 +                      Ctree.get_obj I state [] |> Ctree.rep_specify_data
    1.58                      val thy_id' = References.for_parse thy_id (#1 spec_ref) (#1 o_ref)
    1.59 -                    val (model, where_) = Model_Pattern.parse_pos ctxt model_input
    1.60 +                    val (model, where_) = Model_Pattern.parse_pos_TEST ctxt model_input
    1.61  (**)
    1.62                      val _ = re_eval References.empty References.empty
    1.63  (**)
    1.64 -              in Preliminary.update_state_TEST thy
    1.65 +                  in
    1.66 +                    Preliminary.update_state_TEST thy
    1.67                        (example_id, (model_input, (thy_id, probl_id, meth_id))) (the_data thy)
    1.68 -               end
    1.69 +                  end
    1.70            in set_data state thy end)));
    1.71  \<close> ML \<open>
    1.72  \<close> ML \<open> (*Example_TEST below*)
    1.73 @@ -180,7 +177,13 @@
    1.74  text \<open>
    1.75    Check complete \<open>Model\<close>, infer empty \<open>References\<close> from data hidden in "Diff_App-No.123a"
    1.76  \<close>
    1.77 -Example_TEST "Diff_App-No.123a" (*complete Model, empty References*)
    1.78 +(*
    1.79 +Example: no syntax check of terms, OK.
    1.80 +Example_TEST: proper syntax check of terms with Model_Pattern.parse_pos,
    1.81 +  but with parse_pos_TEST ERROR Malformed YXML: unbalanced element "input"
    1.82 +*)
    1.83 +(**)Example
    1.84 +(** )Example_TEST( **) "Diff_App-No.123a" (*complete Model, empty References*)
    1.85    Specification:
    1.86      Model:
    1.87        Given: \<open>Constants [r = 7]\<close>