# HG changeset patch
# User wenzelm
# Date 1526071202 -7200
# Node ID e469d529e6da7d85093bbbda6ad6b494ce1e54ae
# Parent  619de043389fda7a08361623e60e62bffaccacd4
support for general theory presentation;

diff -r 619de043389f -r e469d529e6da src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Fri May 11 20:35:29 2018 +0200
+++ b/src/Pure/Thy/thy_info.ML	Fri May 11 22:40:02 2018 +0200
@@ -7,6 +7,8 @@
 
 signature THY_INFO =
 sig
+  val add_presentation: (theory -> unit) -> theory -> theory
+  val apply_presentation: theory -> unit
   val get_names: unit -> string list
   val lookup_theory: string -> theory option
   val get_theory: string -> theory
@@ -28,6 +30,23 @@
 structure Thy_Info: THY_INFO =
 struct
 
+(** presentation of consolidated theory **)
+
+structure Presentation = Theory_Data
+(
+  type T = ((theory -> unit) * stamp) list;
+  val empty = [];
+  val extend = I;
+  fun merge data : T = Library.merge (eq_snd op =) data;
+);
+
+fun add_presentation f = Presentation.map (cons (f, stamp ()));
+
+fun apply_presentation thy =
+  ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f thy));
+
+
+
 (** thy database **)
 
 (* messages *)
@@ -264,6 +283,7 @@
     fun present () =
       let
         val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
+        val _ = apply_presentation thy;
       in
         if exists (Toplevel.is_skipped_proof o #2) res then ()
         else