cleanup
authorwneuper <Walther.Neuper@jku.at>
Wed, 03 Aug 2022 18:17:27 +0200
changeset 60508ce09935439b3
parent 60507 b125dcf14489
child 60509 2e0b7ca391dc
cleanup
src/Tools/isac/BaseDefinitions/Know_Store.thy
src/Tools/isac/BridgeJEdit/Calculation.thy
test/Tools/isac/BridgeJEdit/vscode-example.sml
     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}",