merged
authorwenzelm
Tue, 26 Oct 2010 11:06:12 +0200
changeset 40148 8728165d366e
parent 40147 d170c322157a (current diff)
parent 40134 8baded087d34 (diff)
child 40149 4c35be108990
merged
src/Tools/quickcheck.ML
--- a/src/HOL/Mutabelle/MutabelleExtra.thy	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/HOL/Mutabelle/MutabelleExtra.thy	Tue Oct 26 11:06:12 2010 +0200
@@ -19,10 +19,11 @@
      "mutabelle_extra.ML"
 begin
 
-ML {* val old_tr = !Output.tracing_fn *}
-ML {* val old_wr = !Output.writeln_fn *}
-ML {* val old_pr = !Output.priority_fn *}
-ML {* val old_wa = !Output.warning_fn *}
+(* FIXME !?!?! *)
+ML {* val old_tr = !Output.Private_Hooks.tracing_fn *}
+ML {* val old_wr = !Output.Private_Hooks.writeln_fn *}
+ML {* val old_ur = !Output.Private_Hooks.urgent_message_fn *}
+ML {* val old_wa = !Output.Private_Hooks.warning_fn *}
 
 quickcheck_params [size = 5, iterations = 1000]
 (*
@@ -48,9 +49,10 @@
 *)
  *}
 
-ML {* Output.tracing_fn := old_tr *}
-ML {* Output.writeln_fn := old_wr *}
-ML {* Output.priority_fn := old_pr *}
-ML {* Output.warning_fn := old_wa *}
+(* FIXME !?!?! *)
+ML {* Output.Private_Hooks.tracing_fn := old_tr *}
+ML {* Output.Private_Hooks.writeln_fn := old_wr *}
+ML {* Output.Private_Hooks.urgent_message_fn := old_ur *}
+ML {* Output.Private_Hooks.warning_fn := old_wa *}
 
 end
--- a/src/HOL/Mutabelle/mutabelle.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -499,14 +499,14 @@
 fun is_executable thy insts th =
  (Quickcheck.test_term
     (ProofContext.init_global thy) false (SOME (!testgen_name)) 1 1 (preprocess thy insts (prop_of th));
-  priority "executable"; true) handle ERROR s =>
-    (priority ("not executable: " ^ s); false);
+  Output.urgent_message "executable"; true) handle ERROR s =>
+    (Output.urgent_message ("not executable: " ^ s); false);
 
 fun qc_recursive usedthy [] insts sz qciter acc = rev acc
  | qc_recursive usedthy (x::xs) insts sz qciter acc = qc_recursive usedthy xs insts sz qciter 
