# HG changeset patch # User wenzelm # Date 1288033616 -7200 # Node ID 7ee65dbffa31690284584809e2d202eee96df077 # Parent 7cbebd636e79aaee14abec88fb87122d6c0027b6 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly; diff -r 7cbebd636e79 -r 7ee65dbffa31 src/HOL/Mutabelle/MutabelleExtra.thy --- 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 diff -r 7cbebd636e79 -r 7ee65dbffa31 src/HOL/Mutabelle/mutabelle.ML --- 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 diff -r 7cbebd636e79 -r 7ee65dbffa31 src/HOL/Mutabelle/mutabelle_extra.ML --- 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)*) diff -r 7cbebd636e79 -r 7ee65dbffa31 src/HOL/Tools/Nitpick/nitpick.ML --- 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 diff -r 7cbebd636e79 -r 7ee65dbffa31 src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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 () diff -r 7cbebd636e79 -r 7ee65dbffa31 src/HOL/Tools/Nitpick/nitpick_model.ML --- 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 () diff -r 7cbebd636e79 -r 7ee65dbffa31 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- 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) diff -r 7cbebd636e79 -r 7ee65dbffa31 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- 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)) = diff -r 7cbebd636e79 -r 7ee65dbffa31 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- 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; diff -r 7cbebd636e79 -r 7ee65dbffa31 src/HOL/Tools/async_manager.ML --- 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 diff -r 7cbebd636e79 -r 7ee65dbffa31 src/HOL/Tools/inductive_codegen.ML --- 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; diff -r 7cbebd636e79 -r 7ee65dbffa31 src/HOL/Tools/refute.ML --- 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) diff -r 7cbebd636e79 -r 7ee65dbffa31 src/HOL/Tools/try.ML --- 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 diff -r 7cbebd636e79 -r 7ee65dbffa31 src/Pure/General/output.ML --- 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); diff -r 7cbebd636e79 -r 7ee65dbffa31 src/Pure/Isar/proof.ML --- 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) diff -r 7cbebd636e79 -r 7ee65dbffa31 src/Pure/Isar/toplevel.ML --- 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); diff -r 7cbebd636e79 -r 7ee65dbffa31 src/Pure/Proof/extraction.ML --- 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 [])); diff -r 7cbebd636e79 -r 7ee65dbffa31 src/Pure/ProofGeneral/proof_general_emacs.ML --- 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); diff -r 7cbebd636e79 -r 7ee65dbffa31 src/Pure/ProofGeneral/proof_general_pgip.ML --- 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 (" 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 (" when no file is open!") @@ -846,7 +847,7 @@ in case !currently_open_file of SOME f => raise PGIP (" 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 diff -r 7cbebd636e79 -r 7ee65dbffa31 src/Pure/System/isabelle_process.ML --- 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; diff -r 7cbebd636e79 -r 7ee65dbffa31 src/Pure/Thy/thy_info.ML --- 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)) diff -r 7cbebd636e79 -r 7ee65dbffa31 src/Tools/quickcheck.ML --- 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) diff -r 7cbebd636e79 -r 7ee65dbffa31 src/Tools/solve_direct.ML --- 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;