question about Outer_Syntax.command \<^command_keyword>?Example?
authorwneuper <Walther.Neuper@jku.at>
Wed, 20 Jul 2022 11:56:45 +0200
changeset 60485c14f2538095c
parent 60484 e5fe5b40a1b4
child 60486 17690ea5da8e
question about Outer_Syntax.command \<^command_keyword>?Example?
TODO.md
src/Tools/isac/BridgeJEdit/Calculation.thy
src/Tools/isac/BridgeJEdit/VSCode_Example.thy
     1.1 --- a/TODO.md	Wed Jul 20 11:48:38 2022 +0200
     1.2 +++ b/TODO.md	Wed Jul 20 11:56:45 2022 +0200
     1.3 @@ -5,6 +5,11 @@
     1.4      Reproducible e.g. at https://hg.risc.uni-linz.ac.at/wneuper/isa/file/9c2e1efe5cde/src/Tools/isac/Knowledge/Biegelinie.thy#l108
     1.5      The respective improvement would be the model for WN continuing ..\<open>Example\<close>. 
     1.6  
     1.7 +* ?MW?: In Outer_Syntax.command \<^command_keyword>\<open>Example\<close> is there a quick fix
     1.8 +  for successfully replacing hacked Problem.parse_cas by parse_references_input?
     1.9 +    How can Scan.* be traced?
    1.10 +    (Tracing should help understanding Problem.parse_cas, Problem.parse_model_input which involve Scan.*)
    1.11 +
    1.12  * MW: check uses of Unsynchronized.ref vs. Synchronized.var;
    1.13  
    1.14  * MW: clarify/eliminate Isabelle/Scala add-ons (presently unused)
     2.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy	Wed Jul 20 11:48:38 2022 +0200
     2.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy	Wed Jul 20 11:56:45 2022 +0200
     2.3 @@ -152,7 +152,7 @@
     2.4      (Parse.name -- Parse.!!! (  \<^keyword>\<open>Problem\<close> |-- Parse.name -- 
     2.5         Parse.!!! ( \<^keyword>\<open>Specification\<close> -- \<^keyword>\<open>:\<close> --
     2.6           \<^keyword>\<open>Model\<close> -- \<^keyword>\<open>:\<close>  |-- Problem.parse_model_input --
     2.7 -         Parse.!!! ( \<^keyword>\<open>References\<close> -- \<^keyword>\<open>:\<close> |-- (*parse_references_input*)Problem.parse_cas))) >>
     2.8 +         Parse.!!! ( \<^keyword>\<open>References\<close> -- \<^keyword>\<open>:\<close> |-- (*parse_references_input*) Problem.parse_cas))) >>
     2.9        (fn (example_id, (_(*probl_id'*), (model_input, _(*references_input*)))) =>
    2.10          Toplevel.theory (fn thy =>
    2.11            let
     3.1 --- a/src/Tools/isac/BridgeJEdit/VSCode_Example.thy	Wed Jul 20 11:48:38 2022 +0200
     3.2 +++ b/src/Tools/isac/BridgeJEdit/VSCode_Example.thy	Wed Jul 20 11:56:45 2022 +0200
     3.3 @@ -207,11 +207,11 @@
     3.4          Relate: \<open>Extremum A = 2 * u * v - u \<up> 2\<close> 
     3.5            \<open>SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\<close>
     3.6        References:
     3.7 -(** )
     3.8 +(**  )
     3.9           Theory_Ref: "Diff_App"
    3.10    (*\<Odot>*) Problem_Ref: "univariate_calculus/Optimisation"
    3.11    (*\<Otimes>*) Method_Ref: "Optimisation/by_univariate_calculus"
    3.12 -( **)
    3.13 +(  **)
    3.14  ML \<open>
    3.15  val state = the_data @{theory};
    3.16  \<close> ML \<open>