1.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Thu Aug 04 15:24:58 2022 +0200
1.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Thu Aug 04 15:25:44 2022 +0200
1.3 @@ -146,7 +146,7 @@
1.4 Parse.!!! ( \<^keyword>\<open>Problem_Ref\<close> -- \<^keyword>\<open>Theory_Ref\<close> |-- Parse.name --
1.5 Parse.!!! ( \<^keyword>\<open>Method_Ref\<close> -- \<^keyword>\<open>Theory_Ref\<close> |-- Parse.name)))
1.6 \<close> ML \<open>
1.7 -parse_references_input: references_input parser (*TODO: dpes not yet work,
1.8 +parse_references_input: references_input parser (*TODO: does not yet work,
1.9 thus in Outer_Syntax.command \<^command_keyword>\<open>Example\<close> replacced by Problem.parse_cas*)
1.10 \<close> ML \<open>
1.11 op -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e;
1.12 @@ -154,6 +154,7 @@
1.13 \<close> ML \<open>
1.14 \<close> ML \<open>
1.15 \<close> ML \<open>
1.16 +(* but "<markup>" would be required as an argument *)
1.17 fun is_empty str =
1.18 let
1.19 val strl = Symbol.explode str |> rev