local qeds: pass cond_print_result;
authorwenzelm
Wed May 26 16:51:05 1999 +0200 (1999-05-26 ago)
changeset 6732cf9f66ca9ee3
parent 6731 57e761134c85
child 6733 429bbd7ef26d
local qeds: pass cond_print_result;
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Wed May 26 16:50:36 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Wed May 26 16:51:05 1999 +0200
     1.3 @@ -285,21 +285,27 @@
     1.4    ProofHistory.applys o Method.proof o apsome Comment.ignore_interest o Comment.ignore_interest';
     1.5  
     1.6  
     1.7 +(* print result *)
     1.8 +
     1.9 +fun pretty_result {kind, name, thm} =
    1.10 +  Pretty.block [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Display.pretty_thm thm];
    1.11 +
    1.12 +val print_result = Pretty.writeln o pretty_result;
    1.13 +fun cond_print_result int res = if int then print_result res else ();
    1.14 +
    1.15 +fun proof'' f = Toplevel.proof' (f o cond_print_result);
    1.16 +
    1.17 +
    1.18  (* local endings *)
    1.19  
    1.20  val local_qed =
    1.21 -  Toplevel.proof' o (ProofHistory.applys_close oo Method.local_qed)
    1.22 -    o apsome Comment.ignore_interest;
    1.23 +  proof'' o (ProofHistory.applys_close oo Method.local_qed) o apsome Comment.ignore_interest;
    1.24  
    1.25  val local_terminal_proof =
    1.26 -  Toplevel.proof' o (ProofHistory.applys_close oo Method.local_terminal_proof)
    1.27 -    o Comment.ignore_interest;
    1.28 +  proof'' o (ProofHistory.applys_close oo Method.local_terminal_proof) o Comment.ignore_interest;
    1.29  
    1.30 -val local_immediate_proof =
    1.31 -  Toplevel.proof' (ProofHistory.applys_close o Method.local_immediate_proof);
    1.32 -
    1.33 -val local_default_proof =
    1.34 -  Toplevel.proof' (ProofHistory.applys_close o Method.local_default_proof);
    1.35 +val local_immediate_proof = proof'' (ProofHistory.applys_close o Method.local_immediate_proof);
    1.36 +val local_default_proof = proof'' (ProofHistory.applys_close o Method.local_default_proof);
    1.37  
    1.38  
    1.39  (* global endings *)
    1.40 @@ -310,11 +316,8 @@
    1.41    let
    1.42      val state = ProofHistory.current prf;
    1.43      val _ = if Proof.at_bottom state then () else raise Toplevel.UNDEF;
    1.44 -    val (thy, {kind, name, thm}) = finish state;
    1.45 -
    1.46 -    val prt_result = Pretty.block
    1.47 -      [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Display.pretty_thm thm];
    1.48 -  in Pretty.writeln prt_result; thy end);
    1.49 +    val (thy, res) = finish state;
    1.50 +  in print_result res; thy end);
    1.51  
    1.52  fun gen_global_qed_with prep_att (alt_name, raw_atts) meth state =
    1.53    let