# HG changeset patch
# User wenzelm
# Date 1399303662 -7200
# Node ID 6e26ae897badccf581b32aed33269d9e578a4892
# Parent  b5fb264d53baf4ee5412bd12794e750073b49475
uniform Toplevel.print for all proof commands;

diff -r b5fb264d53ba -r 6e26ae897bad src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon May 05 17:14:46 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon May 05 17:27:42 2014 +0200
@@ -673,32 +673,36 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "qed"} "conclude proof"
-    (Scan.option Method.parse >> (fn m => (Option.map Method.report m; Isar_Cmd.qed m)));
+    (Scan.option Method.parse >> (fn m =>
+     (Option.map Method.report m;
+      Toplevel.print o Isar_Cmd.qed m)));
 
 val _ =
   Outer_Syntax.command @{command_spec "by"} "terminal backward proof"
     (Method.parse -- Scan.option Method.parse >> (fn (m1, m2) =>
-      (Method.report m1; Option.map Method.report m2; Isar_Cmd.terminal_proof (m1, m2))));
+     (Method.report m1;
+      Option.map Method.report m2;
+      Toplevel.print o Isar_Cmd.terminal_proof (m1, m2))));
 
 val _ =
   Outer_Syntax.command @{command_spec ".."} "default proof"
-    (Scan.succeed Isar_Cmd.default_proof);
+    (Scan.succeed (Toplevel.print o Isar_Cmd.default_proof));
 
 val _ =
   Outer_Syntax.command @{command_spec "."} "immediate proof"
-    (Scan.succeed Isar_Cmd.immediate_proof);
+    (Scan.succeed (Toplevel.print o Isar_Cmd.immediate_proof));
 
 val _ =
   Outer_Syntax.command @{command_spec "done"} "done proof"
-    (Scan.succeed Isar_Cmd.done_proof);
+    (Scan.succeed (Toplevel.print o Isar_Cmd.done_proof));
 
 val _ =
   Outer_Syntax.command @{command_spec "sorry"} "skip proof (quick-and-dirty mode only!)"
-    (Scan.succeed Isar_Cmd.skip_proof);
+    (Scan.succeed (Toplevel.print o Isar_Cmd.skip_proof));
 
 val _ =
   Outer_Syntax.command @{command_spec "oops"} "forget proof"
-    (Scan.succeed Toplevel.forget_proof);
+    (Scan.succeed (Toplevel.print o Toplevel.forget_proof));
 
 
 (* proof steps *)
@@ -742,7 +746,8 @@
       Toplevel.skip_proof (fn h => (report_back (); h))));
 
 
-(* nested commands *)
+
+(** nested commands **)
 
 val props_text =
   Scan.optional Parse.properties [] -- Parse.position Parse.string