--- a/src/Pure/Isar/proof.ML Thu May 08 15:30:28 2014 +0200
+++ b/src/Pure/Isar/proof.ML Thu May 08 16:15:20 2014 +0200
@@ -364,8 +364,12 @@
if verbose orelse mode = Forward then Proof_Context.pretty_context ctxt
else if mode = Backward then Proof_Context.pretty_ctxt ctxt
else [];
+
+ val position_markup = Position.markup (Position.thread_data ()) Markup.position;
in
- [Pretty.str ("proof (" ^ mode_name mode ^ "): depth " ^ string_of_int (level state div 2 - 1)),
+ [Pretty.block
+ [Pretty.mark_str (position_markup, "proof"),
+ Pretty.str (" (" ^ mode_name mode ^ "): depth " ^ string_of_int (level state div 2 - 1))],
Pretty.str ""] @
(if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @
(if verbose orelse mode = Forward then