1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Mon Jun 21 16:18:27 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Mon Jun 21 20:06:12 2021 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  
     1.5  theory Know_Store
     1.6    imports Complex_Main
     1.7 -  keywords "rule_set_knowledge" :: thy_decl
     1.8 +  keywords "rule_set_knowledge" "calculation" :: thy_decl
     1.9  begin
    1.10  
    1.11  setup \<open>
    1.12 @@ -193,6 +193,25 @@
    1.13        thy |> Context.theory_map
    1.14          (ML_Context.expression (Position.thread_data ()) (ml_rules thy args)))));
    1.15  
    1.16 +val calc_name =
    1.17 +  Parse.name -- (\<^keyword>\<open>(\<close> |-- Parse.const --| \<^keyword>\<open>)\<close>) ||
    1.18 +  Scan.ahead Parse.name -- Parse.const;
    1.19 +
    1.20 +val _ =
    1.21 +  Outer_Syntax.command \<^command_keyword>\<open>calculation\<close>
    1.22 +    "prepare ISAC calculation and register it to Knowledge Store"
    1.23 +    (calc_name -- (\<^keyword>\<open>=\<close> |-- Parse.!!! Parse.ML_source) >> (fn ((calcID, const), source) =>
    1.24 +      Toplevel.theory (fn thy =>
    1.25 +        let
    1.26 +          val ctxt = Proof_Context.init_global thy;
    1.27 +          val Const (c, _) = Proof_Context.read_const {proper = true, strict = true} ctxt const;
    1.28 +          val eval_ml =
    1.29 +            ML_Context.expression (Input.pos_of source)
    1.30 +              (ml "Theory.setup (Eval_Def.set_data (" @ ML_Lex.read_source source @ ml "))")
    1.31 +            |> Context.theory_map;
    1.32 +          val eval = Eval_Def.the_data (eval_ml thy);
    1.33 +        in KEStore_Elems.add_calcs [(calcID, (c, eval))] thy end)))
    1.34 +
    1.35  in end;
    1.36  \<close>
    1.37