# HG changeset patch
# User wenzelm
# Date 1414771734 -3600
# Node ID fd0c85d7da38ed5e1ba378ef0d870d67525db88e
# Parent  c44aff8ac8940a78e28d653f0ecf8d3e7fb700bc
eliminated odd flags and hook;

diff -r c44aff8ac894 -r fd0c85d7da38 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Fri Oct 31 16:56:23 2014 +0100
+++ b/src/Pure/Isar/specification.ML	Fri Oct 31 17:08:54 2014 +0100
@@ -74,7 +74,6 @@
     (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
     (xstring * Position.T) list -> Element.context list -> Element.statement ->
     bool -> local_theory -> Proof.state
-  val add_theorem_hook: (bool -> Proof.state -> Proof.state) -> Context.generic -> Context.generic
 end;
 
 structure Specification: SPECIFICATION =
@@ -372,14 +371,6 @@
             #2 #> pair ths);
       in ((more_atts, prems, stmt, SOME facts), goal_ctxt) end);
 
-structure Theorem_Hook = Generic_Data
-(
-  type T = ((bool -> Proof.state -> Proof.state) * stamp) list;
-  val empty = [];
-  val extend = I;
-  fun merge data : T = Library.merge (eq_snd op =) data;
-);
-
 fun gen_theorem schematic bundle_includes prep_att prep_stmt
     kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int lthy =
   let
@@ -419,7 +410,6 @@
     |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
     |> tap (fn state => not schematic andalso Proof.schematic_goal state andalso
         error "Illegal schematic goal statement")
-    |> fold_rev (fn (f, _) => f int) (Theorem_Hook.get (Context.Proof goal_ctxt))
   end;
 
 in
@@ -434,8 +424,6 @@
 val schematic_theorem_cmd =
   gen_theorem true Bundle.includes_cmd Attrib.check_src Expression.read_statement;
 
-fun add_theorem_hook f = Theorem_Hook.map (cons (f, stamp ()));
-
 end;
 
 end;
diff -r c44aff8ac894 -r fd0c85d7da38 src/Pure/Isar/toplevel.ML
--- 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 *)
diff -r c44aff8ac894 -r fd0c85d7da38 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Fri Oct 31 16:56:23 2014 +0100
+++ b/src/Pure/System/isabelle_process.ML	Fri Oct 31 17:08:54 2014 +0100
@@ -204,7 +204,7 @@
     val channel = rendezvous ();
     val msg_channel = init_channels channel;
     val _ = Session.init_protocol_handlers ();
-    val _ = (loop |> Unsynchronized.setmp Toplevel.quiet true) channel;
+    val _ = loop channel;
   in Message_Channel.shutdown msg_channel end);
 
 fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);
diff -r c44aff8ac894 -r fd0c85d7da38 src/Tools/try.ML
--- a/src/Tools/try.ML	Fri Oct 31 16:56:23 2014 +0100
+++ b/src/Tools/try.ML	Fri Oct 31 17:08:54 2014 +0100
@@ -91,17 +91,6 @@
                            | _ => NONE)
   |> the_default state
 
-val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
-  let
-    val auto_time_limit = Options.default_real @{system_option auto_time_limit}
-  in
-    if interact andalso not (!Toplevel.quiet) andalso auto_time_limit > 0.0 then
-      TimeLimit.timeLimit (seconds auto_time_limit) auto_try state
-      handle TimeLimit.TimeOut => state
-    else
-      state
-  end))
-
 
 (* asynchronous print function (PIDE) *)