(*  Title:      src/Tools/isac/BridgeJEdit/Calculation.thy

    Author:     Walther Neuper, JKU Linz

Outer syntax for Isabelle/Isac's Calculation interactive via Isabelle/PIDE.

Second trial following Makarius' definition of "problem" already existing in this repository.

*)

theory Calculation

  imports

  (**)"$ISABELLE_ISAC/Knowledge/Build_Thydata"   (*remove after devel.of BridgeJEdit*)

  (**)"$ISABELLE_ISAC/MathEngine/MathEngine"

  (** )"SPARK_FDL"                             ( * remove after devel.of BridgeJEdit*)

  keywords "Example" :: thy_decl

begin

ML_file "parseC.sml"

ML_file "preliminary.sml"

section \<open>new code for Outer_Syntax Example  ...\<close>

text \<open> UPDATE:

1.  The code re-uses Makarius' \<open>Outer_Syntax.command..problem ..\<close> to a maximal extent.

2. GOON

\<close>

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

structure Data = Theory_Data

(

  type T = Rule_Set.T option;

  val empty = NONE;

  val extend = I;

  fun merge _ = NONE;

);

val set_data = Data.put o SOME;

val the_data = the o Data.get;

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

local

(*this assigns code to the keyword ---vvvvvvvvv, without error message here but

                                                 with error message in Demo_Example ?!? *)

val _ =

  Outer_Syntax.command \<^command_keyword>\<open>Example\<close>

    "prepare ISAC problem type and register it to Knowledge Store"

    (Parse.name -- Parse.!!! (\<^keyword>\<open>:\<close> |-- Parse.name --

      Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source -- Problem.parse_authors --

        Problem.parse_methods -- Problem.parse_cas -- Problem.parse_model_input)) >>

      (fn (name, (id, ((((source, maa), mets), cas), model_input))) =>

        Toplevel.theory (fn thy =>

          let

            val pblID = References_Def.explode_id id;

            val metIDs = map References_Def.explode_id mets;

            val set_data =

              ML_Context.expression (Input.pos_of source)

                (Problem.ml "Theory.setup (Problem.set_data (" 

                  @ ML_Lex.read_source source @ Problem.ml "))")

              |> Context.theory_map;

            val input = the_data (set_data thy);

            val arg = Problem.prep_input thy name maa Problem.id_empty (pblID, model_input, input, cas, metIDs);

          in KEStore_Elems.add_pbts [arg] thy end)))

in end;

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> 

end