# HG changeset patch # User wenzelm # Date 1288083972 -7200 # Node ID 8728165d366e7278b034805c2b706a2fec350e71 # Parent d170c322157ad96d524e51ac020005c3f8abd77f# Parent 8baded087d342eaf5b7617ddf3698987935e556d merged diff -r d170c322157a -r 8728165d366e src/HOL/Mutabelle/MutabelleExtra.thy --- 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 diff -r d170c322157a -r 8728165d366e src/HOL/Mutabelle/mutabelle.ML --- 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 diff -r d170c322157a -r 8728165d366e src/HOL/Mutabelle/mutabelle_extra.ML --- 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)*) diff -r d170c322157a -r 8728165d366e src/HOL/Tools/Nitpick/nitpick.ML --- 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 diff -r d170c322157a -r 8728165d366e src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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 () diff -r d170c322157a -r 8728165d366e src/HOL/Tools/Nitpick/nitpick_model.ML --- 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 () diff -r d170c322157a -r 8728165d366e src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- 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) diff -r d170c322157a -r 8728165d366e src/HOL/Tools/Sledgehammer/sledgehammer.ML --- 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)) = diff -r d170c322157a -r 8728165d366e src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- 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; diff -r d170c322157a -r 8728165d366e src/HOL/Tools/async_manager.ML --- 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 diff -r d170c322157a -r 8728165d366e src/HOL/Tools/inductive_codegen.ML --- 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; diff -r d170c322157a -r 8728165d366e src/HOL/Tools/refute.ML --- 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) diff -r d170c322157a -r 8728165d366e src/HOL/Tools/try.ML --- 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 diff -r d170c322157a -r 8728165d366e src/Pure/General/markup.ML --- 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; diff -r d170c322157a -r 8728165d366e src/Pure/General/output.ML --- 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); diff -r d170c322157a -r 8728165d366e src/Pure/General/pretty.ML --- 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 diff -r d170c322157a -r 8728165d366e src/Pure/General/symbol.ML --- 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 = diff -r d170c322157a -r 8728165d366e src/Pure/General/xml.ML --- 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 diff -r d170c322157a -r 8728165d366e src/Pure/Isar/proof.ML --- 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) diff -r d170c322157a -r 8728165d366e src/Pure/Isar/toplevel.ML --- 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); diff -r d170c322157a -r 8728165d366e src/Pure/Proof/extraction.ML --- 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 [])); diff -r d170c322157a -r 8728165d366e src/Pure/ProofGeneral/proof_general_emacs.ML --- 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); diff -r d170c322157a -r 8728165d366e src/Pure/ProofGeneral/proof_general_pgip.ML --- 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 (" 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 d170c322157a -r 8728165d366e src/Pure/System/isabelle_process.ML --- 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)); diff -r d170c322157a -r 8728165d366e src/Pure/Thy/thy_info.ML --- 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)) diff -r d170c322157a -r 8728165d366e src/Pure/Thy/thy_syntax.ML --- 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 diff -r d170c322157a -r 8728165d366e src/Tools/quickcheck.ML --- 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) diff -r d170c322157a -r 8728165d366e src/Tools/solve_direct.ML --- 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;