1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed May 26 16:19:41 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed May 26 16:24:05 2021 +0200
     1.3 @@ -15,7 +15,9 @@
     1.4  appropriate use of polymorphic high order functions.
     1.5  *)
     1.6  
     1.7 -theory Know_Store imports Complex_Main
     1.8 +theory Know_Store
     1.9 +  imports Complex_Main
    1.10 +  keywords "setup_rule" :: thy_decl
    1.11  begin
    1.12  
    1.13  setup \<open>
    1.14 @@ -166,6 +168,35 @@
    1.15  end;
    1.16  \<close>
    1.17  
    1.18 +
    1.19 +subsection \<open>Isar command syntax\<close>
    1.20 +
    1.21 +ML \<open>
    1.22 +local
    1.23 +
    1.24 +val parse_rule = Parse.name -- Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source);
    1.25 +
    1.26 +val ml = ML_Lex.read;
    1.27 +
    1.28 +fun ml_rule thy (name, source) =
    1.29 +  ml "(" @ ml (ML_Syntax.print_string name) @ ml ", " @
    1.30 +  ml "(" @ ml (ML_Syntax.print_string (Context.theory_name thy)) @ ml ", " @
    1.31 +  ML_Lex.read_source source @ ml "))";
    1.32 +
    1.33 +fun ml_rules thy args =
    1.34 +  ml "Theory.setup (KEStore_Elems.add_rlss [" @
    1.35 +    flat (separate (ml ",") (map (ml_rule thy) args)) @ ml "])";
    1.36 +
    1.37 +val _ =
    1.38 +  Outer_Syntax.command \<^command_keyword>\<open>setup_rule\<close> "setup ISAC rules"
    1.39 +    (Parse.and_list1 parse_rule >> (fn args => Toplevel.theory (fn thy =>
    1.40 +      thy |> Context.theory_map
    1.41 +        (ML_Context.expression (Position.thread_data ()) (ml_rules thy args)))));
    1.42 +
    1.43 +in end;
    1.44 +\<close>
    1.45 +
    1.46 +
    1.47  section \<open>Re-use existing access functions for knowledge elements\<close>
    1.48  text \<open>
    1.49    The independence of problems' and methods' structure enforces the accesse
    1.50 @@ -206,9 +237,10 @@
    1.51  fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets;
    1.52  fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
    1.53  \<close>
    1.54 -setup \<open>KEStore_Elems.add_rlss 
    1.55 -  [("empty", (Context.theory_name @{theory}, Rule_Set.empty)), 
    1.56 -  ("e_rrls", (Context.theory_name @{theory}, Rule_Set.e_rrls))]\<close>
    1.57 +
    1.58 +setup_rule
    1.59 +  empty = \<open>Rule_Set.empty\<close> and
    1.60 +  e_rrls = \<open>Rule_Set.e_rrls\<close>
    1.61  
    1.62  section \<open>determine sequence of main parts in thehier\<close>
    1.63  setup \<open>