renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
--- a/src/HOL/Mutabelle/MutabelleExtra.thy Mon Oct 25 20:24:13 2010 +0200
+++ b/src/HOL/Mutabelle/MutabelleExtra.thy Mon Oct 25 21:06:56 2010 +0200
@@ -21,7 +21,7 @@
ML {* val old_tr = !Output.tracing_fn *}
ML {* val old_wr = !Output.writeln_fn *}
-ML {* val old_pr = !Output.priority_fn *}
+ML {* val old_ur = !Output.urgent_message_fn *}
ML {* val old_wa = !Output.warning_fn *}
quickcheck_params [size = 5, iterations = 1000]
@@ -50,7 +50,7 @@
ML {* Output.tracing_fn := old_tr *}
ML {* Output.writeln_fn := old_wr *}
-ML {* Output.priority_fn := old_pr *}
+ML {* Output.urgent_message_fn := old_ur *}
ML {* Output.warning_fn := old_wa *}
end
--- a/src/HOL/Mutabelle/mutabelle.ML Mon Oct 25 20:24:13 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle.ML Mon Oct 25 21:06:56 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 Mon Oct 25 20:24:13 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Mon Oct 25 21:06:56 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 Mon Oct 25 20:24:13 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Oct 25 21:06:56 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 Mon Oct 25 20:24:13 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Oct 25 21:06:56 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 Mon Oct 25 20:24:13 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Oct 25 21:06:56 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 Mon Oct 25 20:24:13 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Mon Oct 25 21:06:56 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 Mon Oct 25 20:24:13 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Oct 25 21:06:56 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 Mon Oct 25 20:24:13 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Oct 25 21:06:56 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 Mon Oct 25 20:24:13 2010 +0200
+++ b/src/HOL/Tools/async_manager.ML Mon Oct 25 21:06:56 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 Mon Oct 25 20:24:13 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Mon Oct 25 21:06:56 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 Mon Oct 25 20:24:13 2010 +0200
+++ b/src/HOL/Tools/refute.ML Mon Oct 25 21:06:56 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 Mon Oct 25 20:24:13 2010 +0200
+++ b/src/HOL/Tools/try.ML Mon Oct 25 21:06:56 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/output.ML Mon Oct 25 20:24:13 2010 +0200
+++ b/src/Pure/General/output.ML Mon Oct 25 21:06:56 2010 +0200
@@ -7,7 +7,6 @@
signature BASIC_OUTPUT =
sig
val writeln: string -> unit
- val priority: string -> unit
val tracing: string -> unit
val warning: string -> unit
val legacy_feature: string -> unit
@@ -32,13 +31,14 @@
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 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
+ val urgent_message: string -> unit
val error_msg: string -> unit
val prompt: string -> unit
val status: string -> unit
@@ -86,7 +86,7 @@
(* Isabelle output channels *)
val writeln_fn = Unsynchronized.ref raw_writeln;
-val priority_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
+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 "*** ");
@@ -95,7 +95,7 @@
val report_fn = Unsynchronized.ref (fn _: string => ());
fun writeln s = ! writeln_fn (output s);
-fun priority s = ! priority_fn (output s);
+fun urgent_message s = ! urgent_message_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);
--- a/src/Pure/Isar/proof.ML Mon Oct 25 20:24:13 2010 +0200
+++ b/src/Pure/Isar/proof.ML Mon Oct 25 21:06:56 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 Mon Oct 25 20:24:13 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Mon Oct 25 21:06:56 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 Mon Oct 25 20:24:13 2010 +0200
+++ b/src/Pure/Proof/extraction.ML Mon Oct 25 21:06:56 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 Mon Oct 25 20:24:13 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Mon Oct 25 21:06:56 2010 +0200
@@ -77,7 +77,7 @@
(Output.writeln_fn := message "" "" "";
Output.status_fn := (fn _ => ());
Output.report_fn := (fn _ => ());
- Output.priority_fn := message (special "I") (special "J") "";
+ Output.urgent_message_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") "*** ";
@@ -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.urgent_message_fn);
setup_thy_loader ();
setup_present_hook ();
initialized := true);
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Oct 25 20:24:13 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Oct 25 21:06:56 2010 +0200
@@ -163,7 +163,7 @@
(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.urgent_message_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));
@@ -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 Mon Oct 25 20:24:13 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML Mon Oct 25 21:06:56 2010 +0200
@@ -106,14 +106,14 @@
val _ = Simple_Thread.fork false (auto_flush TextIO.stdOut);
val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr);
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;
+ 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.urgent_message_fn := ! Output.writeln_fn;
+ Output.prompt_fn := ignore;
(in_stream, out_stream)
end;
--- a/src/Pure/Thy/thy_info.ML Mon Oct 25 20:24:13 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML Mon Oct 25 21:06:56 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/Tools/quickcheck.ML Mon Oct 25 20:24:13 2010 +0200
+++ b/src/Tools/quickcheck.ML Mon Oct 25 21:06:56 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 Mon Oct 25 20:24:13 2010 +0200
+++ b/src/Tools/solve_direct.ML Mon Oct 25 21:06:56 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;