--- a/src/HOL/Library/refute.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Library/refute.ML Fri Oct 31 11:36:41 2014 +0100
@@ -1068,31 +1068,31 @@
". Available solvers: " ^
commas (map (quote o fst) (SAT_Solver.get_solvers ())) ^ ".")
in
- Output.urgent_message "Invoking SAT solver...";
+ writeln "Invoking SAT solver...";
(case solver fm of
SAT_Solver.SATISFIABLE assignment =>
- (Output.urgent_message ("Model found:\n" ^ print_model ctxt model
+ (writeln ("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")
| SAT_Solver.UNSATISFIABLE _ =>
- (Output.urgent_message "No model exists.";
+ (writeln "No model exists.";
case next_universe universe sizes minsize maxsize of
SOME universe' => find_model_loop universe'
- | NONE => (Output.urgent_message
+ | NONE => (writeln
"Search terminated, no larger universe within the given limits.";
"none"))
| SAT_Solver.UNKNOWN =>
- (Output.urgent_message "No model found.";
+ (writeln "No model found.";
case next_universe universe sizes minsize maxsize of
SOME universe' => find_model_loop universe'
- | NONE => (Output.urgent_message
+ | NONE => (writeln
"Search terminated, no larger universe within the given limits.";
"unknown"))) handle SAT_Solver.NOT_CONFIGURED =>
(error ("SAT solver " ^ quote satsolver ^ " is not configured.");
"unknown")
end
handle MAXVARS_EXCEEDED =>
- (Output.urgent_message ("Search terminated, number of Boolean variables ("
+ (writeln ("Search terminated, number of Boolean variables ("
^ string_of_int maxvars ^ " allowed) exceeded.");
"unknown")
@@ -1114,14 +1114,14 @@
maxtime>=0 orelse
error ("\"maxtime\" is " ^ string_of_int maxtime ^ ", must be at least 0");
(* enter loop with or without time limit *)
- Output.urgent_message ("Trying to find a model that "
+ writeln ("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 =>
- (Output.urgent_message ("Search terminated, time limit (" ^
+ (writeln ("Search terminated, time limit (" ^
string_of_int maxtime
^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.");
check_expect "unknown")
@@ -1207,7 +1207,7 @@
val t = th |> prop_of
in
if Logic.count_prems t = 0 then
- (Output.urgent_message "No subgoal!"; "none")
+ (writeln "No subgoal!"; "none")
else
let
val assms = map term_of (Assumption.all_assms_of ctxt)
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Oct 31 11:36:41 2014 +0100
@@ -428,7 +428,7 @@
|> tap (fn factss =>
"Line " ^ str0 (Position.line_of pos) ^ ": " ^
Sledgehammer.string_of_factss factss
- |> Output.urgent_message)
+ |> writeln)
val prover = get_prover ctxt prover_name params goal facts
val problem =
{comment = "", state = st', goal = goal, subgoal = i,
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Oct 31 11:36:41 2014 +0100
@@ -171,7 +171,7 @@
let
val params = []
val res = Refute.refute_term (Proof_Context.init_global thy) params [] t
- val _ = Output.urgent_message ("Refute: " ^ res)
+ val _ = writeln ("Refute: " ^ res)
in
(rpair []) (case res of
"genuine" => GenuineCex
@@ -194,7 +194,7 @@
val state = Proof.init ctxt
val (res, _) = Nitpick.pick_nits_in_term state
(Nitpick_Commands.default_params thy []) Nitpick.Normal 1 1 1 [] [] [] t
- val _ = Output.urgent_message ("Nitpick: " ^ res)
+ val _ = writeln ("Nitpick: " ^ res)
in
(rpair []) (case res of
"genuine" => GenuineCex
@@ -343,21 +343,21 @@
(*
fun unsafe_invoke_mtd thy (mtd_name, invoke_mtd) t =
let
- val _ = Output.urgent_message ("Invoking " ^ mtd_name)
+ val _ = writeln ("Invoking " ^ mtd_name)
val ((res, (timing, reports)), time) = cpu_time "total time" (fn () => invoke_mtd thy t
handle ERROR s => (tracing s; (Error, ([], NONE))))
- val _ = Output.urgent_message (" Done")
+ val _ = writeln (" Done")
in (res, (time :: timing, reports)) end
*)
fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t =
let
- val _ = Output.urgent_message ("Invoking " ^ mtd_name)
+ val _ = writeln ("Invoking " ^ mtd_name)
val (res, timing) = elapsed_time "total time"
(fn () => case try (invoke_mtd thy) t of
SOME (res, _) => res
- | NONE => (Output.urgent_message ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
+ | NONE => (writeln ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
Error))
- val _ = Output.urgent_message (" Done")
+ val _ = writeln (" Done")
in (res, [timing]) end
(* creating entries *)
@@ -387,7 +387,7 @@
val mutants =
if exec then
let
- val _ = Output.urgent_message ("BEFORE PARTITION OF " ^
+ val _ = writeln ("BEFORE PARTITION OF " ^
string_of_int (length mutants) ^ " MUTANTS")
val (execs, noexecs) = List.partition (is_executable_term thy) (take_random (20 * max_mutants) mutants)
val _ = tracing ("AFTER PARTITION (" ^ string_of_int (length execs) ^
@@ -404,7 +404,7 @@
|> filter (is_some o try (Thm.cterm_of thy))
|> filter (is_some o try (Syntax.check_term (Proof_Context.init_global thy)))
|> take_random max_mutants
- val _ = map (fn t => Output.urgent_message ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
+ val _ = map (fn t => writeln ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
in
create_entry thy thm exec mutants mtds
end
@@ -458,7 +458,7 @@
(* theory -> mtd list -> thm list -> string -> unit *)
fun mutate_theorems_and_write_report thy (num_mutations, max_mutants) mtds thms file_name =
let
- val _ = Output.urgent_message "Starting Mutabelle..."
+ val _ = writeln "Starting Mutabelle..."
val ctxt = Proof_Context.init_global thy
val path = Path.explode file_name
(* for normal report: *)
--- a/src/HOL/TPTP/atp_problem_import.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML Fri Oct 31 11:36:41 2014 +0100
@@ -117,7 +117,7 @@
if falsify then "CounterSatisfiable" else "Satisfiable"
else
"Unknown")
- |> Output.urgent_message
+ |> writeln
val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy snd file_name
val params =
[("maxtime", string_of_int timeout),
@@ -135,7 +135,7 @@
fun SOLVE_TIMEOUT seconds name tac st =
let
- val _ = Output.urgent_message ("running " ^ name ^ " for " ^ string_of_int seconds ^ " s")
+ val _ = writeln ("running " ^ name ^ " for " ^ string_of_int seconds ^ " s")
val result =
TimeLimit.timeLimit (Time.fromSeconds seconds) (fn () => SINGLE (SOLVE tac) st) ()
handle
@@ -143,8 +143,8 @@
| ERROR _ => NONE
in
(case result of
- NONE => (Output.urgent_message ("FAILURE: " ^ name); Seq.empty)
- | SOME st' => (Output.urgent_message ("SUCCESS: " ^ name); Seq.single st'))
+ NONE => (writeln ("FAILURE: " ^ name); Seq.empty)
+ | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st'))
end
fun nitpick_finite_oracle_tac ctxt timeout i th =
@@ -264,7 +264,7 @@
Logic.list_implies (rev defs @ rev nondefs, case conjs of conj :: _ => conj | [] => @{prop False})
fun print_szs_of_success conjs success =
- Output.urgent_message ("% SZS status " ^
+ writeln ("% SZS status " ^
(if success then
if null conjs then "Unsatisfiable" else "Theorem"
else
--- a/src/HOL/Tools/Nitpick/nitpick.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Oct 31 11:36:41 2014 +0100
@@ -241,11 +241,11 @@
o Pretty.mark Markup.information
else
print o Pretty.string_of
- val pprint_a = pprint Output.urgent_message
- fun pprint_nt f = () |> is_mode_nt mode ? pprint Output.urgent_message o f
- fun pprint_v f = () |> verbose ? pprint Output.urgent_message o f
+ val pprint_a = pprint writeln
+ fun pprint_nt f = () |> is_mode_nt mode ? pprint writeln o f
+ fun pprint_v f = () |> verbose ? pprint writeln o f
fun pprint_d f = () |> debug ? pprint tracing o f
- val print = pprint Output.urgent_message o curry Pretty.blk 0 o pstrs
+ val print = pprint writeln o curry Pretty.blk 0 o pstrs
fun print_t f = () |> mode = TPTP ? print o f
(*
val print_g = pprint tracing o Pretty.str
@@ -1015,8 +1015,8 @@
fun pick_nits_in_term state (params as {timeout, expect, ...}) mode i n step
subst def_assm_ts nondef_assm_ts orig_t =
let
- val print_nt = if is_mode_nt mode then Output.urgent_message else K ()
- val print_t = if mode = TPTP then Output.urgent_message else K ()
+ val print_nt = if is_mode_nt mode then writeln else K ()
+ val print_t = if mode = TPTP then writeln else K ()
in
if getenv "KODKODI" = "" then
(* The "expect" argument is deliberately ignored if Kodkodi is missing so
@@ -1068,7 +1068,7 @@
val t = state |> Proof.raw_goal |> #goal |> prop_of
in
case Logic.count_prems t of
- 0 => (Output.urgent_message "No subgoal!"; (noneN, state))
+ 0 => (writeln "No subgoal!"; (noneN, state))
| n =>
let
val t = Logic.goal_params t i |> fst
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Oct 31 11:36:41 2014 +0100
@@ -2140,8 +2140,7 @@
map (wf_constraint_for_triple rel) triples
|> foldr1 s_conj |> HOLogic.mk_Trueprop
val _ = if debug then
- Output.urgent_message ("Wellfoundedness goal: " ^
- Syntax.string_of_term ctxt prop ^ ".")
+ writeln ("Wellfoundedness goal: " ^ Syntax.string_of_term ctxt prop ^ ".")
else
()
in
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Oct 31 11:36:41 2014 +0100
@@ -1059,7 +1059,7 @@
if debug then
(if negate then "Genuineness" else "Spuriousness") ^ " goal: " ^
Syntax.string_of_term ctxt prop ^ "."
- |> Output.urgent_message
+ |> writeln
else
()
val goal = prop |> cterm_of thy |> Goal.init
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Oct 31 11:36:41 2014 +0100
@@ -360,7 +360,7 @@
fun try_upto_depth ctxt f =
let
val max_depth = Config.get ctxt Quickcheck.depth
- fun message s = if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message s
+ fun message s = if Config.get ctxt Quickcheck.quiet then () else writeln s
fun try' i =
if i <= max_depth then
let
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Oct 31 11:36:41 2014 +0100
@@ -221,8 +221,8 @@
fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code_modules, _) =
let
val ((is_genuine, counterexample_of), (get, put, put_ml)) = cookie
- fun message s = if quiet then () else Output.urgent_message s
- fun verbose_message s = if not quiet andalso verbose then Output.urgent_message s else ()
+ fun message s = if quiet then () else writeln s
+ fun verbose_message s = if not quiet andalso verbose then writeln s else ()
val current_size = Unsynchronized.ref 0
val current_result = Unsynchronized.ref Quickcheck.empty_result
val tmp_prefix = "Quickcheck_Narrowing"
@@ -511,7 +511,7 @@
(maps (map snd) correct_inst_goals) []
end
else
- (if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message
+ (if Config.get ctxt Quickcheck.quiet then () else writeln
("Environment variable ISABELLE_GHC is not set. To use narrowing-based quickcheck, please set "
^ "this variable to your GHC Haskell compiler in your settings file. "
^ "To deactivate narrowing-based quickcheck, set quickcheck_narrowing_active to false.");
--- a/src/HOL/Tools/Sledgehammer/async_manager.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/async_manager.ML Fri Oct 31 11:36:41 2014 +0100
@@ -106,7 +106,7 @@
tool ^ ": " ^
implode_message (workers |> sort_distinct string_ord, work)
|> break_into_chunks
- |> List.app Output.urgent_message)
+ |> List.app writeln)
fun check_thread_manager () = Synchronized.change global_state
(fn state as {manager, timeout_heap, active, canceling, messages, store} =>
@@ -178,7 +178,7 @@
val state' = make_state manager timeout_heap [] (killing @ canceling) messages store
val _ =
if null killing then ()
- else Output.urgent_message ("Interrupted active " ^ das_wort_worker ^ "s.")
+ else writeln ("Interrupted active " ^ das_wort_worker ^ "s.")
in state' end)
fun str_of_time time = string_of_int (Time.toSeconds time) ^ " s"
@@ -210,7 +210,7 @@
case map_filter canceling_info canceling of
[] => []
| ss => "Interrupting " ^ das_wort_worker ^ "s" :: ss
- in Output.urgent_message (space_implode "\n\n" (running @ interrupting)) end
+ in writeln (space_implode "\n\n" (running @ interrupting)) end
fun thread_messages tool das_wort_worker opt_limit =
let
@@ -222,6 +222,6 @@
(if length tool_store <= limit then ":"
else " (" ^ string_of_int limit ^ " displayed):")
val ss = tool_store |> chop limit |> #1 |> map (op ^ o snd)
- in List.app Output.urgent_message (header :: maps break_into_chunks ss) end
+ in List.app writeln (header :: maps break_into_chunks ss) end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 31 11:36:41 2014 +0100
@@ -137,7 +137,7 @@
|> commas
|> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
" proof (of " ^ string_of_int (length facts) ^ "): ") "."
- |> Output.urgent_message
+ |> writeln
fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) =
let
@@ -230,7 +230,7 @@
else
outcome
|> Async_Manager.break_into_chunks
- |> List.app Output.urgent_message
+ |> List.app writeln
in (outcome_code, state) end
else
(Async_Manager.thread SledgehammerN birth_time death_time
@@ -259,12 +259,12 @@
else
(case subgoal_count state of
0 =>
- ((if blocking then error else Output.urgent_message) "No subgoal!"; (false, (noneN, state)))
+ ((if blocking then error else writeln) "No subgoal!"; (false, (noneN, state)))
| n =>
let
val _ = Proof.assert_backward state
val print =
- if mode = Normal andalso is_none output_result then Output.urgent_message else K ()
+ if mode = Normal andalso is_none output_result then writeln else K ()
val ctxt = Proof.context_of state
val {facts = chained, goal, ...} = Proof.goal state
val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Oct 31 11:36:41 2014 +0100
@@ -150,7 +150,7 @@
fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
(one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) =
let
- val _ = if debug then Output.urgent_message "Constructing Isar proof..." else ()
+ val _ = if debug then writeln "Constructing Isar proof..." else ()
fun generate_proof_text () =
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Oct 31 11:36:41 2014 +0100
@@ -1016,7 +1016,7 @@
val num_isar_deps = length isar_deps
in
if verbose andalso auto_level = 0 then
- Output.urgent_message ("MaSh: " ^ quote prover ^ " on " ^ quote name ^ " with " ^
+ writeln ("MaSh: " ^ quote prover ^ " on " ^ quote name ^ " with " ^
string_of_int num_isar_deps ^ " + " ^ string_of_int (length facts - num_isar_deps) ^
" facts.")
else
@@ -1025,7 +1025,7 @@
{outcome = NONE, used_facts, ...} =>
(if verbose andalso auto_level = 0 then
let val num_facts = length used_facts in
- Output.urgent_message ("Found proof with " ^ string_of_int num_facts ^ " fact" ^
+ writeln ("Found proof with " ^ string_of_int num_facts ^ " fact" ^
plural_s num_facts ^ ".")
end
else
@@ -1212,7 +1212,7 @@
|> pairself (map fact_of_raw_fact)
end
-fun mash_unlearn () = (clear_state (); Output.urgent_message "Reset MaSh.")
+fun mash_unlearn () = (clear_state (); writeln "Reset MaSh.")
fun learn_wrt_access_graph ctxt (name, parents, feats, deps)
(accum as (access_G, (fact_xtab, feat_xtab))) =
@@ -1361,11 +1361,11 @@
end
fun commit last learns relearns flops =
- (if debug andalso auto_level = 0 then Output.urgent_message "Committing..." else ();
+ (if debug andalso auto_level = 0 then writeln "Committing..." else ();
map_state ctxt (do_commit (rev learns) relearns flops);
if not last andalso auto_level = 0 then
let val num_proofs = length learns + length relearns in
- Output.urgent_message ("Learned " ^ string_of_int num_proofs ^ " " ^
+ writeln ("Learned " ^ string_of_int num_proofs ^ " " ^
(if run_prover then "automatic" else "Isar") ^ " proof" ^
plural_s num_proofs ^ " in the last " ^ string_of_time commit_timeout ^ ".")
end
@@ -1474,18 +1474,18 @@
fun learn auto_level run_prover =
mash_learn_facts ctxt params prover auto_level run_prover one_year facts
- |> Output.urgent_message
+ |> writeln
in
if run_prover then
- (Output.urgent_message ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
+ (writeln ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
plural_s num_facts ^ " for automatic proofs (" ^ quote prover ^ " timeout: " ^
string_of_time timeout ^ ").\n\nCollecting Isar proofs first...");
learn 1 false;
- Output.urgent_message "Now collecting automatic proofs. This may take several hours. You \
+ writeln "Now collecting automatic proofs. This may take several hours. You \
\can safely stop the learning process at any point.";
learn 0 true)
else
- (Output.urgent_message ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
+ (writeln ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
plural_s num_facts ^ " for Isar proofs...");
learn 0 false)
end
@@ -1522,7 +1522,7 @@
Time.toSeconds timeout >= min_secs_for_learning then
let val timeout = time_mult learn_timeout_slack timeout in
(if verbose then
- Output.urgent_message ("Started MaShing through " ^
+ writeln ("Started MaShing through " ^
(if exact then "" else "at least ") ^ string_of_int min_num_facts_to_learn ^
" fact" ^ plural_s min_num_facts_to_learn ^ " in the background.")
else
@@ -1545,7 +1545,7 @@
| num_facts_to_learn =>
if num_facts_to_learn <= max_facts_to_learn_before_query then
mash_learn_facts ctxt params prover 2 false timeout facts
- |> (fn "" => () | s => Output.urgent_message (MaShN ^ ": " ^ s))
+ |> (fn "" => () | s => writeln (MaShN ^ ": " ^ s))
else
maybe_launch_thread true num_facts_to_learn)
else
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Oct 31 11:36:41 2014 +0100
@@ -198,7 +198,7 @@
sort_strings (supported_atps thy) @ sort_strings (SMT_Config.available_solvers_of ctxt)
|> List.partition (String.isPrefix remote_prefix)
in
- Output.urgent_message ("Supported provers: " ^ commas (local_provers @ remote_provers) ^ ".")
+ writeln ("Supported provers: " ^ commas (local_provers @ remote_provers) ^ ".")
end
fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Oct 31 11:36:41 2014 +0100
@@ -250,7 +250,7 @@
quote name ^ " slice #" ^ string_of_int (slice + 1) ^
" with " ^ string_of_int num_facts ^ " fact" ^
plural_s num_facts ^ " for " ^ string_of_time slice_timeout ^ "..."
- |> Output.urgent_message
+ |> writeln
else
()
val readable_names = not (Config.get ctxt atp_full_names)
@@ -370,7 +370,7 @@
(used_facts, preferred_methss,
fn preplay =>
let
- val _ = if verbose then Output.urgent_message "Generating proof text..." else ()
+ val _ = if verbose then writeln "Generating proof text..." else ()
fun isar_params () =
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Oct 31 11:36:41 2014 +0100
@@ -76,7 +76,7 @@
(if n > 0 then ": " ^ (names |> map fst |> sort string_ord |> space_implode " ") else "")
end
-fun print silent f = if silent then () else Output.urgent_message (f ())
+fun print silent f = if silent then () else writeln (f ())
fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Fri Oct 31 11:36:41 2014 +0100
@@ -113,7 +113,7 @@
if debug then
quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^
" fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout
- |> Output.urgent_message
+ |> writeln
else
()
val birth = Timer.checkRealTimer timer
@@ -163,7 +163,7 @@
string_of_atp_failure (failure_of_smt_failure (the outcome)) ^
" Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
"..."
- |> Output.urgent_message
+ |> writeln
else
()
in
@@ -204,7 +204,7 @@
(preferred_methss,
fn preplay =>
let
- val _ = if verbose then Output.urgent_message "Generating proof text..." else ()
+ val _ = if verbose then writeln "Generating proof text..." else ()
fun isar_params () =
(verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (),
--- a/src/HOL/Tools/try0.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/Tools/try0.ML Fri Oct 31 11:36:41 2014 +0100
@@ -124,12 +124,12 @@
if mode = Normal then
"Trying " ^ space_implode " " (Try.serial_commas "and" (map (quote o fst) named_methods)) ^
"..."
- |> Output.urgent_message
+ |> writeln
else
();
(case par_map (fn f => f mode timeout_opt quad st) apply_methods of
[] =>
- (if mode = Normal then Output.urgent_message "No proof found." else (); (false, (noneN, st)))
+ (if mode = Normal then writeln "No proof found." else (); (false, (noneN, st)))
| xs as (name, command, _) :: _ =>
let
val xs = xs |> map (fn (name, _, n) => (n, name))
@@ -152,7 +152,7 @@
|> (if mode = Auto_Try then
Proof.goal_message (fn () => Pretty.markup Markup.information [Pretty.str message])
else
- tap (fn _ => Output.urgent_message message))))
+ tap (fn _ => writeln message))))
end)
end;
--- a/src/Pure/General/output.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/Pure/General/output.ML Fri Oct 31 11:36:41 2014 +0100
@@ -26,7 +26,6 @@
val physical_writeln: output -> unit
exception Protocol_Message of Properties.T
val writelns: string list -> unit
- val urgent_message: string -> unit
val error_message': serial * string -> unit
val error_message: string -> unit
val system_message: string -> unit
@@ -42,7 +41,6 @@
sig
include OUTPUT
val writeln_fn: (output list -> unit) Unsynchronized.ref
- val urgent_message_fn: (output list -> unit) Unsynchronized.ref
val tracing_fn: (output list -> unit) Unsynchronized.ref
val warning_fn: (output list -> unit) Unsynchronized.ref
val error_message_fn: (serial * output list -> unit) Unsynchronized.ref
@@ -98,7 +96,6 @@
exception Protocol_Message of Properties.T;
val writeln_fn = Unsynchronized.ref (physical_writeln o implode);
-val urgent_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss); (*Proof General legacy*)
val tracing_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### " o implode);
val error_message_fn =
@@ -113,7 +110,6 @@
fun writelns ss = ! writeln_fn (map output ss);
fun writeln s = writelns [s];
-fun urgent_message s = ! urgent_message_fn [output s]; (*Proof General legacy*)
fun tracing s = ! tracing_fn [output s];
fun warning s = ! warning_fn [output s];
fun error_message' (i, s) = ! error_message_fn (i, [output s]);
--- a/src/Pure/Isar/calculation.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/Pure/Isar/calculation.ML Fri Oct 31 11:36:41 2014 +0100
@@ -120,7 +120,7 @@
if int then
Proof_Context.pretty_fact ctxt'
(Proof_Context.full_name ctxt' (Binding.name calculationN), calc)
- |> Pretty.string_of |> Output.urgent_message
+ |> Pretty.string_of |> writeln
else ();
in state' |> final ? (put_calculation NONE #> Proof.chain_facts calc) end;
--- a/src/Pure/Isar/runtime.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/Pure/Isar/runtime.ML Fri Oct 31 11:36:41 2014 +0100
@@ -172,7 +172,7 @@
(fn () =>
debugging NONE body () handle exn =>
if Exn.is_interrupt exn then ()
- else Output.urgent_message ("## INTERNAL ERROR ##\n" ^ exn_message exn),
+ else writeln ("## INTERNAL ERROR ##\n" ^ exn_message exn),
Simple_Thread.attributes interrupts);
end;
--- a/src/Pure/Proof/extraction.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/Pure/Proof/extraction.ML Fri Oct 31 11:36:41 2014 +0100
@@ -121,7 +121,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 = Output.urgent_message (Pretty.spaces d ^ s);
+fun msg d s = writeln (Pretty.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/System/isabelle_process.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/Pure/System/isabelle_process.ML Fri Oct 31 11:36:41 2014 +0100
@@ -126,7 +126,6 @@
(fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
Output.system_message_fn := message Markup.systemN [];
Output.protocol_message_fn := message Markup.protocolN;
- Output.urgent_message_fn := ! Output.writeln_fn;
Output.prompt_fn := ignore;
message Markup.initN [] [Session.welcome ()];
msg_channel
--- a/src/Pure/Thy/thy_info.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/Pure/Thy/thy_info.ML Fri Oct 31 11:36:41 2014 +0100
@@ -143,7 +143,7 @@
else
let
val succs = thy_graph String_Graph.all_succs [name];
- val _ = Output.urgent_message ("Theory loader: removing " ^ commas_quote succs);
+ val _ = writeln ("Theory loader: removing " ^ commas_quote succs);
val _ = List.app (perform Remove) succs;
val _ = change_thys (fold String_Graph.del_node succs);
in () end);
@@ -269,7 +269,7 @@
fun load_thy document last_timing initiators update_time deps text (name, pos) keywords parents =
let
val _ = kill_thy name;
- val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
+ val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators);
val _ = Output.try_protocol_message (Markup.loading_theory name) [];
val {master = (thy_path, _), imports} = deps;
@@ -405,7 +405,7 @@
in
NAMED_CRITICAL "Thy_Info" (fn () =>
(kill_thy name;
- Output.urgent_message ("Registering theory " ^ quote name);
+ writeln ("Registering theory " ^ quote name);
update_thy (make_deps master imports) theory))
end;
--- a/src/Tools/quickcheck.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/Tools/quickcheck.ML Fri Oct 31 11:36:41 2014 +0100
@@ -294,11 +294,11 @@
if is_interactive then exc () else raise TimeLimit.TimeOut
else f ();
-fun message ctxt s = if Config.get ctxt quiet then () else Output.urgent_message s;
+fun message ctxt s = if Config.get ctxt quiet then () else writeln s;
fun verbose_message ctxt s =
if not (Config.get ctxt quiet) andalso Config.get ctxt verbose
- then Output.urgent_message s else ();
+ then writeln s else ();
fun test_terms ctxt (limit_time, is_interactive) insts goals =
(case active_testers ctxt of
@@ -517,7 +517,7 @@
gen_quickcheck args i (Toplevel.proof_of state)
|> apfst (Option.map (the o get_first response_of))
|> (fn (r, state) =>
- Output.urgent_message (Pretty.string_of
+ writeln (Pretty.string_of
(pretty_counterex (Proof.context_of state) false r)));
val parse_arg =
@@ -563,7 +563,7 @@
|> (if auto then
Proof.goal_message (K (Pretty.mark Markup.information msg))
else
- tap (fn _ => Output.urgent_message (Pretty.string_of msg))))
+ tap (fn _ => writeln (Pretty.string_of msg))))
else
(noneN, state)
end)
--- a/src/Tools/solve_direct.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/Tools/solve_direct.ML Fri Oct 31 11:36:41 2014 +0100
@@ -83,13 +83,13 @@
Pretty.markup Markup.information (message results))
else
tap (fn _ =>
- Output.urgent_message (Pretty.string_of (Pretty.chunks (message results))))))
+ writeln (Pretty.string_of (Pretty.chunks (message results))))))
| SOME NONE =>
- (if mode = Normal then Output.urgent_message "No proof found."
+ (if mode = Normal then writeln "No proof found."
else ();
(noneN, state))
| NONE =>
- (if mode = Normal then Output.urgent_message "An error occurred."
+ (if mode = Normal then writeln "An error occurred."
else ();
(unknownN, state)))
end
--- a/src/Tools/try.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/Tools/try.ML Fri Oct 31 11:36:41 2014 +0100
@@ -60,19 +60,19 @@
fun try_tools state =
if subgoal_count state = 0 then
- (Output.urgent_message "No subgoal!"; NONE)
+ (writeln "No subgoal!"; NONE)
else
get_tools (Proof.theory_of state)
|> tap (fn tools =>
"Trying " ^ space_implode " "
(serial_commas "and" (map (quote o fst) tools)) ^ "..."
- |> Output.urgent_message)
+ |> writeln)
|> Par_List.get_some
(fn (name, (_, _, tool)) =>
case try (tool false) state of
SOME (true, (outcome_code, _)) => SOME (name, outcome_code)
| _ => NONE)
- |> tap (fn NONE => Output.urgent_message "Tried in vain." | _ => ())
+ |> tap (fn NONE => writeln "Tried in vain." | _ => ())
val _ =
Outer_Syntax.improper_command @{command_spec "try"}