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 @@ \ ML \ \ ML \ (** preliminary handling of References **) \ ML \ (* 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 @@ \ ML \ \ ML \ \ ML \ -(*\-------------------- state of src/../preliminary at that time -----------------------------/*) +(*\-------------------- state of src/../preliminary.sml at that time -------------------------/*) \ ML \ (*\ test/../calculation.sml*) "----------- build Outer_Syntax Example_TEST ---------------------------------------------------"; "----------- build Outer_Syntax Example_TEST ---------------------------------------------------"; @@ -94,18 +94,12 @@ | _ => the_data thy \ ML \ (*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*) \ ML \ -\ ML \ -(*Specify.check_input \ specify.sml*) -fun check_input _ = 123 -\ ML \ -\ ML \ -\ ML \ +(model, where_) (*GOON*) \ ML \ (**) 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*) \ ML \ +(*POSTPONED Specify.check_input \ specify.sml*) +fun check_input _ = 123 \ ML \ \ ML \ \ ML \ @@ -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))); \ ML \ \ ML \ (*Example_TEST below*) @@ -180,7 +177,13 @@ text \ Check complete \Model\, infer empty \References\ from data hidden in "Diff_App-No.123a" \ -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: \Constants [r = 7]\