# HG changeset patch
# User wenzelm
# Date 1413221650 -7200
# Node ID 8d4aebb9e327900207cc35c011bee99eda59483f
# Parent  6c9821c32dd57b327fed2ff784978266081cb5ec
clarified load order;
tuned signature;

diff -r 6c9821c32dd5 -r 8d4aebb9e327 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Oct 13 18:45:48 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Oct 13 19:34:10 2014 +0200
@@ -1614,7 +1614,7 @@
          Scan.repeat1 (Scan.unless (Parse.reserved "rel" ||
            Parse.reserved "plugins") Parse.term)) [] --
        Scan.option ((Parse.reserved "rel" -- @{keyword ":"}) |-- Parse.term) --
-       Scan.optional Plugin_Name.parse_filter (K (K true))
+       Scan.optional Plugin_Name.parse_filter (K Plugin_Name.default_filter)
        >> bnf_cmd);
 
 end;
diff -r 6c9821c32dd5 -r 8d4aebb9e327 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Oct 13 18:45:48 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Oct 13 19:34:10 2014 +0200
@@ -1066,11 +1066,11 @@
 
 val parse_bound_term = Parse.binding --| @{keyword ":"} -- Parse.term;
 
-type ctr_options = (string -> bool) * bool;
-type ctr_options_cmd = (Proof.context -> string -> bool) * bool;
+type ctr_options = Plugin_Name.filter * bool;
+type ctr_options_cmd = (Proof.context -> Plugin_Name.filter) * bool;
 
-val default_ctr_options : ctr_options = (K true, false);
-val default_ctr_options_cmd : ctr_options_cmd = (K (K true), false);
+val default_ctr_options : ctr_options = (Plugin_Name.default_filter, false);
+val default_ctr_options_cmd : ctr_options_cmd = (K Plugin_Name.default_filter, false);
 
 val parse_ctr_options =
   Scan.optional (@{keyword "("} |-- Parse.list1
diff -r 6c9821c32dd5 -r 8d4aebb9e327 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Oct 13 18:45:48 2014 +0200
+++ b/src/Pure/Pure.thy	Mon Oct 13 19:34:10 2014 +0200
@@ -120,7 +120,6 @@
 ML_file "Tools/proof_general_pure.ML"
 ML_file "Tools/simplifier_trace.ML"
 ML_file "Tools/named_theorems.ML"
-ML_file "Tools/plugin.ML"
 
 
 section \<open>Basic attributes\<close>
diff -r 6c9821c32dd5 -r 8d4aebb9e327 src/Pure/ROOT
--- a/src/Pure/ROOT	Mon Oct 13 18:45:48 2014 +0200
+++ b/src/Pure/ROOT	Mon Oct 13 19:34:10 2014 +0200
@@ -210,6 +210,7 @@
     "Thy/thy_syntax.ML"
     "Tools/build.ML"
     "Tools/named_thms.ML"
+    "Tools/plugin.ML"
     "Tools/proof_general.ML"
     "assumption.ML"
     "axclass.ML"
diff -r 6c9821c32dd5 -r 8d4aebb9e327 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Oct 13 18:45:48 2014 +0200
+++ b/src/Pure/ROOT.ML	Mon Oct 13 19:34:10 2014 +0200
@@ -278,6 +278,7 @@
 use "Isar/bundle.ML";
 
 use "simplifier.ML";
+use "Tools/plugin.ML";
 
 (*executable theory content*)
 use "Isar/code.ML";
diff -r 6c9821c32dd5 -r 8d4aebb9e327 src/Pure/Tools/plugin.ML
--- a/src/Pure/Tools/plugin.ML	Mon Oct 13 18:45:48 2014 +0200
+++ b/src/Pure/Tools/plugin.ML	Mon Oct 13 19:34:10 2014 +0200
@@ -15,8 +15,9 @@
   val declare: binding -> theory -> string * theory
   val declare_setup: binding -> string
   type filter = string -> bool
+  val default_filter: filter
+  val make_filter: Proof.context -> (Proof.context -> filter) -> filter
   val parse_filter: (Proof.context -> filter) parser
-  val make_filter: Proof.context -> (Proof.context -> filter) -> filter
 end;
 
 structure Plugin_Name: PLUGIN_NAME =
@@ -71,12 +72,14 @@
 
 type filter = string -> bool;
 
+val default_filter: filter = K true;
+
 fun make_filter (ctxt: Proof.context) f : filter = f ctxt;
 
 val parse_filter =
   Parse.position (Parse.reserved "plugins") --
     Parse.position (Parse.reserved "only" >> K I || Parse.reserved "del" >> K not) --
-    (@{keyword ":"} |-- Scan.repeat (Parse.position Parse.name)) >>
+    (Parse.$$$ ":" |-- Scan.repeat (Parse.position Parse.name)) >>
       (fn (((_, pos1), (modif, pos2)), args) => fn ctxt =>
         let
           val thy = Proof_Context.theory_of ctxt;