src/Pure/Tools/plugin.ML
changeset 58666 9e3426766267
parent 58665 50b229a5a097
child 58668 1891f17c6124
     1.1 --- a/src/Pure/Tools/plugin.ML	Mon Oct 13 21:41:29 2014 +0200
     1.2 +++ b/src/Pure/Tools/plugin.ML	Mon Oct 13 21:46:41 2014 +0200
     1.3 @@ -97,6 +97,7 @@
     1.4  sig
     1.5    type T
     1.6    val data: Plugin_Name.filter -> T -> local_theory -> local_theory
     1.7 +  val data_default: T -> local_theory -> local_theory
     1.8    val interpretation: string -> (T -> local_theory -> local_theory) -> theory -> theory
     1.9  end;
    1.10  
    1.11 @@ -178,6 +179,8 @@
    1.12      Plugin_Data.map (apfst (cons (mk_data filter (Sign.naming_of thy) x))) thy)
    1.13    #> consolidate;
    1.14  
    1.15 +val data_default = data Plugin_Name.default_filter;
    1.16 +
    1.17  fun interpretation name f =
    1.18    Plugin_Data.map (apsnd (cons (mk_interp name f, [])))
    1.19    #> perhaps consolidate';