--- a/src/Pure/Isar/toplevel.ML Fri Oct 31 16:56:23 2014 +0100
+++ b/src/Pure/Isar/toplevel.ML Fri Oct 31 17:08:54 2014 +0100
@@ -26,8 +26,6 @@
val pretty_state: state -> Pretty.T list
val print_state: state -> unit
val pretty_abstract: state -> Pretty.T
- val quiet: bool Unsynchronized.ref
- val interact: bool Unsynchronized.ref
val timing: bool Unsynchronized.ref
val profiling: int Unsynchronized.ref
type transition
@@ -213,9 +211,7 @@
(** toplevel transitions **)
-val quiet = Unsynchronized.ref false; (*Proof General legacy*)
-val interact = Unsynchronized.ref false; (*Proof General legacy*)
-val timing = Unsynchronized.ref false; (*Proof General legacy*)
+val timing = Unsynchronized.ref false;
val profiling = Unsynchronized.ref 0;
@@ -528,12 +524,10 @@
(fn Proof (prf, x) => Proof (f prf, x)
| _ => raise UNDEF));
-(*Proof General legacy*)
fun skip_proof f = transaction (fn _ =>
(fn Skipped_Proof (h, x) => Skipped_Proof (f h, x)
| _ => raise UNDEF));
-(*Proof General legacy*)
fun skip_proof_to_theory pred = transaction (fn _ =>
(fn Skipped_Proof (d, (gthy, _)) => if pred d then Theory (gthy, NONE) else raise UNDEF
| _ => raise UNDEF));
@@ -580,10 +574,6 @@
val (result, opt_err) =
state |> (apply_trans int trans |> ! profiling > 0 ? profile (! profiling));
- val _ =
- if int andalso not (! quiet) andalso Keyword.is_printed name
- then print_state result else ();
-
val timing_result = Timing.result timing_start;
val timing_props =
Markup.command_timing :: (Markup.nameN, name_of tr) :: Position.properties_of (pos_of tr);
@@ -627,7 +617,7 @@
if Exn.is_interrupt exn then reraise exn else raise Runtime.EXCURSION_FAIL (exn, info)
| NONE => raise Runtime.EXCURSION_FAIL (Runtime.TERMINATE, at_command tr));
-fun command tr = command_exception (! interact) tr;
+val command = command_exception false;
(* reset state *)