clarified load order;
authorwenzelm
Mon Oct 13 19:34:10 2014 +0200 (2014-10-13)
changeset 586608d4aebb9e327
parent 58659 6c9821c32dd5
child 58661 2b9485a2d152
clarified load order;
tuned signature;
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/Pure/Pure.thy
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/Tools/plugin.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Oct 13 18:45:48 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Oct 13 19:34:10 2014 +0200
     1.3 @@ -1614,7 +1614,7 @@
     1.4           Scan.repeat1 (Scan.unless (Parse.reserved "rel" ||
     1.5             Parse.reserved "plugins") Parse.term)) [] --
     1.6         Scan.option ((Parse.reserved "rel" -- @{keyword ":"}) |-- Parse.term) --
     1.7 -       Scan.optional Plugin_Name.parse_filter (K (K true))
     1.8 +       Scan.optional Plugin_Name.parse_filter (K Plugin_Name.default_filter)
     1.9         >> bnf_cmd);
    1.10  
    1.11  end;
     2.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Oct 13 18:45:48 2014 +0200
     2.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Oct 13 19:34:10 2014 +0200
     2.3 @@ -1066,11 +1066,11 @@
     2.4  
     2.5  val parse_bound_term = Parse.binding --| @{keyword ":"} -- Parse.term;
     2.6  
     2.7 -type ctr_options = (string -> bool) * bool;
     2.8 -type ctr_options_cmd = (Proof.context -> string -> bool) * bool;
     2.9 +type ctr_options = Plugin_Name.filter * bool;
    2.10 +type ctr_options_cmd = (Proof.context -> Plugin_Name.filter) * bool;
    2.11  
    2.12 -val default_ctr_options : ctr_options = (K true, false);
    2.13 -val default_ctr_options_cmd : ctr_options_cmd = (K (K true), false);
    2.14 +val default_ctr_options : ctr_options = (Plugin_Name.default_filter, false);
    2.15 +val default_ctr_options_cmd : ctr_options_cmd = (K Plugin_Name.default_filter, false);
    2.16  
    2.17  val parse_ctr_options =
    2.18    Scan.optional (@{keyword "("} |-- Parse.list1
     3.1 --- a/src/Pure/Pure.thy	Mon Oct 13 18:45:48 2014 +0200
     3.2 +++ b/src/Pure/Pure.thy	Mon Oct 13 19:34:10 2014 +0200
     3.3 @@ -120,7 +120,6 @@
     3.4  ML_file "Tools/proof_general_pure.ML"
     3.5  ML_file "Tools/simplifier_trace.ML"
     3.6  ML_file "Tools/named_theorems.ML"
     3.7 -ML_file "Tools/plugin.ML"
     3.8  
     3.9  
    3.10  section \<open>Basic attributes\<close>
     4.1 --- a/src/Pure/ROOT	Mon Oct 13 18:45:48 2014 +0200
     4.2 +++ b/src/Pure/ROOT	Mon Oct 13 19:34:10 2014 +0200
     4.3 @@ -210,6 +210,7 @@
     4.4      "Thy/thy_syntax.ML"
     4.5      "Tools/build.ML"
     4.6      "Tools/named_thms.ML"
     4.7 +    "Tools/plugin.ML"
     4.8      "Tools/proof_general.ML"
     4.9      "assumption.ML"
    4.10      "axclass.ML"
     5.1 --- a/src/Pure/ROOT.ML	Mon Oct 13 18:45:48 2014 +0200
     5.2 +++ b/src/Pure/ROOT.ML	Mon Oct 13 19:34:10 2014 +0200
     5.3 @@ -278,6 +278,7 @@
     5.4  use "Isar/bundle.ML";
     5.5  
     5.6  use "simplifier.ML";
     5.7 +use "Tools/plugin.ML";
     5.8  
     5.9  (*executable theory content*)
    5.10  use "Isar/code.ML";
     6.1 --- a/src/Pure/Tools/plugin.ML	Mon Oct 13 18:45:48 2014 +0200
     6.2 +++ b/src/Pure/Tools/plugin.ML	Mon Oct 13 19:34:10 2014 +0200
     6.3 @@ -15,8 +15,9 @@
     6.4    val declare: binding -> theory -> string * theory
     6.5    val declare_setup: binding -> string
     6.6    type filter = string -> bool
     6.7 +  val default_filter: filter
     6.8 +  val make_filter: Proof.context -> (Proof.context -> filter) -> filter
     6.9    val parse_filter: (Proof.context -> filter) parser
    6.10 -  val make_filter: Proof.context -> (Proof.context -> filter) -> filter
    6.11  end;
    6.12  
    6.13  structure Plugin_Name: PLUGIN_NAME =
    6.14 @@ -71,12 +72,14 @@
    6.15  
    6.16  type filter = string -> bool;
    6.17  
    6.18 +val default_filter: filter = K true;
    6.19 +
    6.20  fun make_filter (ctxt: Proof.context) f : filter = f ctxt;
    6.21  
    6.22  val parse_filter =
    6.23    Parse.position (Parse.reserved "plugins") --
    6.24      Parse.position (Parse.reserved "only" >> K I || Parse.reserved "del" >> K not) --
    6.25 -    (@{keyword ":"} |-- Scan.repeat (Parse.position Parse.name)) >>
    6.26 +    (Parse.$$$ ":" |-- Scan.repeat (Parse.position Parse.name)) >>
    6.27        (fn (((_, pos1), (modif, pos2)), args) => fn ctxt =>
    6.28          let
    6.29            val thy = Proof_Context.theory_of ctxt;