support for general theory presentation;
authorwenzelm
Fri May 11 22:40:02 2018 +0200 (13 months ago)
changeset 68153e469d529e6da
parent 68152 619de043389f
child 68154 42d63ea39161
support for general theory presentation;
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/Thy/thy_info.ML	Fri May 11 20:35:29 2018 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Fri May 11 22:40:02 2018 +0200
     1.3 @@ -7,6 +7,8 @@
     1.4  
     1.5  signature THY_INFO =
     1.6  sig
     1.7 +  val add_presentation: (theory -> unit) -> theory -> theory
     1.8 +  val apply_presentation: theory -> unit
     1.9    val get_names: unit -> string list
    1.10    val lookup_theory: string -> theory option
    1.11    val get_theory: string -> theory
    1.12 @@ -28,6 +30,23 @@
    1.13  structure Thy_Info: THY_INFO =
    1.14  struct
    1.15  
    1.16 +(** presentation of consolidated theory **)
    1.17 +
    1.18 +structure Presentation = Theory_Data
    1.19 +(
    1.20 +  type T = ((theory -> unit) * stamp) list;
    1.21 +  val empty = [];
    1.22 +  val extend = I;
    1.23 +  fun merge data : T = Library.merge (eq_snd op =) data;
    1.24 +);
    1.25 +
    1.26 +fun add_presentation f = Presentation.map (cons (f, stamp ()));
    1.27 +
    1.28 +fun apply_presentation thy =
    1.29 +  ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f thy));
    1.30 +
    1.31 +
    1.32 +
    1.33  (** thy database **)
    1.34  
    1.35  (* messages *)
    1.36 @@ -264,6 +283,7 @@
    1.37      fun present () =
    1.38        let
    1.39          val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
    1.40 +        val _ = apply_presentation thy;
    1.41        in
    1.42          if exists (Toplevel.is_skipped_proof o #2) res then ()
    1.43          else