# HG changeset patch # User wenzelm # Date 1399464317 -7200 # Node ID ba507cc9647360cee9bab82cab633aae75ab0eba # Parent c668735fb8b56a90a729fbfe7cd44529b524d76f tuned message: "step" goes back to TTY mode before Proof General, while "depth" is more informative but sometimes confusing due to implementation details; diff -r c668735fb8b5 -r ba507cc96473 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Wed May 07 13:55:16 2014 +0200 +++ b/src/Pure/Isar/proof.ML Wed May 07 14:05:17 2014 +0200 @@ -365,8 +365,7 @@ else if mode = Backward then Proof_Context.pretty_ctxt ctxt else []; in - [Pretty.str ("proof (" ^ mode_name mode ^ "): step " ^ string_of_int nr ^ - (if verbose then ", depth " ^ string_of_int (level state div 2 - 1) else "")), + [Pretty.str ("proof (" ^ 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