1.1 --- a/TODO.md Tue May 31 09:16:12 2022 +0200
1.2 +++ b/TODO.md Tue May 31 09:36:02 2022 +0200
1.3 @@ -69,4 +69,4 @@
1.4 * WN: for calculation by use of Makarius' "problem" as boilerplate clarify:
1.5 - How inspect Token lists, e.g. from ML_Lex.read OR ML_Lex.read_source ?
1.6 - Why the ERROR in Demo_Example.thy at: \<open>problem pbl_bieg : "Biegelinien" = ..\<close> ?
1.7 - - TODO: remove test code written in this changeset
1.8 +
2.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Tue May 31 09:16:12 2022 +0200
2.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Tue May 31 09:36:02 2022 +0200
2.3 @@ -34,29 +34,11 @@
2.4 fun merge _ = NONE;
2.5 );
2.6
2.7 -val set_data = (writeln "=== set_data"; Data.put o SOME);
2.8 -val the_data = (writeln "=== the_data"; the o Data.get);
2.9 +val set_data = Data.put o SOME;
2.10 +val the_data = the o Data.get;
2.11
2.12 \<close> ML \<open>
2.13 \<close> ML \<open>
2.14 -set_data: Rule_Def.rule_set -> theory -> theory
2.15 -\<close> ML \<open>
2.16 -fun set_data rls thy =
2.17 - ((case rls of
2.18 - Rule_Def.Empty => writeln "=== Rule_Def.Empty"
2.19 - | Rule_Def.Repeat _ => writeln "=== Rule_Def.Repeat _"
2.20 - | Rule_Def.Sequence _ => writeln "=== Rule_Def.RepSequenceeat _"
2.21 - | Rule_Def.Rrls _ => writeln "=== Rule_Def.Rrls _"
2.22 - );
2.23 - (Data.put o SOME) rls thy)
2.24 -\<close> ML \<open>
2.25 -the_data: theory -> Rule_Def.rule_set
2.26 -\<close> ML \<open>
2.27 -(*+*)fun the_data thy =
2.28 - case Data.get thy of
2.29 - SOME rls => (writeln ("=== the_data thy \<Rightarrow> " ^ Rule_Set.to_string rls); rls)
2.30 - | NONE => raise ERROR "=== the_data thy \<Rightarrow> NONE"
2.31 -\<close> ML \<open>
2.32 \<close> ML \<open>
2.33
2.34 \<close> ML \<open>
2.35 @@ -80,50 +62,12 @@
2.36 (Problem.ml "Theory.setup (Problem.set_data ("
2.37 @ ML_Lex.read_source source @ Problem.ml "))")
2.38 |> Context.theory_map;
2.39 -val _ = writeln "=== Outer_Syntax.command 4"
2.40 val input = the_data (set_data thy);
2.41 -val _ = writeln "=== Outer_Syntax.command 5"
2.42 val arg = Problem.prep_input thy name maa Problem.id_empty (pblID, model_input, input, cas, metIDs);
2.43 - in KEStore_Elems.add_pbts [arg] thy end
2.44 - )
2.45 - )
2.46 - )
2.47 + in KEStore_Elems.add_pbts [arg] thy end)))
2.48 +
2.49 in end;
2.50 \<close> ML \<open>
2.51 -ML_Context.expression:
2.52 - Position.T -> ML_Lex.token Antiquote.antiquote list -> Context.generic
2.53 - -> Context.generic
2.54 -\<close> ML \<open>
2.55 -Problem.ml "Theory.setup (Problem.set_data (" (* =
2.56 - [Text (Token (({}, {}), (Long_Ident, "Theory.setup"))),
2.57 - Text (Token (({}, {}), (Space, " "))),
2.58 - Text (Token (({}, {}), (Keyword, "("))),
2.59 - Text (Token (({}, {}), (Long_Ident, "Problem.set_data"))),
2.60 - Text (Token (({}, {}), (Space, " "))),
2.61 - Text (Token (({}, {}), (Keyword, "("))),
2.62 - Text (Token (({}, {}), (Space, " ")))]:
2.63 - ML_Lex.token Antiquote.antiquote list*)
2.64 -\<close> text \<open>
2.65 -@
2.66 -ML_Lex.read_source source:
2.67 - ML_Lex.token Antiquote.antiquote list
2.68 -@
2.69 -\<close> ML \<open>
2.70 -Problem.ml "))" (* =
2.71 - [Text (Token (({}, {}), (Keyword, ")"))),
2.72 - Text (Token (({}, {}), (Keyword, ")"))),
2.73 - Text (Token (({}, {}), (Space, " ")))]:
2.74 - ML_Lex.token Antiquote.antiquote list*)
2.75 -\<close> ML \<open>
2.76 -Context.theory_map: (Context.generic -> Context.generic) -> theory -> theory
2.77 -\<close> ML \<open>
2.78 -\<close> ML \<open>
2.79 -\<close> ML \<open>
2.80 -\<close> ML \<open>
2.81 -\<close> ML \<open>
2.82 -\<close> ML \<open>
2.83 -\<close> ML \<open>
2.84 -\<close> ML \<open>
2.85 \<close> ML \<open>
2.86 \<close> ML \<open>
2.87 \<close>
3.1 --- a/src/Tools/isac/BridgeJEdit/Demo_Example.thy Tue May 31 09:16:12 2022 +0200
3.2 +++ b/src/Tools/isac/BridgeJEdit/Demo_Example.thy Tue May 31 09:36:02 2022 +0200
3.3 @@ -105,7 +105,8 @@
3.4 \<close> ML \<open>
3.5 Rule_Set.append_rules "empty" Rule_Set.empty []
3.6 \<close>
3.7 -text \<open> (*Output from: Example pbl_bieg : "Biegelinien" = .. HERE*)
3.8 +text \<open> for testcode cf. 1c8263e775d4
3.9 + (*Output from: Example pbl_bieg : "Biegelinien" = .. HERE*)
3.10 val it = Repeat {calc = [], erls = Empty, errpatts = [], id = "empty", preconds = [],
3.11 rew_ord = ("dummy_ord", fn), rules = [], scr = Empty_Prog, srls = Empty}: Rule_Def.rule_set
3.12
4.1 --- a/src/Tools/isac/Calculation.thy Tue May 31 09:16:12 2022 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,18 +0,0 @@
4.4 -(* Title: src/Tools/isac/BridgeJEdit/Calculation.thy
4.5 - Author: Walther Neuper, JKU Linz
4.6 - (c) due to copyright terms
4.7 -
4.8 -Outer syntax for Isabelle/Isac's Calculation.
4.9 -Second trial following Makarius' definition of "problem", "method", etc
4.10 -already existing in this repository.
4.11 -*)
4.12 -
4.13 -theory Calculation
4.14 -imports
4.15 -(** )"$ISABELLE_ISAC/Knowledge/Build_Thydata" ( *remove after devel.of BridgeJEdit*)
4.16 -(**)"$ISABELLE_ISAC/Knowledge/Build_Thydata" (*remove after devel.of BridgeJEdit*)
4.17 -(**)"$ISABELLE_ISAC/MathEngine/MathEngine"
4.18 -
4.19 -begin
4.20 -
4.21 -end
4.22 \ No newline at end of file
5.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Tue May 31 09:16:12 2022 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Tue May 31 09:36:02 2022 +0200
5.3 @@ -109,9 +109,6 @@
5.4 (* Where: "0 < l_l" ...wait for < and handling Arbfix*)
5.5 Find: "Biegelinie b_b"
5.6 Relate: "Randbedingungen r_b"
5.7 -ML \<open>
5.8 -Rule_Set.append_rules "empty" Rule_Set.empty []
5.9 -\<close>
5.10
5.11 problem pbl_bieg_mom : "MomentBestimmte/Biegelinien" =
5.12 \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
6.1 --- a/src/Tools/isac/MathEngBasic/problem.sml Tue May 31 09:16:12 2022 +0200
6.2 +++ b/src/Tools/isac/MathEngBasic/problem.sml Tue May 31 09:36:02 2022 +0200
6.3 @@ -139,10 +139,6 @@
6.4 val set_data = Data.put o SOME;
6.5 val the_data = the o Data.get;
6.6
6.7 -(*+*)fun the_data thy =
6.8 - case Data.get thy of
6.9 - SOME rls => (writeln ("--- the_data thy \<Rightarrow> " ^ Rule_Set.to_string rls); rls)
6.10 - | NONE => raise ERROR "--- the_data thy \<Rightarrow> NONE"
6.11
6.12 (* auxiliary parsers *)
6.13
6.14 @@ -189,9 +185,7 @@
6.15 ML_Context.expression (Input.pos_of source)
6.16 (ml "Theory.setup (Problem.set_data (" @ ML_Lex.read_source source @ ml "))")
6.17 |> Context.theory_map;
6.18 -val _ = writeln "--- Outer_Syntax.command 4"
6.19 val input = the_data (set_data thy);
6.20 -val _ = writeln "--- Outer_Syntax.command 5"
6.21 val arg = prep_input thy name maa id_empty (pblID, model_input, input, cas, metIDs);
6.22 in KEStore_Elems.add_pbts [arg] thy end)))
6.23