1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Wed Aug 03 18:06:02 2022 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Wed Aug 03 18:17:27 2022 +0200
1.3 @@ -87,7 +87,7 @@
1.4 val insert_fillpats: (Thy_Write.theID * Error_Pattern_Def.fill_in list) list -> theory -> theory
1.5 val get_ref_thy: unit -> theory
1.6 val set_ref_thy: theory -> unit
1.7 -end;
1.8 +end;
1.9
1.10 structure KEStore_Elems(**): KESTORE_ELEMS(**) =
1.11 struct
1.12 @@ -247,8 +247,9 @@
1.13
1.14 section \<open>Re-use existing access functions for knowledge elements\<close>
1.15 text \<open>
1.16 - The independence of problems' and methods' structure enforces the accesse
1.17 - functions to use "Isac_Knowledge", the final theory which comprises all knowledge defined.
1.18 + The independence of problems' and methods' structure from theory dependency structure
1.19 + enforces the access functions to use "Isac_Knowledge",
1.20 + the final theory which comprises all knowledge defined.
1.21 \<close>
1.22 ML \<open>
1.23 val get_ref_thy = KEStore_Elems.get_ref_thy;
2.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Wed Aug 03 18:06:02 2022 +0200
2.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Wed Aug 03 18:17:27 2022 +0200
2.3 @@ -11,7 +11,7 @@
2.4 (**)"$ISABELLE_ISAC/MathEngine/MathEngine"
2.5 (** )"SPARK_FDL" ( * remove after devel.of BridgeJEdit*)
2.6 keywords "Example" :: thy_decl
2.7 -and "Problem" "Specification" "Model" "References" "Solution"
2.8 +and "Specification" "Model" "References" "Solution"
2.9
2.10 begin
2.11
2.12 @@ -198,15 +198,14 @@
2.13 \<close> ML \<open>
2.14 \<close> ML \<open>
2.15 (*/----------------------------------------------------------------------------\*)
2.16 - Parse.name -- Parse.!!! ( \<^keyword>\<open>Problem\<close> |-- Parse.name --
2.17 - Parse.!!! ( \<^keyword>\<open>Specification\<close> -- \<^keyword>\<open>:\<close> --
2.18 + Parse.name -- Parse.!!! ( \<^keyword>\<open>Specification\<close> -- \<^keyword>\<open>:\<close> --
2.19 \<^keyword>\<open>Model\<close> -- \<^keyword>\<open>:\<close> |-- Problem.parse_model_input --
2.20 - Parse.!!! ( \<^keyword>\<open>References\<close> -- \<^keyword>\<open>:\<close> |-- parse_references_input)))
2.21 -: (string * (string * (Problem.model_input * references_input))) parser
2.22 + Parse.!!! ( \<^keyword>\<open>References\<close> -- \<^keyword>\<open>:\<close> |-- parse_references_input))
2.23 +(*: (string * (Problem.model_input * references_input)) parser*)
2.24 (*\----------------------------------------------------------------------------/*)
2.25 : Token.T list ->
2.26 (*/----------------------------------------------------------------------------\*)
2.27 - (string * (string * (Problem.model_input * references_input)))
2.28 + (string * (Problem.model_input * references_input))
2.29 (*\----------------------------------------------------------------------------/*)
2.30 * Token.T list
2.31 (*/----------------------------------------------------------------------------\* )
3.1 --- a/test/Tools/isac/BridgeJEdit/vscode-example.sml Wed Aug 03 18:06:02 2022 +0200
3.2 +++ b/test/Tools/isac/BridgeJEdit/vscode-example.sml Wed Aug 03 18:17:27 2022 +0200
3.3 @@ -23,7 +23,7 @@
3.4 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]",
3.5 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]",
3.6 "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]",
3.7 -(*MethodC model:*)
3.8 +(*MethodC model:*)
3.9 "FunctionVariable a", "FunctionVariable b", "FunctionVariable \<alpha>",
3.10 "Domain {0 <..< r}",
3.11 "Domain {0 <..< r}",