# HG changeset patch
# User wenzelm
# Date 1394640125 -3600
# Node ID 600781e03bf6d93e8e4190860e3aa8e0522d8d50
# Parent  7658489047e3d8d87034a6f27d86216097768158
more explicit markup and explanation of the improper status of 'back', following the AFP style-guide;

diff -r 7658489047e3 -r 600781e03bf6 src/Doc/IsarRef/Proof.thy
--- a/src/Doc/IsarRef/Proof.thy	Wed Mar 12 16:43:17 2014 +0100
+++ b/src/Doc/IsarRef/Proof.thy	Wed Mar 12 17:02:05 2014 +0100
@@ -897,8 +897,10 @@
   front.
   
   \item @{command "back"} does back-tracking over the result sequence
-  of the latest proof command.  Basically, any proof command may
-  return multiple results.
+  of the latest proof command.  Any proof command may return multiple
+  results, and this command explores the possibilities step-by-step.
+  It is mainly useful for experimentation and interactive exploration,
+  and should be avoided in finished proofs.
   
   \end{description}
 
diff -r 7658489047e3 -r 600781e03bf6 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Mar 12 16:43:17 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Mar 12 17:02:05 2014 +0100
@@ -699,9 +699,14 @@
 
 (* proof navigation *)
 
+fun report_back () =
+  Output.report (Markup.markup Markup.bad "Explicit backtracking");
+
 val _ =
-  Outer_Syntax.command @{command_spec "back"} "backtracking of proof command"
-    (Scan.succeed (Toplevel.print o Toplevel.actual_proof Proof_Node.back o Toplevel.skip_proof I));
+  Outer_Syntax.command @{command_spec "back"} "explicit backtracking of proof command"
+    (Scan.succeed (Toplevel.print o
+      Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o
+      Toplevel.skip_proof (fn h => (report_back (); h))));
 
 
 (* nested commands *)