discontinued obsolete Output.urgent_message;
authorwenzelm
Fri Oct 31 11:36:41 2014 +0100 (2014-10-31)
changeset 58843521cea5fa777
parent 58842 22b87ab47d3b
child 58844 d659a12f9b7f
discontinued obsolete Output.urgent_message;
src/HOL/Library/refute.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Mutabelle/mutabelle_extra.ML
src/HOL/TPTP/atp_problem_import.ML
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/Sledgehammer/async_manager.ML
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
src/HOL/Tools/try0.ML
src/Pure/General/output.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/runtime.ML
src/Pure/Proof/extraction.ML
src/Pure/System/isabelle_process.ML
src/Pure/Thy/thy_info.ML
src/Tools/quickcheck.ML
src/Tools/solve_direct.ML
src/Tools/try.ML
     1.1 --- a/src/HOL/Library/refute.ML	Fri Oct 31 11:18:17 2014 +0100
     1.2 +++ b/src/HOL/Library/refute.ML	Fri Oct 31 11:36:41 2014 +0100
     1.3 @@ -1068,31 +1068,31 @@
     1.4                              ". Available solvers: " ^
     1.5                              commas (map (quote o fst) (SAT_Solver.get_solvers ())) ^ ".")
     1.6            in
     1.7 -            Output.urgent_message "Invoking SAT solver...";
     1.8 +            writeln "Invoking SAT solver...";
     1.9              (case solver fm of
    1.10                SAT_Solver.SATISFIABLE assignment =>
    1.11 -                (Output.urgent_message ("Model found:\n" ^ print_model ctxt model
    1.12 +                (writeln ("Model found:\n" ^ print_model ctxt model
    1.13                    (fn i => case assignment i of SOME b => b | NONE => true));
    1.14                   if maybe_spurious then "potential" else "genuine")
    1.15              | SAT_Solver.UNSATISFIABLE _ =>
    1.16 -                (Output.urgent_message "No model exists.";
    1.17 +                (writeln "No model exists.";
    1.18                  case next_universe universe sizes minsize maxsize of
    1.19                    SOME universe' => find_model_loop universe'
    1.20 -                | NONE => (Output.urgent_message
    1.21 +                | NONE => (writeln
    1.22                      "Search terminated, no larger universe within the given limits.";
    1.23                      "none"))
    1.24              | SAT_Solver.UNKNOWN =>
    1.25 -                (Output.urgent_message "No model found.";
    1.26 +                (writeln "No model found.";
    1.27                  case next_universe universe sizes minsize maxsize of
    1.28                    SOME universe' => find_model_loop universe'
    1.29 -                | NONE => (Output.urgent_message
    1.30 +                | NONE => (writeln
    1.31                    "Search terminated, no larger universe within the given limits.";
    1.32                    "unknown"))) handle SAT_Solver.NOT_CONFIGURED =>
    1.33                (error ("SAT solver " ^ quote satsolver ^ " is not configured.");
    1.34                 "unknown")
    1.35            end
    1.36            handle MAXVARS_EXCEEDED =>
    1.37 -            (Output.urgent_message ("Search terminated, number of Boolean variables ("
    1.38 +            (writeln ("Search terminated, number of Boolean variables ("
    1.39                ^ string_of_int maxvars ^ " allowed) exceeded.");
    1.40                "unknown")
    1.41  
    1.42 @@ -1114,14 +1114,14 @@
    1.43      maxtime>=0 orelse
    1.44        error ("\"maxtime\" is " ^ string_of_int maxtime ^ ", must be at least 0");
    1.45      (* enter loop with or without time limit *)
    1.46 -    Output.urgent_message ("Trying to find a model that "
    1.47 +    writeln ("Trying to find a model that "
    1.48        ^ (if negate then "refutes" else "satisfies") ^ ": "
    1.49        ^ Syntax.string_of_term ctxt t);
    1.50      if maxtime > 0 then (
    1.51        TimeLimit.timeLimit (Time.fromSeconds maxtime)
    1.52          wrapper ()
    1.53        handle TimeLimit.TimeOut =>
    1.54 -        (Output.urgent_message ("Search terminated, time limit (" ^
    1.55 +        (writeln ("Search terminated, time limit (" ^
    1.56              string_of_int maxtime
    1.57              ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.");
    1.58           check_expect "unknown")
    1.59 @@ -1207,7 +1207,7 @@
    1.60      val t = th |> prop_of
    1.61    in
    1.62      if Logic.count_prems t = 0 then
    1.63 -      (Output.urgent_message "No subgoal!"; "none")
    1.64 +      (writeln "No subgoal!"; "none")
    1.65      else
    1.66        let
    1.67          val assms = map term_of (Assumption.all_assms_of ctxt)
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Oct 31 11:18:17 2014 +0100
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Oct 31 11:36:41 2014 +0100
     2.3 @@ -428,7 +428,7 @@
     2.4            |> tap (fn factss =>
     2.5                       "Line " ^ str0 (Position.line_of pos) ^ ": " ^
     2.6                       Sledgehammer.string_of_factss factss
     2.7 -                     |> Output.urgent_message)
     2.8 +                     |> writeln)
     2.9          val prover = get_prover ctxt prover_name params goal facts
    2.10          val problem =
    2.11            {comment = "", state = st', goal = goal, subgoal = i,
     3.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Oct 31 11:18:17 2014 +0100
     3.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Oct 31 11:36:41 2014 +0100
     3.3 @@ -171,7 +171,7 @@
     3.4    let
     3.5      val params = []
     3.6      val res = Refute.refute_term (Proof_Context.init_global thy) params [] t
     3.7 -    val _ = Output.urgent_message ("Refute: " ^ res)
     3.8 +    val _ = writeln ("Refute: " ^ res)
     3.9    in
    3.10      (rpair []) (case res of
    3.11        "genuine" => GenuineCex
    3.12 @@ -194,7 +194,7 @@
    3.13      val state = Proof.init ctxt
    3.14      val (res, _) = Nitpick.pick_nits_in_term state
    3.15        (Nitpick_Commands.default_params thy []) Nitpick.Normal 1 1 1 [] [] [] t
    3.16 -    val _ = Output.urgent_message ("Nitpick: " ^ res)
    3.17 +    val _ = writeln ("Nitpick: " ^ res)
    3.18    in
    3.19      (rpair []) (case res of
    3.20        "genuine" => GenuineCex
    3.21 @@ -343,21 +343,21 @@
    3.22  (*
    3.23  fun unsafe_invoke_mtd thy (mtd_name, invoke_mtd) t =
    3.24    let
    3.25 -    val _ = Output.urgent_message ("Invoking " ^ mtd_name)
    3.26 +    val _ = writeln ("Invoking " ^ mtd_name)
    3.27      val ((res, (timing, reports)), time) = cpu_time "total time" (fn () => invoke_mtd thy t
    3.28        handle ERROR s => (tracing s; (Error, ([], NONE))))
    3.29 -    val _ = Output.urgent_message (" Done")
    3.30 +    val _ = writeln (" Done")
    3.31    in (res, (time :: timing, reports)) end
    3.32  *)  
    3.33  fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t =
    3.34    let
    3.35 -    val _ = Output.urgent_message ("Invoking " ^ mtd_name)
    3.36 +    val _ = writeln ("Invoking " ^ mtd_name)
    3.37      val (res, timing) = elapsed_time "total time"
    3.38        (fn () => case try (invoke_mtd thy) t of
    3.39            SOME (res, _) => res
    3.40 -        | NONE => (Output.urgent_message ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
    3.41 +        | NONE => (writeln ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
    3.42              Error))
    3.43 -    val _ = Output.urgent_message (" Done")
    3.44 +    val _ = writeln (" Done")
    3.45    in (res, [timing]) end
    3.46  
    3.47  (* creating entries *)
    3.48 @@ -387,7 +387,7 @@
    3.49      val mutants =
    3.50        if exec then
    3.51          let
    3.52 -          val _ = Output.urgent_message ("BEFORE PARTITION OF " ^
    3.53 +          val _ = writeln ("BEFORE PARTITION OF " ^
    3.54                              string_of_int (length mutants) ^ " MUTANTS")
    3.55            val (execs, noexecs) = List.partition (is_executable_term thy) (take_random (20 * max_mutants) mutants)
    3.56            val _ = tracing ("AFTER PARTITION (" ^ string_of_int (length execs) ^
    3.57 @@ -404,7 +404,7 @@
    3.58            |> filter (is_some o try (Thm.cterm_of thy))
    3.59            |> filter (is_some o try (Syntax.check_term (Proof_Context.init_global thy)))
    3.60            |> take_random max_mutants
    3.61 -    val _ = map (fn t => Output.urgent_message ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
    3.62 +    val _ = map (fn t => writeln ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
    3.63    in
    3.64      create_entry thy thm exec mutants mtds
    3.65    end
    3.66 @@ -458,7 +458,7 @@
    3.67  (* theory -> mtd list -> thm list -> string -> unit *)
    3.68  fun mutate_theorems_and_write_report thy (num_mutations, max_mutants) mtds thms file_name =
    3.69    let
    3.70 -    val _ = Output.urgent_message "Starting Mutabelle..."
    3.71 +    val _ = writeln "Starting Mutabelle..."
    3.72      val ctxt = Proof_Context.init_global thy
    3.73      val path = Path.explode file_name
    3.74      (* for normal report: *)
     4.1 --- a/src/HOL/TPTP/atp_problem_import.ML	Fri Oct 31 11:18:17 2014 +0100
     4.2 +++ b/src/HOL/TPTP/atp_problem_import.ML	Fri Oct 31 11:36:41 2014 +0100
     4.3 @@ -117,7 +117,7 @@
     4.4           if falsify then "CounterSatisfiable" else "Satisfiable"
     4.5         else
     4.6           "Unknown")
     4.7 -      |> Output.urgent_message
     4.8 +      |> writeln
     4.9      val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy snd file_name
    4.10      val params =
    4.11        [("maxtime", string_of_int timeout),
    4.12 @@ -135,7 +135,7 @@
    4.13  
    4.14  fun SOLVE_TIMEOUT seconds name tac st =
    4.15    let
    4.16 -    val _ = Output.urgent_message ("running " ^ name ^ " for " ^ string_of_int seconds ^ " s")
    4.17 +    val _ = writeln ("running " ^ name ^ " for " ^ string_of_int seconds ^ " s")
    4.18      val result =
    4.19        TimeLimit.timeLimit (Time.fromSeconds seconds) (fn () => SINGLE (SOLVE tac) st) ()
    4.20        handle
    4.21 @@ -143,8 +143,8 @@
    4.22        | ERROR _ => NONE
    4.23    in
    4.24      (case result of
    4.25 -      NONE => (Output.urgent_message ("FAILURE: " ^ name); Seq.empty)
    4.26 -    | SOME st' => (Output.urgent_message ("SUCCESS: " ^ name); Seq.single st'))
    4.27 +      NONE => (writeln ("FAILURE: " ^ name); Seq.empty)
    4.28 +    | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st'))
    4.29    end
    4.30  
    4.31  fun nitpick_finite_oracle_tac ctxt timeout i th =
    4.32 @@ -264,7 +264,7 @@
    4.33    Logic.list_implies (rev defs @ rev nondefs, case conjs of conj :: _ => conj | [] => @{prop False})
    4.34  
    4.35  fun print_szs_of_success conjs success =
    4.36 -  Output.urgent_message ("% SZS status " ^
    4.37 +  writeln ("% SZS status " ^
    4.38      (if success then
    4.39         if null conjs then "Unsatisfiable" else "Theorem"
    4.40       else
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri Oct 31 11:18:17 2014 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri Oct 31 11:36:41 2014 +0100
     5.3 @@ -241,11 +241,11 @@
     5.4          o Pretty.mark Markup.information
     5.5        else
     5.6          print o Pretty.string_of
     5.7 -    val pprint_a = pprint Output.urgent_message
     5.8 -    fun pprint_nt f = () |> is_mode_nt mode ? pprint Output.urgent_message o f
     5.9 -    fun pprint_v f = () |> verbose ? pprint Output.urgent_message o f
    5.10 +    val pprint_a = pprint writeln
    5.11 +    fun pprint_nt f = () |> is_mode_nt mode ? pprint writeln o f
    5.12 +    fun pprint_v f = () |> verbose ? pprint writeln o f
    5.13      fun pprint_d f = () |> debug ? pprint tracing o f
    5.14 -    val print = pprint Output.urgent_message o curry Pretty.blk 0 o pstrs
    5.15 +    val print = pprint writeln o curry Pretty.blk 0 o pstrs
    5.16      fun print_t f = () |> mode = TPTP ? print o f
    5.17  (*
    5.18      val print_g = pprint tracing o Pretty.str
    5.19 @@ -1015,8 +1015,8 @@
    5.20  fun pick_nits_in_term state (params as {timeout, expect, ...}) mode i n step
    5.21                        subst def_assm_ts nondef_assm_ts orig_t =
    5.22    let
    5.23 -    val print_nt = if is_mode_nt mode then Output.urgent_message else K ()
    5.24 -    val print_t = if mode = TPTP then Output.urgent_message else K ()
    5.25 +    val print_nt = if is_mode_nt mode then writeln else K ()
    5.26 +    val print_t = if mode = TPTP then writeln else K ()
    5.27    in
    5.28      if getenv "KODKODI" = "" then
    5.29        (* The "expect" argument is deliberately ignored if Kodkodi is missing so
    5.30 @@ -1068,7 +1068,7 @@
    5.31      val t = state |> Proof.raw_goal |> #goal |> prop_of
    5.32    in
    5.33      case Logic.count_prems t of
    5.34 -      0 => (Output.urgent_message "No subgoal!"; (noneN, state))
    5.35 +      0 => (writeln "No subgoal!"; (noneN, state))
    5.36      | n =>
    5.37        let
    5.38          val t = Logic.goal_params t i |> fst
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Oct 31 11:18:17 2014 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Oct 31 11:36:41 2014 +0100
     6.3 @@ -2140,8 +2140,7 @@
     6.4                      map (wf_constraint_for_triple rel) triples
     6.5                      |> foldr1 s_conj |> HOLogic.mk_Trueprop
     6.6           val _ = if debug then
     6.7 -                   Output.urgent_message ("Wellfoundedness goal: " ^
     6.8 -                             Syntax.string_of_term ctxt prop ^ ".")
     6.9 +                   writeln ("Wellfoundedness goal: " ^ Syntax.string_of_term ctxt prop ^ ".")
    6.10                   else
    6.11                     ()
    6.12         in
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Oct 31 11:18:17 2014 +0100
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Oct 31 11:36:41 2014 +0100
     7.3 @@ -1059,7 +1059,7 @@
     7.4            if debug then
     7.5              (if negate then "Genuineness" else "Spuriousness") ^ " goal: " ^
     7.6              Syntax.string_of_term ctxt prop ^ "."
     7.7 -            |> Output.urgent_message
     7.8 +            |> writeln
     7.9            else
    7.10              ()
    7.11          val goal = prop |> cterm_of thy |> Goal.init
     8.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Oct 31 11:18:17 2014 +0100
     8.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Oct 31 11:36:41 2014 +0100
     8.3 @@ -360,7 +360,7 @@
     8.4  fun try_upto_depth ctxt f =
     8.5    let
     8.6      val max_depth = Config.get ctxt Quickcheck.depth
     8.7 -    fun message s = if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message s
     8.8 +    fun message s = if Config.get ctxt Quickcheck.quiet then () else writeln s
     8.9      fun try' i =
    8.10        if i <= max_depth then
    8.11          let
     9.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Oct 31 11:18:17 2014 +0100
     9.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Oct 31 11:36:41 2014 +0100
     9.3 @@ -221,8 +221,8 @@
     9.4  fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code_modules, _) =
     9.5    let
     9.6      val ((is_genuine, counterexample_of), (get, put, put_ml)) = cookie
     9.7 -    fun message s = if quiet then () else Output.urgent_message s
     9.8 -    fun verbose_message s = if not quiet andalso verbose then Output.urgent_message s else ()
     9.9 +    fun message s = if quiet then () else writeln s
    9.10 +    fun verbose_message s = if not quiet andalso verbose then writeln s else ()
    9.11      val current_size = Unsynchronized.ref 0
    9.12      val current_result = Unsynchronized.ref Quickcheck.empty_result 
    9.13      val tmp_prefix = "Quickcheck_Narrowing"
    9.14 @@ -511,7 +511,7 @@
    9.15          (maps (map snd) correct_inst_goals) []
    9.16      end
    9.17    else
    9.18 -    (if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message
    9.19 +    (if Config.get ctxt Quickcheck.quiet then () else writeln
    9.20        ("Environment variable ISABELLE_GHC is not set. To use narrowing-based quickcheck, please set "
    9.21          ^ "this variable to your GHC Haskell compiler in your settings file. "
    9.22          ^ "To deactivate narrowing-based quickcheck, set quickcheck_narrowing_active to false.");
    10.1 --- a/src/HOL/Tools/Sledgehammer/async_manager.ML	Fri Oct 31 11:18:17 2014 +0100
    10.2 +++ b/src/HOL/Tools/Sledgehammer/async_manager.ML	Fri Oct 31 11:36:41 2014 +0100
    10.3 @@ -106,7 +106,7 @@
    10.4                    tool ^ ": " ^
    10.5                    implode_message (workers |> sort_distinct string_ord, work)
    10.6                    |> break_into_chunks
    10.7 -                  |> List.app Output.urgent_message)
    10.8 +                  |> List.app writeln)
    10.9  
   10.10  fun check_thread_manager () = Synchronized.change global_state
   10.11    (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
   10.12 @@ -178,7 +178,7 @@
   10.13        val state' = make_state manager timeout_heap [] (killing @ canceling) messages store
   10.14        val _ =
   10.15          if null killing then ()
   10.16 -        else Output.urgent_message ("Interrupted active " ^ das_wort_worker ^ "s.")
   10.17 +        else writeln ("Interrupted active " ^ das_wort_worker ^ "s.")
   10.18      in state' end)
   10.19  
   10.20  fun str_of_time time = string_of_int (Time.toSeconds time) ^ " s"
   10.21 @@ -210,7 +210,7 @@
   10.22        case map_filter canceling_info canceling of
   10.23          [] => []
   10.24        | ss => "Interrupting " ^ das_wort_worker ^ "s" :: ss
   10.25 -  in Output.urgent_message (space_implode "\n\n" (running @ interrupting)) end
   10.26 +  in writeln (space_implode "\n\n" (running @ interrupting)) end
   10.27  
   10.28  fun thread_messages tool das_wort_worker opt_limit =
   10.29    let
   10.30 @@ -222,6 +222,6 @@
   10.31          (if length tool_store <= limit then ":"
   10.32           else " (" ^ string_of_int limit ^ " displayed):")
   10.33      val ss = tool_store |> chop limit |> #1 |> map (op ^ o snd)
   10.34 -  in List.app Output.urgent_message (header :: maps break_into_chunks ss) end
   10.35 +  in List.app writeln (header :: maps break_into_chunks ss) end
   10.36  
   10.37  end;
    11.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Oct 31 11:18:17 2014 +0100
    11.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Oct 31 11:36:41 2014 +0100
    11.3 @@ -137,7 +137,7 @@
    11.4        |> commas
    11.5        |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
    11.6                    " proof (of " ^ string_of_int (length facts) ^ "): ") "."
    11.7 -      |> Output.urgent_message
    11.8 +      |> writeln
    11.9  
   11.10      fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) =
   11.11          let
   11.12 @@ -230,7 +230,7 @@
   11.13            else
   11.14              outcome
   11.15              |> Async_Manager.break_into_chunks
   11.16 -            |> List.app Output.urgent_message
   11.17 +            |> List.app writeln
   11.18        in (outcome_code, state) end
   11.19      else
   11.20        (Async_Manager.thread SledgehammerN birth_time death_time
   11.21 @@ -259,12 +259,12 @@
   11.22    else
   11.23      (case subgoal_count state of
   11.24        0 =>
   11.25 -      ((if blocking then error else Output.urgent_message) "No subgoal!"; (false, (noneN, state)))
   11.26 +      ((if blocking then error else writeln) "No subgoal!"; (false, (noneN, state)))
   11.27      | n =>
   11.28        let
   11.29          val _ = Proof.assert_backward state
   11.30          val print =
   11.31 -          if mode = Normal andalso is_none output_result then Output.urgent_message else K ()
   11.32 +          if mode = Normal andalso is_none output_result then writeln else K ()
   11.33          val ctxt = Proof.context_of state
   11.34          val {facts = chained, goal, ...} = Proof.goal state
   11.35          val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
    12.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Oct 31 11:18:17 2014 +0100
    12.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Oct 31 11:36:41 2014 +0100
    12.3 @@ -150,7 +150,7 @@
    12.4  fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
    12.5      (one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) =
    12.6    let
    12.7 -    val _ = if debug then Output.urgent_message "Constructing Isar proof..." else ()
    12.8 +    val _ = if debug then writeln "Constructing Isar proof..." else ()
    12.9  
   12.10      fun generate_proof_text () =
   12.11        let
    13.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Oct 31 11:18:17 2014 +0100
    13.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Oct 31 11:36:41 2014 +0100
    13.3 @@ -1016,7 +1016,7 @@
    13.4        val num_isar_deps = length isar_deps
    13.5      in
    13.6        if verbose andalso auto_level = 0 then
    13.7 -        Output.urgent_message ("MaSh: " ^ quote prover ^ " on " ^ quote name ^ " with " ^
    13.8 +        writeln ("MaSh: " ^ quote prover ^ " on " ^ quote name ^ " with " ^
    13.9            string_of_int num_isar_deps ^ " + " ^ string_of_int (length facts - num_isar_deps) ^
   13.10            " facts.")
   13.11        else
   13.12 @@ -1025,7 +1025,7 @@
   13.13          {outcome = NONE, used_facts, ...} =>
   13.14          (if verbose andalso auto_level = 0 then
   13.15             let val num_facts = length used_facts in
   13.16 -             Output.urgent_message ("Found proof with " ^ string_of_int num_facts ^ " fact" ^
   13.17 +             writeln ("Found proof with " ^ string_of_int num_facts ^ " fact" ^
   13.18                 plural_s num_facts ^ ".")
   13.19             end
   13.20           else
   13.21 @@ -1212,7 +1212,7 @@
   13.22      |> pairself (map fact_of_raw_fact)
   13.23    end
   13.24  
   13.25 -fun mash_unlearn () = (clear_state (); Output.urgent_message "Reset MaSh.")
   13.26 +fun mash_unlearn () = (clear_state (); writeln "Reset MaSh.")
   13.27  
   13.28  fun learn_wrt_access_graph ctxt (name, parents, feats, deps)
   13.29      (accum as (access_G, (fact_xtab, feat_xtab))) =
   13.30 @@ -1361,11 +1361,11 @@
   13.31              end
   13.32  
   13.33          fun commit last learns relearns flops =
   13.34 -          (if debug andalso auto_level = 0 then Output.urgent_message "Committing..." else ();
   13.35 +          (if debug andalso auto_level = 0 then writeln "Committing..." else ();
   13.36             map_state ctxt (do_commit (rev learns) relearns flops);
   13.37             if not last andalso auto_level = 0 then
   13.38               let val num_proofs = length learns + length relearns in
   13.39 -               Output.urgent_message ("Learned " ^ string_of_int num_proofs ^ " " ^
   13.40 +               writeln ("Learned " ^ string_of_int num_proofs ^ " " ^
   13.41                   (if run_prover then "automatic" else "Isar") ^ " proof" ^
   13.42                   plural_s num_proofs ^ " in the last " ^ string_of_time commit_timeout ^ ".")
   13.43               end
   13.44 @@ -1474,18 +1474,18 @@
   13.45  
   13.46      fun learn auto_level run_prover =
   13.47        mash_learn_facts ctxt params prover auto_level run_prover one_year facts
   13.48 -      |> Output.urgent_message
   13.49 +      |> writeln
   13.50    in
   13.51      if run_prover then
   13.52 -      (Output.urgent_message ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
   13.53 +      (writeln ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
   13.54           plural_s num_facts ^ " for automatic proofs (" ^ quote prover ^ " timeout: " ^
   13.55           string_of_time timeout ^ ").\n\nCollecting Isar proofs first...");
   13.56         learn 1 false;
   13.57 -       Output.urgent_message "Now collecting automatic proofs. This may take several hours. You \
   13.58 +       writeln "Now collecting automatic proofs. This may take several hours. You \
   13.59           \can safely stop the learning process at any point.";
   13.60         learn 0 true)
   13.61      else
   13.62 -      (Output.urgent_message ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
   13.63 +      (writeln ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
   13.64           plural_s num_facts ^ " for Isar proofs...");
   13.65         learn 0 false)
   13.66    end
   13.67 @@ -1522,7 +1522,7 @@
   13.68             Time.toSeconds timeout >= min_secs_for_learning then
   13.69            let val timeout = time_mult learn_timeout_slack timeout in
   13.70              (if verbose then
   13.71 -               Output.urgent_message ("Started MaShing through " ^
   13.72 +               writeln ("Started MaShing through " ^
   13.73                   (if exact then "" else "at least ") ^ string_of_int min_num_facts_to_learn ^
   13.74                   " fact" ^ plural_s min_num_facts_to_learn ^ " in the background.")
   13.75               else
   13.76 @@ -1545,7 +1545,7 @@
   13.77              | num_facts_to_learn =>
   13.78                if num_facts_to_learn <= max_facts_to_learn_before_query then
   13.79                  mash_learn_facts ctxt params prover 2 false timeout facts
   13.80 -                |> (fn "" => () | s => Output.urgent_message (MaShN ^ ": " ^ s))
   13.81 +                |> (fn "" => () | s => writeln (MaShN ^ ": " ^ s))
   13.82                else
   13.83                  maybe_launch_thread true num_facts_to_learn)
   13.84            else
    14.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Oct 31 11:18:17 2014 +0100
    14.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Oct 31 11:36:41 2014 +0100
    14.3 @@ -198,7 +198,7 @@
    14.4        sort_strings (supported_atps thy) @ sort_strings (SMT_Config.available_solvers_of ctxt)
    14.5        |> List.partition (String.isPrefix remote_prefix)
    14.6    in
    14.7 -    Output.urgent_message ("Supported provers: " ^ commas (local_provers @ remote_provers) ^ ".")
    14.8 +    writeln ("Supported provers: " ^ commas (local_provers @ remote_provers) ^ ".")
    14.9    end
   14.10  
   14.11  fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover"
    15.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Oct 31 11:18:17 2014 +0100
    15.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Oct 31 11:36:41 2014 +0100
    15.3 @@ -250,7 +250,7 @@
    15.4                  quote name ^ " slice #" ^ string_of_int (slice + 1) ^
    15.5                  " with " ^ string_of_int num_facts ^ " fact" ^
    15.6                  plural_s num_facts ^ " for " ^ string_of_time slice_timeout ^ "..."
    15.7 -                |> Output.urgent_message
    15.8 +                |> writeln
    15.9                else
   15.10                  ()
   15.11              val readable_names = not (Config.get ctxt atp_full_names)
   15.12 @@ -370,7 +370,7 @@
   15.13            (used_facts, preferred_methss,
   15.14             fn preplay =>
   15.15                let
   15.16 -                val _ = if verbose then Output.urgent_message "Generating proof text..." else ()
   15.17 +                val _ = if verbose then writeln "Generating proof text..." else ()
   15.18  
   15.19                  fun isar_params () =
   15.20                    let
    16.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Fri Oct 31 11:18:17 2014 +0100
    16.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Fri Oct 31 11:36:41 2014 +0100
    16.3 @@ -76,7 +76,7 @@
    16.4      (if n > 0 then ": " ^ (names |> map fst |> sort string_ord |> space_implode " ") else "")
    16.5    end
    16.6  
    16.7 -fun print silent f = if silent then () else Output.urgent_message (f ())
    16.8 +fun print silent f = if silent then () else writeln (f ())
    16.9  
   16.10  fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
   16.11        type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs,
    17.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Fri Oct 31 11:18:17 2014 +0100
    17.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Fri Oct 31 11:36:41 2014 +0100
    17.3 @@ -113,7 +113,7 @@
    17.4            if debug then
    17.5              quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^
    17.6              " fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout
    17.7 -            |> Output.urgent_message
    17.8 +            |> writeln
    17.9            else
   17.10              ()
   17.11          val birth = Timer.checkRealTimer timer
   17.12 @@ -163,7 +163,7 @@
   17.13                  string_of_atp_failure (failure_of_smt_failure (the outcome)) ^
   17.14                  " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
   17.15                  "..."
   17.16 -                |> Output.urgent_message
   17.17 +                |> writeln
   17.18                else
   17.19                  ()
   17.20            in
   17.21 @@ -204,7 +204,7 @@
   17.22            (preferred_methss,
   17.23             fn preplay =>
   17.24               let
   17.25 -               val _ = if verbose then Output.urgent_message "Generating proof text..." else ()
   17.26 +               val _ = if verbose then writeln "Generating proof text..." else ()
   17.27  
   17.28                 fun isar_params () =
   17.29                   (verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (),
    18.1 --- a/src/HOL/Tools/try0.ML	Fri Oct 31 11:18:17 2014 +0100
    18.2 +++ b/src/HOL/Tools/try0.ML	Fri Oct 31 11:36:41 2014 +0100
    18.3 @@ -124,12 +124,12 @@
    18.4      if mode = Normal then
    18.5        "Trying " ^ space_implode " " (Try.serial_commas "and" (map (quote o fst) named_methods)) ^
    18.6        "..."
    18.7 -      |> Output.urgent_message
    18.8 +      |> writeln
    18.9      else
   18.10        ();
   18.11      (case par_map (fn f => f mode timeout_opt quad st) apply_methods of
   18.12        [] =>
   18.13 -      (if mode = Normal then Output.urgent_message "No proof found." else (); (false, (noneN, st)))
   18.14 +      (if mode = Normal then writeln "No proof found." else (); (false, (noneN, st)))
   18.15      | xs as (name, command, _) :: _ =>
   18.16        let
   18.17          val xs = xs |> map (fn (name, _, n) => (n, name))
   18.18 @@ -152,7 +152,7 @@
   18.19             |> (if mode = Auto_Try then
   18.20                   Proof.goal_message (fn () => Pretty.markup Markup.information [Pretty.str message])
   18.21                 else
   18.22 -                 tap (fn _ => Output.urgent_message message))))
   18.23 +                 tap (fn _ => writeln message))))
   18.24        end)
   18.25    end;
   18.26  
    19.1 --- a/src/Pure/General/output.ML	Fri Oct 31 11:18:17 2014 +0100
    19.2 +++ b/src/Pure/General/output.ML	Fri Oct 31 11:36:41 2014 +0100
    19.3 @@ -26,7 +26,6 @@
    19.4    val physical_writeln: output -> unit
    19.5    exception Protocol_Message of Properties.T
    19.6    val writelns: string list -> unit
    19.7 -  val urgent_message: string -> unit
    19.8    val error_message': serial * string -> unit
    19.9    val error_message: string -> unit
   19.10    val system_message: string -> unit
   19.11 @@ -42,7 +41,6 @@
   19.12  sig
   19.13    include OUTPUT
   19.14    val writeln_fn: (output list -> unit) Unsynchronized.ref
   19.15 -  val urgent_message_fn: (output list -> unit) Unsynchronized.ref
   19.16    val tracing_fn: (output list -> unit) Unsynchronized.ref
   19.17    val warning_fn: (output list -> unit) Unsynchronized.ref
   19.18    val error_message_fn: (serial * output list -> unit) Unsynchronized.ref
   19.19 @@ -98,7 +96,6 @@
   19.20  exception Protocol_Message of Properties.T;
   19.21  
   19.22  val writeln_fn = Unsynchronized.ref (physical_writeln o implode);
   19.23 -val urgent_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);  (*Proof General legacy*)
   19.24  val tracing_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
   19.25  val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### " o implode);
   19.26  val error_message_fn =
   19.27 @@ -113,7 +110,6 @@
   19.28  
   19.29  fun writelns ss = ! writeln_fn (map output ss);
   19.30  fun writeln s = writelns [s];
   19.31 -fun urgent_message s = ! urgent_message_fn [output s];  (*Proof General legacy*)
   19.32  fun tracing s = ! tracing_fn [output s];
   19.33  fun warning s = ! warning_fn [output s];
   19.34  fun error_message' (i, s) = ! error_message_fn (i, [output s]);
    20.1 --- a/src/Pure/Isar/calculation.ML	Fri Oct 31 11:18:17 2014 +0100
    20.2 +++ b/src/Pure/Isar/calculation.ML	Fri Oct 31 11:36:41 2014 +0100
    20.3 @@ -120,7 +120,7 @@
    20.4        if int then
    20.5          Proof_Context.pretty_fact ctxt'
    20.6            (Proof_Context.full_name ctxt' (Binding.name calculationN), calc)
    20.7 -        |> Pretty.string_of |> Output.urgent_message
    20.8 +        |> Pretty.string_of |> writeln
    20.9        else ();
   20.10    in state' |> final ? (put_calculation NONE #> Proof.chain_facts calc) end;
   20.11  
    21.1 --- a/src/Pure/Isar/runtime.ML	Fri Oct 31 11:18:17 2014 +0100
    21.2 +++ b/src/Pure/Isar/runtime.ML	Fri Oct 31 11:36:41 2014 +0100
    21.3 @@ -172,7 +172,7 @@
    21.4      (fn () =>
    21.5        debugging NONE body () handle exn =>
    21.6          if Exn.is_interrupt exn then ()
    21.7 -        else Output.urgent_message ("## INTERNAL ERROR ##\n" ^ exn_message exn),
    21.8 +        else writeln ("## INTERNAL ERROR ##\n" ^ exn_message exn),
    21.9        Simple_Thread.attributes interrupts);
   21.10  
   21.11  end;
    22.1 --- a/src/Pure/Proof/extraction.ML	Fri Oct 31 11:18:17 2014 +0100
    22.2 +++ b/src/Pure/Proof/extraction.ML	Fri Oct 31 11:36:41 2014 +0100
    22.3 @@ -121,7 +121,7 @@
    22.4  fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs));
    22.5  fun corr_name s vs = extr_name s vs ^ "_correctness";
    22.6  
    22.7 -fun msg d s = Output.urgent_message (Pretty.spaces d ^ s);
    22.8 +fun msg d s = writeln (Pretty.spaces d ^ s);
    22.9  
   22.10  fun vars_of t = map Var (rev (Term.add_vars t []));
   22.11  fun frees_of t = map Free (rev (Term.add_frees t []));
    23.1 --- a/src/Pure/System/isabelle_process.ML	Fri Oct 31 11:18:17 2014 +0100
    23.2 +++ b/src/Pure/System/isabelle_process.ML	Fri Oct 31 11:36:41 2014 +0100
    23.3 @@ -126,7 +126,6 @@
    23.4        (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
    23.5      Output.system_message_fn := message Markup.systemN [];
    23.6      Output.protocol_message_fn := message Markup.protocolN;
    23.7 -    Output.urgent_message_fn := ! Output.writeln_fn;
    23.8      Output.prompt_fn := ignore;
    23.9      message Markup.initN [] [Session.welcome ()];
   23.10      msg_channel
    24.1 --- a/src/Pure/Thy/thy_info.ML	Fri Oct 31 11:18:17 2014 +0100
    24.2 +++ b/src/Pure/Thy/thy_info.ML	Fri Oct 31 11:36:41 2014 +0100
    24.3 @@ -143,7 +143,7 @@
    24.4    else
    24.5      let
    24.6        val succs = thy_graph String_Graph.all_succs [name];
    24.7 -      val _ = Output.urgent_message ("Theory loader: removing " ^ commas_quote succs);
    24.8 +      val _ = writeln ("Theory loader: removing " ^ commas_quote succs);
    24.9        val _ = List.app (perform Remove) succs;
   24.10        val _ = change_thys (fold String_Graph.del_node succs);
   24.11      in () end);
   24.12 @@ -269,7 +269,7 @@
   24.13  fun load_thy document last_timing initiators update_time deps text (name, pos) keywords parents =
   24.14    let
   24.15      val _ = kill_thy name;
   24.16 -    val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
   24.17 +    val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators);
   24.18      val _ = Output.try_protocol_message (Markup.loading_theory name) [];
   24.19  
   24.20      val {master = (thy_path, _), imports} = deps;
   24.21 @@ -405,7 +405,7 @@
   24.22    in
   24.23      NAMED_CRITICAL "Thy_Info" (fn () =>
   24.24       (kill_thy name;
   24.25 -      Output.urgent_message ("Registering theory " ^ quote name);
   24.26 +      writeln ("Registering theory " ^ quote name);
   24.27        update_thy (make_deps master imports) theory))
   24.28    end;
   24.29  
    25.1 --- a/src/Tools/quickcheck.ML	Fri Oct 31 11:18:17 2014 +0100
    25.2 +++ b/src/Tools/quickcheck.ML	Fri Oct 31 11:36:41 2014 +0100
    25.3 @@ -294,11 +294,11 @@
    25.4          if is_interactive then exc () else raise TimeLimit.TimeOut
    25.5    else f ();
    25.6  
    25.7 -fun message ctxt s = if Config.get ctxt quiet then () else Output.urgent_message s;
    25.8 +fun message ctxt s = if Config.get ctxt quiet then () else writeln s;
    25.9  
   25.10  fun verbose_message ctxt s =
   25.11    if not (Config.get ctxt quiet) andalso Config.get ctxt verbose
   25.12 -  then Output.urgent_message s else ();
   25.13 +  then writeln s else ();
   25.14  
   25.15  fun test_terms ctxt (limit_time, is_interactive) insts goals =
   25.16    (case active_testers ctxt of
   25.17 @@ -517,7 +517,7 @@
   25.18    gen_quickcheck args i (Toplevel.proof_of state)
   25.19    |> apfst (Option.map (the o get_first response_of))
   25.20    |> (fn (r, state) =>
   25.21 -      Output.urgent_message (Pretty.string_of
   25.22 +      writeln (Pretty.string_of
   25.23          (pretty_counterex (Proof.context_of state) false r)));
   25.24  
   25.25  val parse_arg =
   25.26 @@ -563,7 +563,7 @@
   25.27               |> (if auto then
   25.28                     Proof.goal_message (K (Pretty.mark Markup.information msg))
   25.29                   else
   25.30 -                   tap (fn _ => Output.urgent_message (Pretty.string_of msg))))
   25.31 +                   tap (fn _ => writeln (Pretty.string_of msg))))
   25.32            else
   25.33              (noneN, state)
   25.34          end)
    26.1 --- a/src/Tools/solve_direct.ML	Fri Oct 31 11:18:17 2014 +0100
    26.2 +++ b/src/Tools/solve_direct.ML	Fri Oct 31 11:36:41 2014 +0100
    26.3 @@ -83,13 +83,13 @@
    26.4                     Pretty.markup Markup.information (message results))
    26.5               else
    26.6                 tap (fn _ =>
    26.7 -                 Output.urgent_message (Pretty.string_of (Pretty.chunks (message results))))))
    26.8 +                 writeln (Pretty.string_of (Pretty.chunks (message results))))))
    26.9      | SOME NONE =>
   26.10 -        (if mode = Normal then Output.urgent_message "No proof found."
   26.11 +        (if mode = Normal then writeln "No proof found."
   26.12           else ();
   26.13           (noneN, state))
   26.14      | NONE =>
   26.15 -        (if mode = Normal then Output.urgent_message "An error occurred."
   26.16 +        (if mode = Normal then writeln "An error occurred."
   26.17           else ();
   26.18           (unknownN, state)))
   26.19    end
    27.1 --- a/src/Tools/try.ML	Fri Oct 31 11:18:17 2014 +0100
    27.2 +++ b/src/Tools/try.ML	Fri Oct 31 11:36:41 2014 +0100
    27.3 @@ -60,19 +60,19 @@
    27.4  
    27.5  fun try_tools state =
    27.6    if subgoal_count state = 0 then
    27.7 -    (Output.urgent_message "No subgoal!"; NONE)
    27.8 +    (writeln "No subgoal!"; NONE)
    27.9    else
   27.10      get_tools (Proof.theory_of state)
   27.11      |> tap (fn tools =>
   27.12                 "Trying " ^ space_implode " "
   27.13                      (serial_commas "and" (map (quote o fst) tools)) ^ "..."
   27.14 -               |> Output.urgent_message)
   27.15 +               |> writeln)
   27.16      |> Par_List.get_some
   27.17             (fn (name, (_, _, tool)) =>
   27.18                 case try (tool false) state of
   27.19                   SOME (true, (outcome_code, _)) => SOME (name, outcome_code)
   27.20                 | _ => NONE)
   27.21 -    |> tap (fn NONE => Output.urgent_message "Tried in vain." | _ => ())
   27.22 +    |> tap (fn NONE => writeln "Tried in vain." | _ => ())
   27.23  
   27.24  val _ =
   27.25    Outer_Syntax.improper_command @{command_spec "try"}