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>