removed obsolete present_results;
authorwenzelm
Wed Aug 13 20:57:31 2008 +0200 (2008-08-13)
changeset 27857fdf43ffceae0
parent 27856 b28b2baada06
child 27858 d385b67f8439
removed obsolete present_results;
added theory_results, which is subject to hooks (formerly in present.ML);
src/Pure/Isar/proof_display.ML
     1.1 --- a/src/Pure/Isar/proof_display.ML	Wed Aug 13 20:57:30 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Wed Aug 13 20:57:31 2008 +0200
     1.3 @@ -23,12 +23,10 @@
     1.4    val print_theorems_diff: theory -> theory -> unit
     1.5    val pretty_full_theory: bool -> theory -> Pretty.T
     1.6    val string_of_rule: Proof.context -> string -> thm -> string
     1.7 -  val print_results: bool -> Proof.context ->
     1.8 -    ((string * string) * (string * thm list) list) -> unit
     1.9 -  val present_results: Proof.context ->
    1.10 -    ((string * string) * (string * thm list) list) -> unit
    1.11 -  val pretty_consts: Proof.context ->
    1.12 -    (string * typ -> bool) -> (string * typ) list -> Pretty.T
    1.13 +  val print_results: bool -> Proof.context -> ((string * string) * (string * thm list) list) -> unit
    1.14 +  val add_hook: ((string * thm list) list -> unit) -> unit
    1.15 +  val theory_results: Proof.context -> ((string * string) * (string * thm list) list) -> unit
    1.16 +  val pretty_consts: Proof.context -> (string * typ -> bool) -> (string * typ) list -> Pretty.T
    1.17  end
    1.18  
    1.19  structure ProofDisplay: PROOF_DISPLAY =
    1.20 @@ -95,6 +93,25 @@
    1.21        [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk,
    1.22          Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]);
    1.23  
    1.24 +in
    1.25 +
    1.26 +fun print_results true = Pretty.writeln oo pretty_results
    1.27 +  | print_results false = K (K ());
    1.28 +
    1.29 +end;
    1.30 +
    1.31 +
    1.32 +(* theory results -- subject to hook *)
    1.33 +
    1.34 +local val hooks = ref ([]: ((string * thm list) list -> unit) list) in
    1.35 +
    1.36 +fun add_hook f = CRITICAL (fn () => change hooks (cons f));
    1.37 +fun get_hooks () = CRITICAL (fn () => ! hooks);
    1.38 +
    1.39 +end;
    1.40 +
    1.41 +local
    1.42 +
    1.43  fun name_results "" res = res
    1.44    | name_results name res =
    1.45        let
    1.46 @@ -113,14 +130,14 @@
    1.47  
    1.48  in
    1.49  
    1.50 -fun print_results true = Pretty.writeln oo pretty_results
    1.51 -  | print_results false = K (K ());
    1.52 -
    1.53 -fun present_results ctxt ((kind, name), res) =
    1.54 +fun theory_results ctxt ((kind, name), res) =
    1.55    if kind = "" orelse kind = Thm.internalK then ()
    1.56 -  else (print_results true ctxt ((kind, name), res);
    1.57 -    Context.setmp_thread_data (SOME (Context.Proof ctxt))
    1.58 -      (Present.results kind) (name_results name res));
    1.59 +  else
    1.60 +    let
    1.61 +      val _ = print_results true ctxt ((kind, name), res);
    1.62 +      val res' = name_results name res;
    1.63 +      val _ = List.app (fn f => f res') (get_hooks ());
    1.64 +    in () end;
    1.65  
    1.66  end;
    1.67