more general presentation hook, with document preparation as application;
authorwenzelm
Mon May 14 11:29:22 2018 +0200 (12 months ago)
changeset 68180112d9624c020
parent 68179 da70c9e91135
child 68181 34592bf86424
more general presentation hook, with document preparation as application;
src/Pure/Thy/export_theory.ML
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/Thy/export_theory.ML	Mon May 14 10:58:14 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Mon May 14 11:29:22 2018 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4  fun present_decls get_space get_decls =
     1.5    present get_space get_decls o export_decls;
     1.6  
     1.7 -val setup_presentation = Theory.setup o Thy_Info.add_presentation;
     1.8 +fun setup_presentation f = Theory.setup (Thy_Info.add_presentation (K f));
     1.9  
    1.10  
    1.11  (* types *)
     2.1 --- a/src/Pure/Thy/thy_info.ML	Mon May 14 10:58:14 2018 +0200
     2.2 +++ b/src/Pure/Thy/thy_info.ML	Mon May 14 11:29:22 2018 +0200
     2.3 @@ -7,8 +7,10 @@
     2.4  
     2.5  signature THY_INFO =
     2.6  sig
     2.7 -  val add_presentation: (theory -> unit) -> theory -> theory
     2.8 -  val apply_presentation: theory -> unit
     2.9 +  type presentation_context =
    2.10 +    {options: Options.T, pos: Position.T, segments: Thy_Output.segment list}
    2.11 +  val apply_presentation: presentation_context -> theory -> unit
    2.12 +  val add_presentation: (presentation_context -> theory -> unit) -> theory -> theory
    2.13    val get_names: unit -> string list
    2.14    val lookup_theory: string -> theory option
    2.15    val get_theory: string -> theory
    2.16 @@ -31,18 +33,28 @@
    2.17  
    2.18  (** presentation of consolidated theory **)
    2.19  
    2.20 +type presentation_context =
    2.21 +  {options: Options.T, pos: Position.T, segments: Thy_Output.segment list};
    2.22 +
    2.23  structure Presentation = Theory_Data
    2.24  (
    2.25 -  type T = ((theory -> unit) * stamp) list;
    2.26 +  type T = ((presentation_context -> theory -> unit) * stamp) list;
    2.27    val empty = [];
    2.28    val extend = I;
    2.29    fun merge data : T = Library.merge (eq_snd op =) data;
    2.30  );
    2.31  
    2.32 +fun apply_presentation (context: presentation_context) thy =
    2.33 +  ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f context thy));
    2.34 +
    2.35  fun add_presentation f = Presentation.map (cons (f, stamp ()));
    2.36  
    2.37 -fun apply_presentation thy =
    2.38 -  ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f thy));
    2.39 +val _ =
    2.40 +  Theory.setup (add_presentation (fn {options, pos, segments} => fn thy =>
    2.41 +    if exists (Toplevel.is_skipped_proof o #result_state) segments then ()
    2.42 +    else
    2.43 +      let val body = Thy_Output.present_thy thy segments;
    2.44 +      in if Present.document_enabled options then Present.theory_output pos thy body else () end));
    2.45  
    2.46  
    2.47  
    2.48 @@ -297,13 +309,8 @@
    2.49        let
    2.50          val segments = (spans ~~ maps Toplevel.join_results results)
    2.51            |> map (fn (span, (tr, st')) => {span = span, tr = tr, result_state = st'});
    2.52 -        val _ = apply_presentation thy;
    2.53 -      in
    2.54 -        if exists (Toplevel.is_skipped_proof o #result_state) segments then ()
    2.55 -        else
    2.56 -          let val body = Thy_Output.present_thy thy segments;
    2.57 -          in if Present.document_enabled options then Present.theory_output text_pos thy body else () end
    2.58 -      end;
    2.59 +        val context = {options = options, pos = text_pos, segments = segments};
    2.60 +      in apply_presentation context thy end;
    2.61    in (thy, present, size text) end;
    2.62  
    2.63