-     (priority ("qc_recursive: " ^ string_of_int (length xs)); ((x, pretty (the_default [] (Quickcheck.test_term
+     (Output.urgent_message ("qc_recursive: " ^ string_of_int (length xs)); ((x, pretty (the_default [] (Quickcheck.test_term
        (ProofContext.init_global usedthy) false (SOME (!testgen_name)) sz qciter (preprocess usedthy insts x)))) :: acc))
-          handle ERROR msg => (priority msg; qc_recursive usedthy xs insts sz qciter acc);
+          handle ERROR msg => (Output.urgent_message msg; qc_recursive usedthy xs insts sz qciter acc);
 
 
 (*quickcheck-test the mutants created by function mutate with type-instantiation insts, 
@@ -721,11 +721,11 @@
 fun mutqc_thystat option p mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename =
  let
    val thmlist = filter
-     (fn (s, th) => not (p s th) andalso (priority s; is_executable mutthy insts th)) (thms_of mutthy)
+     (fn (s, th) => not (p s th) andalso (Output.urgent_message s; is_executable mutthy insts th)) (thms_of mutthy)
    fun mutthmrec [] = ()
    |   mutthmrec ((name,thm)::xs) =
      let          
-       val _ = priority ("mutthmrec: " ^ name);
+       val _ = Output.urgent_message ("mutthmrec: " ^ name);
        val mutated = mutate option (prop_of thm) usedthy
            commutatives forbidden_funs iter
        val (passednum,_,cenum,_) = qc_test mutated insts usedthy sz qciter
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -109,7 +109,7 @@
 fun invoke_refute thy t =
   let
     val res = MyRefute.refute_term thy [] t
-    val _ = priority ("Refute: " ^ res)
+    val _ = Output.urgent_message ("Refute: " ^ res)
   in
     case res of
       "genuine" => GenuineCex
@@ -137,7 +137,7 @@
   in
     let
       val (res, _) = Nitpick.pick_nits_in_term state (Nitpick_Isar.default_params thy []) false [] t
-      val _ = priority ("Nitpick: " ^ res)
+      val _ = Output.urgent_message ("Nitpick: " ^ res)
     in
       case res of
         "genuine" => GenuineCex
@@ -182,7 +182,7 @@
            (error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^
                    "."))
          | Exn.Interrupt => raise Exn.Interrupt
-         | _ => (priority ("Unknown error in Nitpick"); Error)
+         | _ => (Output.urgent_message ("Unknown error in Nitpick"); Error)
   end
 val nitpick_mtd = ("nitpick", invoke_nitpick)
 *)
@@ -281,13 +281,13 @@
 
 fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t =
   let
-    val _ = priority ("Invoking " ^ mtd_name)
+    val _ = Output.urgent_message ("Invoking " ^ mtd_name)
     val ((res, (timing, reports)), time) = cpu_time "total time"
       (fn () => case try (invoke_mtd thy) t of
           SOME (res, (timing, reports)) => (res, (timing, reports))
-        | NONE => (priority ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
+        | NONE => (Output.urgent_message ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
            (Error , ([], NONE))))
-    val _ = priority (" Done")
+    val _ = Output.urgent_message (" Done")
   in (res, (time :: timing, reports)) end
 
 (* theory -> term list -> mtd -> subentry *)
@@ -316,7 +316,7 @@
 fun mutate_theorem create_entry thy mtds thm =
   let
     val exec = is_executable_thm thy thm
-    val _ = priority (if exec then "EXEC" else "NOEXEC")
+    val _ = Output.urgent_message (if exec then "EXEC" else "NOEXEC")
     val mutants =
           (if num_mutations = 0 then
              [Thm.prop_of thm]
@@ -327,7 +327,7 @@
     val mutants =
       if exec then
         let
-          val _ = priority ("BEFORE PARTITION OF " ^
+          val _ = Output.urgent_message ("BEFORE PARTITION OF " ^
                             Int.toString (length mutants) ^ " MUTANTS")
           val (execs, noexecs) = List.partition (is_executable_term thy) (take_random (20 * max_mutants) mutants)
           val _ = tracing ("AFTER PARTITION (" ^ Int.toString (length execs) ^
@@ -342,7 +342,7 @@
           |> map Mutabelle.freeze |> map freezeT
 (*          |> filter (not o is_forbidden_mutant) *)
           |> List.mapPartial (try (Sign.cert_term thy))
-    val _ = map (fn t => priority ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
+    val _ = map (fn t => Output.urgent_message ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
   in
     create_entry thy thm exec mutants mtds
   end
@@ -421,7 +421,7 @@
 (* theory -> mtd list -> thm list -> string -> unit *)
 fun mutate_theorems_and_write_report thy mtds thms file_name =
   let
-    val _ = priority "Starting Mutabelle..."
+    val _ = Output.urgent_message "Starting Mutabelle..."
     val path = Path.explode file_name
     (* for normal report: *)
     (*val (gen_create_entry, gen_string_for_entry) = (create_entry, string_for_entry)*)
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -216,7 +216,7 @@
         o Pretty.chunks o cons (Pretty.str "") o single
         o Pretty.mark Markup.hilite
       else
-        (fn s => (priority s; if debug then tracing s else ()))
+        (fn s => (Output.urgent_message s; if debug then tracing s else ()))
         o Pretty.string_of
     fun pprint_m f = () |> not auto ? pprint o f
     fun pprint_v f = () |> verbose ? pprint o f
@@ -989,7 +989,7 @@
            raise Interrupt
          else
            if passed_deadline deadline then
-             (priority "Nitpick ran out of time."; ("unknown", state))
+             (Output.urgent_message "Nitpick ran out of time."; ("unknown", state))
            else
              error "Nitpick was interrupted."
 
@@ -1040,7 +1040,7 @@
     val t = state |> Proof.raw_goal |> #goal |> prop_of
   in
     case Logic.count_prems t of
-      0 => (priority "No subgoal!"; ("none", state))
+      0 => (Output.urgent_message "No subgoal!"; ("none", state))
     | n =>
       let
         val t = Logic.goal_params t i |> fst
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -2054,7 +2054,7 @@
                     map (wf_constraint_for_triple rel) triples
                     |> foldr1 s_conj |> HOLogic.mk_Trueprop
          val _ = if debug then
-                   priority ("Wellfoundedness goal: " ^
+                   Output.urgent_message ("Wellfoundedness goal: " ^
                              Syntax.string_of_term ctxt prop ^ ".")
                  else
                    ()
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -1043,7 +1043,7 @@
                                      (fn (s, []) => TFree (s, HOLogic.typeS)
                                        | x => TFree x))
        val _ = if debug then
-                 priority ((if negate then "Genuineness" else "Spuriousness") ^
+                 Output.urgent_message ((if negate then "Genuineness" else "Spuriousness") ^
                            " goal: " ^ Syntax.string_of_term ctxt prop ^ ".")
                else
                  ()
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -327,7 +327,7 @@
     fun try' j =
       if j <= i then
         let
-          val _ = if quiet then () else priority ("Executing depth " ^ string_of_int j)
+          val _ = if quiet then () else Output.urgent_message ("Executing depth " ^ string_of_int j)
         in
           case f j handle Match => (if quiet then ()
              else warning "Exception Match raised during quickcheck"; NONE)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -169,7 +169,7 @@
       sort_strings (available_atps thy) @ smt_prover_names
       |> List.partition (String.isPrefix remote_prefix)
   in
-    priority ("Available provers: " ^ commas (local_provers @ remote_provers) ^
+    Output.urgent_message ("Available provers: " ^ commas (local_provers @ remote_provers) ^
               ".")
   end
 
@@ -481,7 +481,7 @@
       end
     else if blocking then
       let val (success, message) = TimeLimit.timeLimit timeout go () in
-        List.app priority
+        List.app Output.urgent_message
                  (Async_Manager.break_into_chunks [desc ^ "\n" ^ message]);
         (success, state)
       end
@@ -497,7 +497,7 @@
   if null provers then
     error "No prover is set."
   else case subgoal_count state of
-    0 => (priority "No subgoal!"; (false, state))
+    0 => (Output.urgent_message "No subgoal!"; (false, state))
   | n =>
     let
       val _ = Proof.assert_backward state
@@ -505,7 +505,7 @@
       val {context = ctxt, facts = chained_ths, goal} = Proof.goal state
       val (_, hyp_ts, concl_t) = strip_subgoal goal i
       val _ = () |> not blocking ? kill_provers
-      val _ = if auto then () else priority "Sledgehammering..."
+      val _ = if auto then () else Output.urgent_message "Sledgehammering..."
       val (smts, atps) = provers |> List.partition is_smt_prover
       fun run_provers full_types irrelevant_consts relevance_fudge
                       maybe_translate provers (res as (success, state)) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -47,7 +47,7 @@
                explicit_apply timeout i n state axioms =
   let
     val _ =
-      priority ("Testing " ^ n_facts (map fst axioms) ^ "...")
+      Output.urgent_message ("Testing " ^ n_facts (map fst axioms) ^ "...")
     val params =
       {blocking = true, debug = debug, verbose = verbose, overlord = overlord,
        provers = provers, full_types = full_types,
@@ -62,7 +62,7 @@
        axioms = axioms, only = true}
     val result as {outcome, used_axioms, ...} = prover params (K "") problem
   in
-    priority (case outcome of
+    Output.urgent_message (case outcome of
                 SOME failure => string_for_failure failure
               | NONE =>
                 if length used_axioms = length axioms then "Found proof."
@@ -94,7 +94,7 @@
     val thy = Proof.theory_of state
     val prover = get_prover thy false prover_name
     val msecs = Time.toMilliseconds timeout
-    val _ = priority ("Sledgehammer minimize: " ^ quote prover_name ^ ".")
+    val _ = Output.urgent_message ("Sledgehammer minimize: " ^ quote prover_name ^ ".")
     val {goal, ...} = Proof.goal state
     val (_, hyp_ts, concl_t) = strip_subgoal goal i
     val explicit_apply =
@@ -115,7 +115,7 @@
            sublinear_minimize (do_test new_timeout)
                (filter_used_axioms used_axioms axioms) ([], result)
          val n = length min_thms
-         val _ = priority (cat_lines
+         val _ = Output.urgent_message (cat_lines
            ["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^
             (case length (filter (curry (op =) Chained o snd o fst) min_thms) of
                0 => ""
@@ -145,10 +145,10 @@
             o name_thm_pairs_from_ref ctxt reserved chained_ths) refs
   in
     case subgoal_count state of
-      0 => priority "No subgoal!"
+      0 => Output.urgent_message "No subgoal!"
     | n =>
       (kill_provers ();
-       priority (#2 (minimize_facts params i n state axioms)))
+       Output.urgent_message (#2 (minimize_facts params i n state axioms)))
   end
 
 end;
--- a/src/HOL/Tools/async_manager.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/HOL/Tools/async_manager.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -105,7 +105,7 @@
     [] => ()
   | msgs as (tool, _) :: _ =>
     let val ss = break_into_chunks (map snd msgs) in
-      List.app priority (tool ^ ": " ^ hd ss :: tl ss)
+      List.app Output.urgent_message (tool ^ ": " ^ hd ss :: tl ss)
     end
 
 fun check_thread_manager () = Synchronized.change global_state
@@ -185,7 +185,7 @@
                        if tool' = tool then SOME (th, (tool', Time.now (), desc))
                        else NONE) active
       val state' = make_state manager timeout_heap [] (killing @ canceling) messages store;
-      val _ = if null killing then () else priority ("Killed active " ^ workers ^ ".")
+      val _ = if null killing then () else Output.urgent_message ("Killed active " ^ workers ^ ".")
     in state' end);
 
 
@@ -218,7 +218,7 @@
       case map_filter canceling_info canceling of
         [] => []
       | ss => "Trying to interrupt the following " ^ workers ^ ":" :: ss
-  in priority (space_implode "\n\n" (running @ interrupting)) end
+  in Output.urgent_message (space_implode "\n\n" (running @ interrupting)) end
 
 fun thread_messages tool worker opt_limit =
   let
@@ -230,7 +230,7 @@
         (if length tool_store <= limit then ":"
          else " (" ^ string_of_int limit ^ " displayed):");
   in
-    List.app priority (header :: break_into_chunks
+    List.app Output.urgent_message (header :: break_into_chunks
                                      (map snd (#1 (chop limit tool_store))))
   end
 
--- a/src/HOL/Tools/inductive_codegen.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -844,7 +844,7 @@
     val test_fn' = !test_fn;
     val dummy_report = ([], false)
     fun test k = (deepen bound (fn i =>
-      (priority ("Search depth: " ^ string_of_int i);
+      (Output.urgent_message ("Search depth: " ^ string_of_int i);
        test_fn' (i, values, k+offset))) start, dummy_report);
   in test end;
 
--- a/src/HOL/Tools/refute.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/HOL/Tools/refute.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -1133,31 +1133,31 @@
                             ". Available solvers: " ^
                             commas (map (quote o fst) (!SatSolver.solvers)) ^ ".")
           in
-            priority "Invoking SAT solver...";
+            Output.urgent_message "Invoking SAT solver...";
             (case solver fm of
               SatSolver.SATISFIABLE assignment =>
-                (priority ("*** Model found: ***\n" ^ print_model ctxt model
+                (Output.urgent_message ("*** Model found: ***\n" ^ print_model ctxt model
                   (fn i => case assignment i of SOME b => b | NONE => true));
                  if maybe_spurious then "potential" else "genuine")
             | SatSolver.UNSATISFIABLE _ =>
-                (priority "No model exists.";
+                (Output.urgent_message "No model exists.";
                 case next_universe universe sizes minsize maxsize of
                   SOME universe' => find_model_loop universe'
-                | NONE => (priority
-                  "Search terminated, no larger universe within the given limits.";
-                  "none"))
+                | NONE => (Output.urgent_message
+                    "Search terminated, no larger universe within the given limits.";
+                    "none"))
             | SatSolver.UNKNOWN =>
-                (priority "No model found.";
+                (Output.urgent_message "No model found.";
                 case next_universe universe sizes minsize maxsize of
                   SOME universe' => find_model_loop universe'
-                | NONE           => (priority
+                | NONE => (Output.urgent_message
                   "Search terminated, no larger universe within the given limits.";
                   "unknown"))) handle SatSolver.NOT_CONFIGURED =>
               (error ("SAT solver " ^ quote satsolver ^ " is not configured.");
                "unknown")
           end
           handle MAXVARS_EXCEEDED =>
-            (priority ("Search terminated, number of Boolean variables ("
+            (Output.urgent_message ("Search terminated, number of Boolean variables ("
               ^ string_of_int maxvars ^ " allowed) exceeded.");
               "unknown")
 
@@ -1179,14 +1179,14 @@
     maxtime>=0 orelse
       error ("\"maxtime\" is " ^ string_of_int maxtime ^ ", must be at least 0");
     (* enter loop with or without time limit *)
-    priority ("Trying to find a model that "
+    Output.urgent_message ("Trying to find a model that "
       ^ (if negate then "refutes" else "satisfies") ^ ": "
       ^ Syntax.string_of_term ctxt t);
     if maxtime > 0 then (
       TimeLimit.timeLimit (Time.fromSeconds maxtime)
         wrapper ()
       handle TimeLimit.TimeOut =>
-        (priority ("Search terminated, time limit (" ^
+        (Output.urgent_message ("Search terminated, time limit (" ^
             string_of_int maxtime
             ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.");
          check_expect "unknown")
@@ -1273,7 +1273,7 @@
     val t = th |> prop_of
   in
     if Logic.count_prems t = 0 then
-      priority "No subgoal!"
+      Output.urgent_message "No subgoal!"
     else
       let
         val assms = map term_of (Assumption.all_assms_of ctxt)
--- a/src/HOL/Tools/try.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/HOL/Tools/try.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -96,7 +96,7 @@
                                     Pretty.markup Markup.hilite
                                                   [Pretty.str message]])
                     else
-                      tap (fn _ => priority message)))
+                      tap (fn _ => Output.urgent_message message)))
     end
 
 val invoke_try = fst oo do_try false
--- a/src/Pure/General/markup.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/Pure/General/markup.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -120,11 +120,11 @@
   val reportN: string val report: T
   val no_reportN: string val no_report: T
   val badN: string val bad: T
-  val no_output: output * output
-  val default_output: T -> output * output
-  val add_mode: string -> (T -> output * output) -> unit
-  val output: T -> output * output
-  val enclose: T -> output -> output
+  val no_output: Output.output * Output.output
+  val default_output: T -> Output.output * Output.output
+  val add_mode: string -> (T -> Output.output * Output.output) -> unit
+  val output: T -> Output.output * Output.output
+  val enclose: T -> Output.output -> Output.output
   val markup: T -> string -> string
 end;
 
--- a/src/Pure/General/output.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/Pure/General/output.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -6,9 +6,7 @@
 
 signature BASIC_OUTPUT =
 sig
-  type output = string
   val writeln: string -> unit
-  val priority: string -> unit
   val tracing: string -> unit
   val warning: string -> unit
   val legacy_feature: string -> unit
@@ -22,6 +20,7 @@
 signature OUTPUT =
 sig
   include BASIC_OUTPUT
+  type output = string
   val default_output: string -> output * int
   val default_escape: output -> string
   val add_mode: string -> (string -> output * int) -> (output -> string) -> unit
@@ -31,14 +30,18 @@
   val raw_stdout: output -> unit
   val raw_stderr: output -> unit
   val raw_writeln: output -> unit
-  val writeln_fn: (output -> unit) Unsynchronized.ref
-  val priority_fn: (output -> unit) Unsynchronized.ref
-  val tracing_fn: (output -> unit) Unsynchronized.ref
-  val warning_fn: (output -> unit) Unsynchronized.ref
-  val error_fn: (output -> unit) Unsynchronized.ref
-  val prompt_fn: (output -> unit) Unsynchronized.ref
-  val status_fn: (output -> unit) Unsynchronized.ref
-  val report_fn: (output -> unit) Unsynchronized.ref
+  structure Private_Hooks:
+  sig
+    val writeln_fn: (output -> unit) Unsynchronized.ref
+    val urgent_message_fn: (output -> unit) Unsynchronized.ref
+    val tracing_fn: (output -> unit) Unsynchronized.ref
+    val warning_fn: (output -> unit) Unsynchronized.ref
+    val error_fn: (output -> unit) Unsynchronized.ref
+    val prompt_fn: (output -> unit) Unsynchronized.ref
+    val status_fn: (output -> unit) Unsynchronized.ref
+    val report_fn: (output -> unit) Unsynchronized.ref
+  end
+  val urgent_message: string -> unit
   val error_msg: string -> unit
   val prompt: string -> unit
   val status: string -> unit
@@ -85,23 +88,26 @@
 
 (* Isabelle output channels *)
 
-val writeln_fn = Unsynchronized.ref raw_writeln;
-val priority_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
-val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
-val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
-val error_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "*** ");
-val prompt_fn = Unsynchronized.ref raw_stdout;
-val status_fn = Unsynchronized.ref (fn _: string => ());
-val report_fn = Unsynchronized.ref (fn _: string => ());
+structure Private_Hooks =
+struct
+  val writeln_fn = Unsynchronized.ref raw_writeln;
+  val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
+  val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
+  val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
+  val error_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "*** ");
+  val prompt_fn = Unsynchronized.ref raw_stdout;
+  val status_fn = Unsynchronized.ref (fn _: string => ());
+  val report_fn = Unsynchronized.ref (fn _: string => ());
+end;
 
-fun writeln s = ! writeln_fn (output s);
-fun priority s = ! priority_fn (output s);
-fun tracing s = ! tracing_fn (output s);
-fun warning s = ! warning_fn (output s);
-fun error_msg s = ! error_fn (output s);
-fun prompt s = ! prompt_fn (output s);
-fun status s = ! status_fn (output s);
-fun report s = ! report_fn (output s);
+fun writeln s = ! Private_Hooks.writeln_fn (output s);
+fun urgent_message s = ! Private_Hooks.urgent_message_fn (output s);
+fun tracing s = ! Private_Hooks.tracing_fn (output s);
+fun warning s = ! Private_Hooks.warning_fn (output s);
+fun error_msg s = ! Private_Hooks.error_fn (output s);
+fun prompt s = ! Private_Hooks.prompt_fn (output s);
+fun status s = ! Private_Hooks.status_fn (output s);
+fun report s = ! Private_Hooks.report_fn (output s);
 
 fun legacy_feature s = warning ("Legacy feature! " ^ s);
 
--- a/src/Pure/General/pretty.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/Pure/General/pretty.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -21,8 +21,8 @@
 
 signature PRETTY =
 sig
-  val default_indent: string -> int -> output
-  val add_mode: string -> (string -> int -> output) -> unit
+  val default_indent: string -> int -> Output.output
+  val add_mode: string -> (string -> int -> Output.output) -> unit
   type T
   val str: string -> T
   val brk: int -> T
@@ -55,7 +55,7 @@
   val margin_default: int Unsynchronized.ref
   val symbolicN: string
   val output_buffer: int option -> T -> Buffer.T
-  val output: int option -> T -> output
+  val output: int option -> T -> Output.output
   val string_of_margin: int -> T -> string
   val string_of: T -> string
   val str_of: T -> string
@@ -103,9 +103,10 @@
 (** printing items: compound phrases, strings, and breaks **)
 
 abstype T =
-  Block of (output * output) * T list * int * int |  (*markup output, body, indentation, length*)
-  String of output * int |                           (*text, length*)
-  Break of bool * int                                (*mandatory flag, width if not taken*)
+    Block of (Output.output * Output.output) * T list * int * int
+      (*markup output, body, indentation, length*)
+  | String of Output.output * int  (*text, length*)
+  | Break of bool * int  (*mandatory flag, width if not taken*)
 with
 
 fun length (Block (_, _, _, len)) = len
--- a/src/Pure/General/symbol.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/Pure/General/symbol.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -66,7 +66,7 @@
   val bump_string: string -> string
   val length: symbol list -> int
   val xsymbolsN: string
-  val output: string -> output * int
+  val output: string -> Output.output * int
 end;
 
 structure Symbol: SYMBOL =
--- a/src/Pure/General/xml.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/Pure/General/xml.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -16,7 +16,7 @@
   val header: string
   val text: string -> string
   val element: string -> attributes -> string list -> string
-  val output_markup: Markup.T -> output * output
+  val output_markup: Markup.T -> Output.output * Output.output
   val string_of: tree -> string
   val output: tree -> TextIO.outstream -> unit
   val parse_comments: string list -> unit * string list
--- a/src/Pure/Isar/proof.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -972,7 +972,7 @@
       if ! testing then () else Proof_Display.print_results int ctxt res;
     fun print_rule ctxt th =
       if ! testing then rule := SOME th
-      else if int then priority (Proof_Display.string_of_rule ctxt "Successful" th)
+      else if int then Output.urgent_message (Proof_Display.string_of_rule ctxt "Successful" th)
       else ();
     val test_proof =
       try (local_skip_proof true)
--- a/src/Pure/Isar/toplevel.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -231,7 +231,8 @@
     (((fn () => body () handle exn => if Exn.is_interrupt exn then () else reraise exn)
         |> Runtime.debugging
         |> Runtime.toplevel_error
-          (fn exn => priority ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
+          (fn exn =>
+            Output.urgent_message ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
       Simple_Thread.attributes interrupts);
 
 
--- a/src/Pure/Proof/extraction.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/Pure/Proof/extraction.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -119,7 +119,7 @@
 fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs));
 fun corr_name s vs = extr_name s vs ^ "_correctness";
 
-fun msg d s = priority (Symbol.spaces d ^ s);
+fun msg d s = Output.urgent_message (Symbol.spaces d ^ s);
 
 fun vars_of t = map Var (rev (Term.add_vars t []));
 fun frees_of t = map Free (rev (Term.add_frees t []));
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -74,14 +74,14 @@
   | s => Output.raw_writeln (enclose bg en (prefix_lines prfx s)));
 
 fun setup_messages () =
- (Output.writeln_fn := message "" "" "";
-  Output.status_fn := (fn _ => ());
-  Output.report_fn := (fn _ => ());
-  Output.priority_fn := message (special "I") (special "J") "";
-  Output.tracing_fn := message (special "I" ^ special "V") (special "J") "";
-  Output.warning_fn := message (special "K") (special "L") "### ";
-  Output.error_fn := message (special "M") (special "N") "*** ";
-  Output.prompt_fn := (fn s => Output.raw_stdout (render s ^ special "S")));
+ (Output.Private_Hooks.writeln_fn := message "" "" "";
+  Output.Private_Hooks.status_fn := (fn _ => ());
+  Output.Private_Hooks.report_fn := (fn _ => ());
+  Output.Private_Hooks.urgent_message_fn := message (special "I") (special "J") "";
+  Output.Private_Hooks.tracing_fn := message (special "I" ^ special "V") (special "J") "";
+  Output.Private_Hooks.warning_fn := message (special "K") (special "L") "### ";
+  Output.Private_Hooks.error_fn := message (special "M") (special "N") "*** ";
+  Output.Private_Hooks.prompt_fn := (fn s => Output.raw_stdout (render s ^ special "S")));
 
 fun panic s =
   (message (special "M") (special "N") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1);
@@ -146,7 +146,7 @@
 
 (* restart top-level loop (keeps most state information) *)
 
-val welcome = priority o Session.welcome;
+val welcome = Output.urgent_message o Session.welcome;
 
 fun restart () =
  (sync_thy_loader ();
@@ -227,7 +227,7 @@
           Output.default_output Output.default_escape;
          Markup.add_mode ProofGeneralPgip.proof_general_emacsN YXML.output_markup;
          setup_messages ();
-         ProofGeneralPgip.pgip_channel_emacs (! Output.priority_fn);
+         ProofGeneralPgip.pgip_channel_emacs (! Output.Private_Hooks.urgent_message_fn);
          setup_thy_loader ();
          setup_present_hook ();
          initialized := true);
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -160,13 +160,13 @@
    add new lines explicitly in PGIP: they are left implicit.  It means that PGIP messages
    can't be written without newlines. *)
 fun setup_messages () =
- (Output.writeln_fn := (fn s => normalmsg Message s);
-  Output.status_fn := (fn _ => ());
-  Output.report_fn := (fn _ => ());
-  Output.priority_fn := (fn s => normalmsg Status s);
-  Output.tracing_fn := (fn s => normalmsg Tracing s);
-  Output.warning_fn := (fn s => errormsg Message Warning s);
-  Output.error_fn := (fn s => errormsg Message Fatal s));
+ (Output.Private_Hooks.writeln_fn := (fn s => normalmsg Message s);
+  Output.Private_Hooks.status_fn := (fn _ => ());
+  Output.Private_Hooks.report_fn := (fn _ => ());
+  Output.Private_Hooks.urgent_message_fn := (fn s => normalmsg Status s);
+  Output.Private_Hooks.tracing_fn := (fn s => normalmsg Tracing s);
+  Output.Private_Hooks.warning_fn := (fn s => errormsg Message Warning s);
+  Output.Private_Hooks.error_fn := (fn s => errormsg Message Fatal s));
 
 
 (* immediate messages *)
@@ -231,7 +231,7 @@
 
 (* restart top-level loop (keeps most state information) *)
 
-val welcome = priority o Session.welcome;
+val welcome = Output.urgent_message o Session.welcome;
 
 fun restart () =
     (sync_thy_loader ();
@@ -807,14 +807,15 @@
                                 PgipTypes.string_of_pgipurl url)
         | NONE => (openfile_retract filepath;
                    changecwd_dir filedir;
-                   priority ("Working in file: " ^ PgipTypes.string_of_pgipurl url);
+                   Output.urgent_message ("Working in file: " ^ PgipTypes.string_of_pgipurl url);
                    currently_open_file := SOME url)
   end
 
 fun closefile _ =
     case !currently_open_file of
         SOME f => (inform_file_processed f (Isar.state ());
-                   priority ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f);
+                   Output.urgent_message
+                    ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f);
                    currently_open_file := NONE)
       | NONE => raise PGIP ("<closefile> when no file is open!")
 
@@ -835,7 +836,7 @@
 fun abortfile _ =
     case !currently_open_file of
         SOME f => (isarcmd "init_toplevel";
-                   priority ("Aborted working in file: " ^
+                   Output.urgent_message ("Aborted working in file: " ^
                              PgipTypes.string_of_pgipurl f);
                    currently_open_file := NONE)
       | NONE => raise PGIP ("<abortfile> when no file is open!")
@@ -846,7 +847,7 @@
     in
         case !currently_open_file of
             SOME f => raise PGIP ("<retractfile> when a file is open!")
-          | NONE => (priority ("Retracting file: " ^ PgipTypes.string_of_pgipurl url);
+          | NONE => (Output.urgent_message ("Retracting file: " ^ PgipTypes.string_of_pgipurl url);
                      (* TODO: next should be in thy loader, here just for testing *)
                      let
                          val name = thy_name url
--- a/src/Pure/System/isabelle_process.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -57,42 +57,33 @@
 end;
 
 
-(* message markup *)
+(* message channels *)
 
 local
 
-fun chunk s = string_of_int (size s) ^ "\n" ^ s;
+fun chunk s = [string_of_int (size s), "\n", s];
 
 fun message _ _ _ "" = ()
-  | message out_stream ch raw_props body =
+  | message mbox ch raw_props body =
       let
         val robust_props = map (pairself YXML.escape_controls) raw_props;
         val header = YXML.string_of (XML.Elem ((ch, robust_props), []));
-      in TextIO.output (out_stream, chunk header ^ chunk body) (*atomic output!*) end;
+      in Mailbox.send mbox (chunk header @ chunk body) end;
 
-in
-
-fun standard_message out_stream with_serial ch body =
-  message out_stream ch
+fun standard_message mbox with_serial ch body =
+  message mbox ch
     ((if with_serial then cons (Markup.serialN, serial_string ()) else I)
       (Position.properties_of (Position.thread_data ()))) body;
 
-fun init_message out_stream =
-  message out_stream "A" [] (Session.welcome ());
-
-end;
-
-
-(* channels *)
-
-local
-
-fun auto_flush stream =
+fun message_output mbox out_stream =
   let
-    val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream stream, IO.BLOCK_BUF);
-    fun loop () =
-      (OS.Process.sleep (Time.fromMilliseconds 20); try TextIO.flushOut stream; loop ());
-  in loop end;
+    fun loop receive =
+      (case receive mbox of
+        SOME msg =>
+         (List.app (fn s => TextIO.output (out_stream, s)) msg;
+          loop (Mailbox.receive_timeout (Time.fromMilliseconds 20)))
+      | NONE => (try TextIO.flushOut out_stream; loop (SOME o Mailbox.receive)));
+  in fn () => loop (SOME o Mailbox.receive) end;
 
 in
 
@@ -102,19 +93,22 @@
     val in_stream = TextIO.openIn in_fifo;
     val out_stream = TextIO.openOut out_fifo;
 
-    val _ = Simple_Thread.fork false (auto_flush out_stream);
-    val _ = Simple_Thread.fork false (auto_flush TextIO.stdOut);
-    val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr);
+    val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
+    val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
+
+    val mbox = Mailbox.create () : string list Mailbox.T;
+    val _ = Simple_Thread.fork false (message_output mbox out_stream);
   in
-    Output.status_fn   := standard_message out_stream false "B";
-    Output.report_fn   := standard_message out_stream false "C";
-    Output.writeln_fn  := standard_message out_stream true "D";
-    Output.tracing_fn  := standard_message out_stream true "E";
-    Output.warning_fn  := standard_message out_stream true "F";
-    Output.error_fn    := standard_message out_stream true "G";
-    Output.priority_fn := ! Output.writeln_fn;
-    Output.prompt_fn   := ignore;
-    (in_stream, out_stream)
+    Output.Private_Hooks.status_fn := standard_message mbox false "B";
+    Output.Private_Hooks.report_fn := standard_message mbox false "C";
+    Output.Private_Hooks.writeln_fn := standard_message mbox true "D";
+    Output.Private_Hooks.tracing_fn := standard_message mbox true "E";
+    Output.Private_Hooks.warning_fn := standard_message mbox true "F";
+    Output.Private_Hooks.error_fn := standard_message mbox true "G";
+    Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
+    Output.Private_Hooks.prompt_fn := ignore;
+    message mbox "A" [] (Session.welcome ());
+    in_stream
   end;
 
 end;
@@ -179,8 +173,7 @@
     val _ = Unsynchronized.change print_mode
       (fold (update op =) [isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
 
-    val (in_stream, out_stream) = setup_channels in_fifo out_fifo;
-    val _ = init_message out_stream;
+    val in_stream = setup_channels in_fifo out_fifo;
     val _ = Keyword.status ();
     val _ = Output.status (Markup.markup Markup.ready "process ready");
   in loop in_stream end));
--- a/src/Pure/Thy/thy_info.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -141,7 +141,7 @@
   else
     let
       val succs = thy_graph Graph.all_succs [name];
-      val _ = priority (loader_msg "removing" succs);
+      val _ = Output.urgent_message (loader_msg "removing" succs);
       val _ = List.app (perform Remove) succs;
       val _ = change_thys (Graph.del_nodes succs);
     in () end);
@@ -222,7 +222,7 @@
 fun load_thy initiators update_time (deps: deps) text name parent_thys =
   let
     val _ = kill_thy name;
-    val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators);
+    val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
 
     val {master = (thy_path, _), ...} = deps;
     val dir = Path.dir thy_path;
@@ -337,7 +337,7 @@
   in
     NAMED_CRITICAL "Thy_Info" (fn () =>
      (kill_thy name;
-      priority ("Registering theory " ^ quote name);
+      Output.urgent_message ("Registering theory " ^ quote name);
       map get_theory parents;
       change_thys (new_entry name parents (SOME deps, SOME theory));
       perform Update name))
--- a/src/Pure/Thy/thy_syntax.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -10,7 +10,7 @@
     (Token.T, (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, 'a)
       Source.source) Source.source) Source.source) Source.source
   val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
-  val present_token: Token.T -> output
+  val present_token: Token.T -> Output.output
   val report_token: Token.T -> unit
   datatype span_kind = Command of string | Ignored | Malformed
   type span
@@ -19,7 +19,7 @@
   val span_range: span -> Position.range
   val span_source: (Token.T, 'a) Source.source -> (span, (Token.T, 'a) Source.source) Source.source
   val parse_spans: Scan.lexicon * Scan.lexicon -> Position.T -> string -> span list
-  val present_span: span -> output
+  val present_span: span -> Output.output
   val report_span: span -> unit
   val atom_source: (span, 'a) Source.source ->
     (span * span list * bool, (span, 'a) Source.source) Source.source
--- a/src/Tools/quickcheck.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/Tools/quickcheck.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -188,8 +188,10 @@
           case iterate (fn () => tester (k - 1)) i empty_report
            of (NONE, report) => apsnd (cons report) (with_testers k testers)
             | (SOME q, report) => (SOME q, [report]);
-    fun with_size k reports = if k > size then (NONE, reports)
-      else (if quiet then () else priority ("Test data size: " ^ string_of_int k);
+    fun with_size k reports =
+      if k > size then (NONE, reports)
+      else
+       (if quiet then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
         let
           val (result, new_report) = with_testers k testers
           val reports = ((k, new_report) :: reports)
--- a/src/Tools/solve_direct.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/Tools/solve_direct.ML	Tue Oct 26 11:06:12 2010 +0200
@@ -84,7 +84,7 @@
                    Pretty.markup Markup.hilite (message results)])
             else
               tap (fn _ =>
-                priority (Pretty.string_of (Pretty.chunks (message results))))))
+                Output.urgent_message (Pretty.string_of (Pretty.chunks (message results))))))
     | _ => (false, state))
   end;