support for named plugins for definitional packages;

--- a/src/Pure/Pure.thy	Sun Oct 12 21:52:45 2014 +0200
+++ b/src/Pure/Pure.thy	Mon Oct 13 15:45:23 2014 +0200
@@ -120,6 +120,7 @@
 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>

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/plugin.ML	Mon Oct 13 15:45:23 2014 +0200
@@ -0,0 +1,171 @@
+(*  Title:      Pure/Tools/plugin.ML
+    Author:     Makarius
+    Author:     Jasmin Blanchette
+
+Named plugins for definitional packages.
+*)
+
+(** plugin name **)
+
+signature PLUGIN_NAME =
+sig
+  val check: Proof.context -> xstring * Position.T -> string
+  val declare: binding -> theory -> string * theory
+  val setup: binding -> string
+  type filter = string -> bool
+  val parse_filter: (Proof.context -> filter) parser
+  val make_filter: Proof.context -> (Proof.context -> filter) -> filter
+end;
+
+structure Plugin_Name: PLUGIN_NAME =
+struct
+
+(* theory data *)
+
+structure Data = Theory_Data
+(
+  type T = unit Name_Space.table;
+  val empty: T = Name_Space.empty_table "plugin";
+  val extend = I;
+  val merge = Name_Space.merge_tables;
+);
+
+
+(* check *)
+
+fun check ctxt =
+  #1 o Name_Space.check (Context.Proof ctxt) (Data.get (Proof_Context.theory_of ctxt));
+
+val _ = Theory.setup
+  (ML_Antiquotation.inline @{binding plugin}
+    (Args.context -- Scan.lift (Parse.position Args.name)
+      >> (ML_Syntax.print_string o uncurry check)));
+
+
+(* declare *)
+
+fun declare binding thy =
+  let
+    val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.default_naming);
+    val (name, data') = Name_Space.define context true (binding, ()) (Data.get thy);
+    val thy' = Data.put data' thy;
+  in (name, thy') end;
+
+fun setup binding = Context.>>> (Context.map_theory_result (declare binding));
+
+
+(* filter *)
+
+type filter = string -> bool;
+
+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)) >>
+      (fn (((_, pos1), (modif, pos2)), args) => fn ctxt =>
+        let
+          val _ = Context_Position.reports ctxt (map (rpair Markup.quasi_keyword) [pos1, pos2]);
+          val names = map (check ctxt) args;
+        in modif o member (op =) names end);
+
+end;
+
+
+
+(** plugin content **)
+
+signature PLUGIN =
+sig
+  type T
+  val data: Plugin_Name.filter -> T -> local_theory -> local_theory
+  val interpretation: string -> (T -> local_theory -> local_theory) -> theory -> theory
+end;
+
+functor Plugin(type T): PLUGIN =
+struct
+
+type T = T;
+
+
+(* data with interpretation *)
+
+type data = {filter: Plugin_Name.filter, naming: Name_Space.naming, value: T, id: serial};
+type interp = {name: string, apply: T -> local_theory -> local_theory, id: serial};
+
+val eq_data: data * data -> bool = op = o pairself #id;
+val eq_interp: interp * interp -> bool = op = o pairself #id;
+
+fun mk_data filter naming x : data = {filter = filter, naming = naming, value = x, id = serial ()};
+fun mk_interp name f : interp = {name = name, apply = f, id = serial ()};
+
+
+(* theory data *)
+
+structure Plugin_Data = Theory_Data
+(
+  type T = data list * (interp * data list) list;
+  val empty : T = ([], []);
+  val extend = I;
+  val merge_data = merge eq_data;
+  fun merge ((data1, interps1), (data2, interps2)) : T =
+    (merge_data (data1, data2), AList.join eq_interp (K merge_data) (interps1, interps2));
+);
+
+
+(* consolidate data wrt. interpretations *)
+
+local
+
+fun apply change_naming (interp: interp) (data: data) lthy =
+  lthy
+  |> change_naming ? Local_Theory.map_naming (K (#naming data))
+  |> #apply interp (#value data)
+  |> Local_Theory.restore_naming lthy;
+
+fun unfinished data (interp: interp, data') =
+  (interp,
+    if eq_list eq_data (data, data') then []
+    else data |> filter (fn d => #filter d (#name interp) andalso not (member eq_data data' d)));
+
+fun unfinished_data thy =
+  let
+    val (data, interps) = Plugin_Data.get thy;
+    val finished = map (apsnd (K data)) interps;
+    val thy' = Plugin_Data.put (data, finished) thy;
+  in (map (unfinished data) interps, thy') end;
+
+in
+
+val consolidate =
+  Local_Theory.raw_theory_result unfinished_data
+  #-> fold_rev (fn (interp, data) => fold_rev (apply false interp) data);
+
+val consolidate' =
+  unfinished_data #> (fn (unfinished, thy) =>
+    if forall (null o #2) unfinished then NONE
+    else
+      Named_Target.theory_init thy
+      |> fold_rev (fn (interp, data) => fold_rev (apply true interp) data) unfinished
+      |> Local_Theory.exit_global
+      |> SOME);
+
+end;
+
+val _ = Theory.setup (Theory.at_begin consolidate');
+
+
+(* add content *)
+
+fun data filter x =
+  Local_Theory.background_theory (fn thy =>
+    Plugin_Data.map (apfst (cons (mk_data filter (Sign.naming_of thy) x))) thy)
+  #> consolidate;
+
+fun interpretation name f =
+  Plugin_Data.map (apsnd (cons (mk_interp name f, [])))
+  #> perhaps consolidate';
+
+end;
+