1.1 --- a/TODO.md	Thu Jul 28 11:30:53 2022 +0200
     1.2 +++ b/TODO.md	Thu Jul 28 11:43:27 2022 +0200
     1.3 @@ -94,8 +94,8 @@
     1.4  * WN: ?How represent items, which have not yet been input?
     1.5     Note: For the purpose of user-guidance the format of requested input should be indicated!
     1.6      - proposal for how to indicate requested input: in VSCode_Example.thy subsubsection \<open>Empty Specification>
     1.7 -    - this proposal presumable involves hacking of parsers -- is there a better way?
     1.8 -    - implementation and tests have solution for (a) above as a prerequisite.
     1.9 +    - the trial with <fun is_empty> in Calculation.thy makes the question more precise: 
    1.10 +      better hack parsers or better work on ML_Syntax?
    1.11  
    1.12  * WN: as soon as parsing in Outer_Syntax.command..‹Example› works, implement in Calculation
    1.13    - init_ctree, update_status, check_input

     2.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy	Thu Jul 28 11:30:53 2022 +0200
     2.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy	Thu Jul 28 11:43:27 2022 +0200
     2.3 @@ -162,25 +162,42 @@
     2.4  \<close> ML \<open>
     2.5  \<close> ML \<open>
     2.6  \<close> ML \<open>
     2.7 +fun is_empty str = 
     2.8 +  let
     2.9 +    val strl = Symbol.explode str |> rev
    2.10 +  in
    2.11 +    take (2, strl) = ["_", " "] orelse take (3, strl) = ["]", "_", "["]
    2.12 +  end
    2.13 +\<close> ML \<open>
    2.14 +val m2 = "0 < r";                val m2' = Symbol.explode m2 |> rev;
    2.15 +val m3 = "Maximum _";            val m3' = Symbol.explode m3 |> rev;
    2.16 +val m4 = "AdditionalValues [_]"; val m4' = Symbol.explode m4 |> rev;
    2.17 +\<close> ML \<open>
    2.18 +\<close> ML \<open>
    2.19  val _ =
    2.20    Outer_Syntax.command \<^command_keyword>\<open>Example\<close>
    2.21      "prepare ISAC problem type and register it to Knowledge Store"
    2.22      (Parse.name -- Parse.!!! ( \<^keyword>\<open>Specification\<close> -- \<^keyword>\<open>:\<close> --
    2.23           \<^keyword>\<open>Model\<close> -- \<^keyword>\<open>:\<close>  |-- Problem.parse_model_input --
    2.24           Parse.!!! ( \<^keyword>\<open>References\<close> -- \<^keyword>\<open>:\<close> |-- (*parse_references_input*) Problem.parse_cas)) >>
    2.25 -      (fn (example_id, (model_input, cas_input(*references_input*))) =>
    2.26 +      (fn (example_id, (model_input, _(*references_input*))) =>
    2.27          Toplevel.theory (fn thy =>
    2.28            let
    2.29 -val _ = writeln ("#Example model_input: " ^ @{make_string} cas_input)
    2.30 -(*
    2.31 +(** )
    2.32  val _ = writeln ("#Example model_input: " ^ @{make_string} model_input)
    2.33 -(*                #Example model_input: 
    2.34 +(*                #Example model_input:
    2.35      [("#Given", ["<markup>"]), ("#Where", ["<markup>"]), ("#Find", ["<markup>", "<markup>"]), ("#Relate", ["<markup>", "<markup>"])]*)
    2.36  val [("#Given", [m1]), ("#Where", [m2]), ("#Find", [m3, m4]), ("#Relate", [m5, m6])] = 
    2.37    model_input : Problem.model_input
    2.38 -val _ = writeln ("#Example m.: " ^ m1 ^ m2 ^ m3 ^ m4 ^ m4 ^ m5 ^ m6)
    2.39 -(*                #Example m.: Constants [r = 7]0 < rMaximum AAdditionalValues [u, v]AdditionalValues [u, v]Extremum A = 2 * u * v - u \<up> 2SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]*)
    2.40 -*)
    2.41 +val _ = writeln ("#Example m.: " ^ m1 ^ " " ^ m2 ^ " " ^ m3 ^ " " ^ m4 ^ " " ^ m4 ^ " " ^ m5 ^ " " ^ m6)
    2.42 +
    2.43 +val m2' = Symbol.explode m2;
    2.44 +val _ = writeln ("#Example Symbol.explode m2: " ^ @{make_string} m2')
    2.45 +val _ = if (is_empty m2) then writeln "true" else writeln "false";
    2.46 +val _ = if (is_empty m3) then writeln "true" else writeln "false";
    2.47 +val _ = if (is_empty m4) then writeln "true" else writeln "false";
    2.48 +(*                #Example m.: Constants [r = 7] 0 < r Maximum _ AdditionalValues [_] AdditionalValues [_] Extremum _ SideCondition [_]*)
    2.49 +( **)
    2.50              val (thy_id, (probl_id, meth_id)) = (*references_input*)("Diff_App", ("univariate_calculus/Optimisation", "Optimisation/by_univariate_calculus"))
    2.51              val input = update_state (example_id, (model_input, 
    2.52                (thy_id, References_Def.explode_id probl_id, References_Def.explode_id meth_id)))