1.1 --- a/src/Tools/isac/MathEngBasic/method.sml	Sun Jun 20 16:26:18 2021 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/method.sml	Sun Jun 20 16:30:56 2021 +0200
     1.3 @@ -17,8 +17,8 @@
     1.4    val prep_input : theory ->  Check_Unique.id -> string list -> id ->
     1.5       id * Problem.model_input * input * thm -> T * id
     1.6  
     1.7 -  val set_input: input -> theory -> theory
     1.8 -  val the_input: theory -> input
     1.9 +  val set_data: input -> theory -> theory
    1.10 +  val the_data: theory -> input
    1.11  
    1.12    val from_store: id -> T
    1.13    val from_store': theory -> id -> T
    1.14 @@ -107,27 +107,13 @@
    1.15    fun merge _ = NONE;
    1.16  );
    1.17  
    1.18 -val set_input = Data.put o SOME;
    1.19 -val the_input = the o Data.get;
    1.20 +val set_data = Data.put o SOME;
    1.21 +val the_data = the o Data.get;
    1.22  
    1.23  local
    1.24  
    1.25 -fun parse_item keyword parse = (keyword -- Args.colon) |-- Parse.!!! parse;
    1.26 -
    1.27 -val parse_authors =
    1.28 -  Scan.optional (parse_item \<^keyword>\<open>Author\<close> (Scan.repeat1 Parse.name)) [];
    1.29 -
    1.30  val parse_program =
    1.31 -  Scan.option (parse_item \<^keyword>\<open>Program\<close> (Parse.position Parse.name));
    1.32 -
    1.33 -fun parse_terms keyword (tag: string) =
    1.34 -  Scan.optional (parse_item keyword (Scan.repeat Parse.term) >> (fn ts => [(tag, ts)])) [];
    1.35 -
    1.36 -val parse_ppc =
    1.37 -  parse_terms \<^keyword>\<open>Given\<close> "#Given" @@@
    1.38 -  parse_terms \<^keyword>\<open>Where\<close> "#Where" @@@
    1.39 -  parse_terms \<^keyword>\<open>Find\<close> "#Find" @@@
    1.40 -  parse_terms \<^keyword>\<open>Relate\<close> "#Relate";
    1.41 +  Scan.option (Problem.parse_item \<^keyword>\<open>Program\<close> (Parse.position Parse.name));
    1.42  
    1.43  val ml = ML_Lex.read;
    1.44  
    1.45 @@ -135,20 +121,21 @@
    1.46    Outer_Syntax.command \<^command_keyword>\<open>method\<close>
    1.47      "prepare ISAC method and register it to Knowledge Store"
    1.48      (Parse.name -- Parse.!!! (\<^keyword>\<open>:\<close> |-- Parse.name --
    1.49 -      Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source -- parse_authors -- parse_program -- parse_ppc)) >>
    1.50 -      (fn (name, (id, (((source, mathauthors), simp), ppc))) => Toplevel.theory (fn thy =>
    1.51 +      Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source -- Problem.parse_authors --
    1.52 +        parse_program -- Problem.parse_model_input)) >>
    1.53 +      (fn (name, (id, (((source, maa), program), model_input))) => Toplevel.theory (fn thy =>
    1.54          let
    1.55            val metID = References_Def.explode_id id;
    1.56            val eval_input =
    1.57              ML_Context.expression (Input.pos_of source)
    1.58 -              (ml "Theory.setup (MethodC.set_input (" @ ML_Lex.read_source source @ ml "))")
    1.59 +              (ml "Theory.setup (MethodC.set_data (" @ ML_Lex.read_source source @ ml "))")
    1.60              |> Context.theory_map;
    1.61 -          val input = the_input (eval_input thy);
    1.62 +          val input = the_data (eval_input thy);
    1.63            val thm =
    1.64 -            (case simp of
    1.65 +            (case program of
    1.66                NONE => @{thm refl}
    1.67              | SOME a => Global_Theory.get_thm thy (Global_Theory.check_fact thy a));
    1.68 -          val arg = prep_input thy name mathauthors id_empty (metID, ppc, input, thm);
    1.69 +          val arg = prep_input thy name maa id_empty (metID, model_input, input, thm);
    1.70          in KEStore_Elems.add_mets [arg] thy end)))
    1.71  
    1.72  in end;