src/Pure/Isar/toplevel.ML

   val theory: (theory -> theory) -> transition -> transition
   val theory_to_proof: (bool -> theory -> ProofHistory.T) -> transition -> transition
   val proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition
   val proof': (bool -> ProofHistory.T -> ProofHistory.T) -> transition -> transition
   val proof_to_theory: (ProofHistory.T -> theory) -> transition -> transition
+  val quiet: bool ref
   val trace: bool ref
   val exn_message: exn -> string
   val apply: bool -> transition -> state -> (state * (exn * string) option) option
   val excursion: transition list -> unit
   val excursion_error: transition list -> unit

   | str_of_node (Proof _) = "in proof mode";
 
 fun print_node (Theory thy) = Pretty.writeln (Pretty.block
       [Pretty.str "Theory:", Pretty.brk 1, Pretty.str (PureThy.get_name thy),
         Pretty.str " =", Pretty.brk 1, Display.pretty_theory thy])
-  | print_node (Proof prf) =
-      (writeln ("Proof: step #" ^ string_of_int (ProofHistory.position prf));
-        Proof.print_state (ProofHistory.current prf));
+  | print_node (Proof prf) = Proof.print_state (ProofHistory.position prf) (ProofHistory.current prf);
 
 
 (* datatype state *)
 
 datatype state = State of (node History.T * ((node -> unit) * (node -> unit))) list;

 
 
 
 (** toplevel transactions **)
 
+val quiet = ref false;
 val trace = ref false;
 
 
 (* print exceptions *)
 

     val _ =
       if int orelse not int_only then ()
       else warning (command_msg "Executing interactive-only " tr);
     val (result, opt_exn) =
       (if ! trace then (writeln (command_msg "" tr); timeap) else I) (apply_trans int trans) state;
-    val _ = if int andalso print then print_state result else ();
+    val _ = if int andalso print andalso not (! quiet) then print_state result else ();
   in (result, apsome (fn UNDEF => type_error tr state | exn => exn) opt_exn) end;
 
 in
 
 fun apply int tr st =