src/Pure/Tools/plugin.ML
changeset 58660 8d4aebb9e327
parent 58658 9002fe021e2f
child 58665 50b229a5a097
     1.1 --- a/src/Pure/Tools/plugin.ML	Mon Oct 13 18:45:48 2014 +0200
     1.2 +++ b/src/Pure/Tools/plugin.ML	Mon Oct 13 19:34:10 2014 +0200
     1.3 @@ -15,8 +15,9 @@
     1.4    val declare: binding -> theory -> string * theory
     1.5    val declare_setup: binding -> string
     1.6    type filter = string -> bool
     1.7 +  val default_filter: filter
     1.8 +  val make_filter: Proof.context -> (Proof.context -> filter) -> filter
     1.9    val parse_filter: (Proof.context -> filter) parser
    1.10 -  val make_filter: Proof.context -> (Proof.context -> filter) -> filter
    1.11  end;
    1.12  
    1.13  structure Plugin_Name: PLUGIN_NAME =
    1.14 @@ -71,12 +72,14 @@
    1.15  
    1.16  type filter = string -> bool;
    1.17  
    1.18 +val default_filter: filter = K true;
    1.19 +
    1.20  fun make_filter (ctxt: Proof.context) f : filter = f ctxt;
    1.21  
    1.22  val parse_filter =
    1.23    Parse.position (Parse.reserved "plugins") --
    1.24      Parse.position (Parse.reserved "only" >> K I || Parse.reserved "del" >> K not) --
    1.25 -    (@{keyword ":"} |-- Scan.repeat (Parse.position Parse.name)) >>
    1.26 +    (Parse.$$$ ":" |-- Scan.repeat (Parse.position Parse.name)) >>
    1.27        (fn (((_, pos1), (modif, pos2)), args) => fn ctxt =>
    1.28          let
    1.29            val thy = Proof_Context.theory_of ctxt;