--- 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