renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
authorwenzelm
Mon Oct 25 21:06:56 2010 +0200 (2010-10-25 ago)
changeset 401327ee65dbffa31
parent 40131 7cbebd636e79
child 40133 b61d52de66f0
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
src/HOL/Mutabelle/MutabelleExtra.thy
src/HOL/Mutabelle/mutabelle.ML
src/HOL/Mutabelle/mutabelle_extra.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/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
src/HOL/Tools/async_manager.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/try.ML
src/Pure/General/output.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/toplevel.ML
src/Pure/Proof/extraction.ML
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/System/isabelle_process.ML
src/Pure/Thy/thy_info.ML
src/Tools/quickcheck.ML
src/Tools/solve_direct.ML
     1.1 --- a/src/HOL/Mutabelle/MutabelleExtra.thy	Mon Oct 25 20:24:13 2010 +0200
     1.2 +++ b/src/HOL/Mutabelle/MutabelleExtra.thy	Mon Oct 25 21:06:56 2010 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4  
     1.5  ML {* val old_tr = !Output.tracing_fn *}
     1.6  ML {* val old_wr = !Output.writeln_fn *}
     1.7 -ML {* val old_pr = !Output.priority_fn *}
     1.8 +ML {* val old_ur = !Output.urgent_message_fn *}
     1.9  ML {* val old_wa = !Output.warning_fn *}
    1.10  
    1.11  quickcheck_params [size = 5, iterations = 1000]
    1.12 @@ -50,7 +50,7 @@
    1.13  
    1.14  ML {* Output.tracing_fn := old_tr *}
    1.15  ML {* Output.writeln_fn := old_wr *}
    1.16 -ML {* Output.priority_fn := old_pr *}
    1.17 +ML {* Output.urgent_message_fn := old_ur *}
    1.18  ML {* Output.warning_fn := old_wa *}
    1.19  
    1.20  end
     2.1 --- a/src/HOL/Mutabelle/mutabelle.ML	Mon Oct 25 20:24:13 2010 +0200
     2.2 +++ b/src/HOL/Mutabelle/mutabelle.ML	Mon Oct 25 21:06:56 2010 +0200
     2.3 @@ -499,14 +499,14 @@
     2.4  fun is_executable thy insts th =
     2.5   (Quickcheck.test_term
     2.6      (ProofContext.init_global thy) false (SOME (!testgen_name)) 1 1 (preprocess thy insts (prop_of th));
     2.7 -  priority "executable"; true) handle ERROR s =>
     2.8 -    (priority ("not executable: " ^ s); false);
     2.9 +  Output.urgent_message "executable"; true) handle ERROR s =>
    2.10 +    (Output.urgent_message ("not executable: " ^ s); false);
    2.11  
    2.12  fun qc_recursive usedthy [] insts sz qciter acc = rev acc
    2.13   | qc_recursive usedthy (x::xs) insts sz qciter acc = qc_recursive usedthy xs insts sz qciter 
    2.14 -     (priority ("qc_recursive: " ^ string_of_int (length xs)); ((x, pretty (the_default [] (Quickcheck.test_term
    2.15 +     (Output.urgent_message ("qc_recursive: " ^ string_of_int (length xs)); ((x, pretty (the_default [] (Quickcheck.test_term
    2.16         (ProofContext.init_global usedthy) false (SOME (!testgen_name)) sz qciter (preprocess usedthy insts x)))) :: acc))
    2.17 -          handle ERROR msg => (priority msg; qc_recursive usedthy xs insts sz qciter acc);
    2.18 +          handle ERROR msg => (Output.urgent_message msg; qc_recursive usedthy xs insts sz qciter acc);
    2.19  
    2.20  
    2.21  (*quickcheck-test the mutants created by function mutate with type-instantiation insts, 
    2.22 @@ -721,11 +721,11 @@
    2.23  fun mutqc_thystat option p mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename =
    2.24   let
    2.25     val thmlist = filter
    2.26 -     (fn (s, th) => not (p s th) andalso (priority s; is_executable mutthy insts th)) (thms_of mutthy)
    2.27 +     (fn (s, th) => not (p s th) andalso (Output.urgent_message s; is_executable mutthy insts th)) (thms_of mutthy)
    2.28     fun mutthmrec [] = ()
    2.29     |   mutthmrec ((name,thm)::xs) =
    2.30       let          
    2.31 -       val _ = priority ("mutthmrec: " ^ name);
    2.32 +       val _ = Output.urgent_message ("mutthmrec: " ^ name);
    2.33         val mutated = mutate option (prop_of thm) usedthy
    2.34             commutatives forbidden_funs iter
    2.35         val (passednum,_,cenum,_) = qc_test mutated insts usedthy sz qciter
     3.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Oct 25 20:24:13 2010 +0200
     3.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Oct 25 21:06:56 2010 +0200
     3.3 @@ -109,7 +109,7 @@
     3.4  fun invoke_refute thy t =
     3.5    let
     3.6      val res = MyRefute.refute_term thy [] t
     3.7 -    val _ = priority ("Refute: " ^ res)
     3.8 +    val _ = Output.urgent_message ("Refute: " ^ res)
     3.9    in
    3.10      case res of
    3.11        "genuine" => GenuineCex
    3.12 @@ -137,7 +137,7 @@
    3.13    in
    3.14      let
    3.15        val (res, _) = Nitpick.pick_nits_in_term state (Nitpick_Isar.default_params thy []) false [] t
    3.16 -      val _ = priority ("Nitpick: " ^ res)
    3.17 +      val _ = Output.urgent_message ("Nitpick: " ^ res)
    3.18      in
    3.19        case res of
    3.20          "genuine" => GenuineCex
    3.21 @@ -182,7 +182,7 @@
    3.22             (error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^
    3.23                     "."))
    3.24           | Exn.Interrupt => raise Exn.Interrupt
    3.25 -         | _ => (priority ("Unknown error in Nitpick"); Error)
    3.26 +         | _ => (Output.urgent_message ("Unknown error in Nitpick"); Error)
    3.27    end
    3.28  val nitpick_mtd = ("nitpick", invoke_nitpick)
    3.29  *)
    3.30 @@ -281,13 +281,13 @@
    3.31  
    3.32  fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t =
    3.33    let
    3.34 -    val _ = priority ("Invoking " ^ mtd_name)
    3.35 +    val _ = Output.urgent_message ("Invoking " ^ mtd_name)
    3.36      val ((res, (timing, reports)), time) = cpu_time "total time"
    3.37        (fn () => case try (invoke_mtd thy) t of
    3.38            SOME (res, (timing, reports)) => (res, (timing, reports))
    3.39 -        | NONE => (priority ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
    3.40 +        | NONE => (Output.urgent_message ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
    3.41             (Error , ([], NONE))))
    3.42 -    val _ = priority (" Done")
    3.43 +    val _ = Output.urgent_message (" Done")
    3.44    in (res, (time :: timing, reports)) end
    3.45  
    3.46  (* theory -> term list -> mtd -> subentry *)
    3.47 @@ -316,7 +316,7 @@
    3.48  fun mutate_theorem create_entry thy mtds thm =
    3.49    let
    3.50      val exec = is_executable_thm thy thm
    3.51 -    val _ = priority (if exec then "EXEC" else "NOEXEC")
    3.52 +    val _ = Output.urgent_message (if exec then "EXEC" else "NOEXEC")
    3.53      val mutants =
    3.54            (if num_mutations = 0 then
    3.55               [Thm.prop_of thm]
    3.56 @@ -327,7 +327,7 @@
    3.57      val mutants =
    3.58        if exec then
    3.59          let
    3.60 -          val _ = priority ("BEFORE PARTITION OF " ^
    3.61 +          val _ = Output.urgent_message ("BEFORE PARTITION OF " ^
    3.62                              Int.toString (length mutants) ^ " MUTANTS")
    3.63            val (execs, noexecs) = List.partition (is_executable_term thy) (take_random (20 * max_mutants) mutants)
    3.64            val _ = tracing ("AFTER PARTITION (" ^ Int.toString (length execs) ^
    3.65 @@ -342,7 +342,7 @@
    3.66            |> map Mutabelle.freeze |> map freezeT
    3.67  (*          |> filter (not o is_forbidden_mutant) *)
    3.68            |> List.mapPartial (try (Sign.cert_term thy))
    3.69 -    val _ = map (fn t => priority ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
    3.70 +    val _ = map (fn t => Output.urgent_message ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
    3.71    in
    3.72      create_entry thy thm exec mutants mtds
    3.73    end
    3.74 @@ -421,7 +421,7 @@
    3.75  (* theory -> mtd list -> thm list -> string -> unit *)
    3.76  fun mutate_theorems_and_write_report thy mtds thms file_name =
    3.77    let
    3.78 -    val _ = priority "Starting Mutabelle..."
    3.79 +    val _ = Output.urgent_message "Starting Mutabelle..."
    3.80      val path = Path.explode file_name
    3.81      (* for normal report: *)
    3.82      (*val (gen_create_entry, gen_string_for_entry) = (create_entry, string_for_entry)*)
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Oct 25 20:24:13 2010 +0200
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Oct 25 21:06:56 2010 +0200
     4.3 @@ -216,7 +216,7 @@
     4.4          o Pretty.chunks o cons (Pretty.str "") o single
     4.5          o Pretty.mark Markup.hilite
     4.6        else
     4.7 -        (fn s => (priority s; if debug then tracing s else ()))
     4.8 +        (fn s => (Output.urgent_message s; if debug then tracing s else ()))
     4.9          o Pretty.string_of
    4.10      fun pprint_m f = () |> not auto ? pprint o f
    4.11      fun pprint_v f = () |> verbose ? pprint o f
    4.12 @@ -989,7 +989,7 @@
    4.13             raise Interrupt
    4.14           else
    4.15             if passed_deadline deadline then
    4.16 -             (priority "Nitpick ran out of time."; ("unknown", state))
    4.17 +             (Output.urgent_message "Nitpick ran out of time."; ("unknown", state))
    4.18             else
    4.19               error "Nitpick was interrupted."
    4.20  
    4.21 @@ -1040,7 +1040,7 @@
    4.22      val t = state |> Proof.raw_goal |> #goal |> prop_of
    4.23    in
    4.24      case Logic.count_prems t of
    4.25 -      0 => (priority "No subgoal!"; ("none", state))
    4.26 +      0 => (Output.urgent_message "No subgoal!"; ("none", state))
    4.27      | n =>
    4.28        let
    4.29          val t = Logic.goal_params t i |> fst
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Oct 25 20:24:13 2010 +0200
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Oct 25 21:06:56 2010 +0200
     5.3 @@ -2054,7 +2054,7 @@
     5.4                      map (wf_constraint_for_triple rel) triples
     5.5                      |> foldr1 s_conj |> HOLogic.mk_Trueprop
     5.6           val _ = if debug then
     5.7 -                   priority ("Wellfoundedness goal: " ^
     5.8 +                   Output.urgent_message ("Wellfoundedness goal: " ^
     5.9                               Syntax.string_of_term ctxt prop ^ ".")
    5.10                   else
    5.11                     ()
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Oct 25 20:24:13 2010 +0200
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Oct 25 21:06:56 2010 +0200
     6.3 @@ -1043,7 +1043,7 @@
     6.4                                       (fn (s, []) => TFree (s, HOLogic.typeS)
     6.5                                         | x => TFree x))
     6.6         val _ = if debug then
     6.7 -                 priority ((if negate then "Genuineness" else "Spuriousness") ^
     6.8 +                 Output.urgent_message ((if negate then "Genuineness" else "Spuriousness") ^
     6.9                             " goal: " ^ Syntax.string_of_term ctxt prop ^ ".")
    6.10                 else
    6.11                   ()
     7.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Mon Oct 25 20:24:13 2010 +0200
     7.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Mon Oct 25 21:06:56 2010 +0200
     7.3 @@ -327,7 +327,7 @@
     7.4      fun try' j =
     7.5        if j <= i then
     7.6          let
     7.7 -          val _ = if quiet then () else priority ("Executing depth " ^ string_of_int j)
     7.8 +          val _ = if quiet then () else Output.urgent_message ("Executing depth " ^ string_of_int j)
     7.9          in
    7.10            case f j handle Match => (if quiet then ()
    7.11               else warning "Exception Match raised during quickcheck"; NONE)
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Oct 25 20:24:13 2010 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Oct 25 21:06:56 2010 +0200
     8.3 @@ -169,7 +169,7 @@
     8.4        sort_strings (available_atps thy) @ smt_prover_names
     8.5        |> List.partition (String.isPrefix remote_prefix)
     8.6    in
     8.7 -    priority ("Available provers: " ^ commas (local_provers @ remote_provers) ^
     8.8 +    Output.urgent_message ("Available provers: " ^ commas (local_provers @ remote_provers) ^
     8.9                ".")
    8.10    end
    8.11  
    8.12 @@ -481,7 +481,7 @@
    8.13        end
    8.14      else if blocking then
    8.15        let val (success, message) = TimeLimit.timeLimit timeout go () in
    8.16 -        List.app priority
    8.17 +        List.app Output.urgent_message
    8.18                   (Async_Manager.break_into_chunks [desc ^ "\n" ^ message]);
    8.19          (success, state)
    8.20        end
    8.21 @@ -497,7 +497,7 @@
    8.22    if null provers then
    8.23      error "No prover is set."
    8.24    else case subgoal_count state of
    8.25 -    0 => (priority "No subgoal!"; (false, state))
    8.26 +    0 => (Output.urgent_message "No subgoal!"; (false, state))
    8.27    | n =>
    8.28      let
    8.29        val _ = Proof.assert_backward state
    8.30 @@ -505,7 +505,7 @@
    8.31        val {context = ctxt, facts = chained_ths, goal} = Proof.goal state
    8.32        val (_, hyp_ts, concl_t) = strip_subgoal goal i
    8.33        val _ = () |> not blocking ? kill_provers
    8.34 -      val _ = if auto then () else priority "Sledgehammering..."
    8.35 +      val _ = if auto then () else Output.urgent_message "Sledgehammering..."
    8.36        val (smts, atps) = provers |> List.partition is_smt_prover
    8.37        fun run_provers full_types irrelevant_consts relevance_fudge
    8.38                        maybe_translate provers (res as (success, state)) =
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Mon Oct 25 20:24:13 2010 +0200
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Mon Oct 25 21:06:56 2010 +0200
     9.3 @@ -47,7 +47,7 @@
     9.4                 explicit_apply timeout i n state axioms =
     9.5    let
     9.6      val _ =
     9.7 -      priority ("Testing " ^ n_facts (map fst axioms) ^ "...")
     9.8 +      Output.urgent_message ("Testing " ^ n_facts (map fst axioms) ^ "...")
     9.9      val params =
    9.10        {blocking = true, debug = debug, verbose = verbose, overlord = overlord,
    9.11         provers = provers, full_types = full_types,
    9.12 @@ -62,7 +62,7 @@
    9.13         axioms = axioms, only = true}
    9.14      val result as {outcome, used_axioms, ...} = prover params (K "") problem
    9.15    in
    9.16 -    priority (case outcome of
    9.17 +    Output.urgent_message (case outcome of
    9.18                  SOME failure => string_for_failure failure
    9.19                | NONE =>
    9.20                  if length used_axioms = length axioms then "Found proof."
    9.21 @@ -94,7 +94,7 @@
    9.22      val thy = Proof.theory_of state
    9.23      val prover = get_prover thy false prover_name
    9.24      val msecs = Time.toMilliseconds timeout
    9.25 -    val _ = priority ("Sledgehammer minimize: " ^ quote prover_name ^ ".")
    9.26 +    val _ = Output.urgent_message ("Sledgehammer minimize: " ^ quote prover_name ^ ".")
    9.27      val {goal, ...} = Proof.goal state
    9.28      val (_, hyp_ts, concl_t) = strip_subgoal goal i
    9.29      val explicit_apply =
    9.30 @@ -115,7 +115,7 @@
    9.31             sublinear_minimize (do_test new_timeout)
    9.32                 (filter_used_axioms used_axioms axioms) ([], result)
    9.33           val n = length min_thms
    9.34 -         val _ = priority (cat_lines
    9.35 +         val _ = Output.urgent_message (cat_lines
    9.36             ["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^
    9.37              (case length (filter (curry (op =) Chained o snd o fst) min_thms) of
    9.38                 0 => ""
    9.39 @@ -145,10 +145,10 @@
    9.40              o name_thm_pairs_from_ref ctxt reserved chained_ths) refs
    9.41    in
    9.42      case subgoal_count state of
    9.43 -      0 => priority "No subgoal!"
    9.44 +      0 => Output.urgent_message "No subgoal!"
    9.45      | n =>
    9.46        (kill_provers ();
    9.47 -       priority (#2 (minimize_facts params i n state axioms)))
    9.48 +       Output.urgent_message (#2 (minimize_facts params i n state axioms)))
    9.49    end
    9.50  
    9.51  end;
    10.1 --- a/src/HOL/Tools/async_manager.ML	Mon Oct 25 20:24:13 2010 +0200
    10.2 +++ b/src/HOL/Tools/async_manager.ML	Mon Oct 25 21:06:56 2010 +0200
    10.3 @@ -105,7 +105,7 @@
    10.4      [] => ()
    10.5    | msgs as (tool, _) :: _ =>
    10.6      let val ss = break_into_chunks (map snd msgs) in
    10.7 -      List.app priority (tool ^ ": " ^ hd ss :: tl ss)
    10.8 +      List.app Output.urgent_message (tool ^ ": " ^ hd ss :: tl ss)
    10.9      end
   10.10  
   10.11  fun check_thread_manager () = Synchronized.change global_state
   10.12 @@ -185,7 +185,7 @@
   10.13                         if tool' = tool then SOME (th, (tool', Time.now (), desc))
   10.14                         else NONE) active
   10.15        val state' = make_state manager timeout_heap [] (killing @ canceling) messages store;
   10.16 -      val _ = if null killing then () else priority ("Killed active " ^ workers ^ ".")
   10.17 +      val _ = if null killing then () else Output.urgent_message ("Killed active " ^ workers ^ ".")
   10.18      in state' end);
   10.19  
   10.20  
   10.21 @@ -218,7 +218,7 @@
   10.22        case map_filter canceling_info canceling of
   10.23          [] => []
   10.24        | ss => "Trying to interrupt the following " ^ workers ^ ":" :: ss
   10.25 -  in priority (space_implode "\n\n" (running @ interrupting)) end
   10.26 +  in Output.urgent_message (space_implode "\n\n" (running @ interrupting)) end
   10.27  
   10.28  fun thread_messages tool worker opt_limit =
   10.29    let
   10.30 @@ -230,7 +230,7 @@
   10.31          (if length tool_store <= limit then ":"
   10.32           else " (" ^ string_of_int limit ^ " displayed):");
   10.33    in
   10.34 -    List.app priority (header :: break_into_chunks
   10.35 +    List.app Output.urgent_message (header :: break_into_chunks
   10.36                                       (map snd (#1 (chop limit tool_store))))
   10.37    end
   10.38  
    11.1 --- a/src/HOL/Tools/inductive_codegen.ML	Mon Oct 25 20:24:13 2010 +0200
    11.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Mon Oct 25 21:06:56 2010 +0200
    11.3 @@ -844,7 +844,7 @@
    11.4      val test_fn' = !test_fn;
    11.5      val dummy_report = ([], false)
    11.6      fun test k = (deepen bound (fn i =>
    11.7 -      (priority ("Search depth: " ^ string_of_int i);
    11.8 +      (Output.urgent_message ("Search depth: " ^ string_of_int i);
    11.9         test_fn' (i, values, k+offset))) start, dummy_report);
   11.10    in test end;
   11.11  
    12.1 --- a/src/HOL/Tools/refute.ML	Mon Oct 25 20:24:13 2010 +0200
    12.2 +++ b/src/HOL/Tools/refute.ML	Mon Oct 25 21:06:56 2010 +0200
    12.3 @@ -1133,31 +1133,31 @@
    12.4                              ". Available solvers: " ^
    12.5                              commas (map (quote o fst) (!SatSolver.solvers)) ^ ".")
    12.6            in
    12.7 -            priority "Invoking SAT solver...";
    12.8 +            Output.urgent_message "Invoking SAT solver...";
    12.9              (case solver fm of
   12.10                SatSolver.SATISFIABLE assignment =>
   12.11 -                (priority ("*** Model found: ***\n" ^ print_model ctxt model
   12.12 +                (Output.urgent_message ("*** Model found: ***\n" ^ print_model ctxt model
   12.13                    (fn i => case assignment i of SOME b => b | NONE => true));
   12.14                   if maybe_spurious then "potential" else "genuine")
   12.15              | SatSolver.UNSATISFIABLE _ =>
   12.16 -                (priority "No model exists.";
   12.17 +                (Output.urgent_message "No model exists.";
   12.18                  case next_universe universe sizes minsize maxsize of
   12.19                    SOME universe' => find_model_loop universe'
   12.20 -                | NONE => (priority
   12.21 -                  "Search terminated, no larger universe within the given limits.";
   12.22 -                  "none"))
   12.23 +                | NONE => (Output.urgent_message
   12.24 +                    "Search terminated, no larger universe within the given limits.";
   12.25 +                    "none"))
   12.26              | SatSolver.UNKNOWN =>
   12.27 -                (priority "No model found.";
   12.28 +                (Output.urgent_message "No model found.";
   12.29                  case next_universe universe sizes minsize maxsize of
   12.30                    SOME universe' => find_model_loop universe'
   12.31 -                | NONE           => (priority
   12.32 +                | NONE => (Output.urgent_message
   12.33                    "Search terminated, no larger universe within the given limits.";
   12.34                    "unknown"))) handle SatSolver.NOT_CONFIGURED =>
   12.35                (error ("SAT solver " ^ quote satsolver ^ " is not configured.");
   12.36                 "unknown")
   12.37            end
   12.38            handle MAXVARS_EXCEEDED =>
   12.39 -            (priority ("Search terminated, number of Boolean variables ("
   12.40 +            (Output.urgent_message ("Search terminated, number of Boolean variables ("
   12.41                ^ string_of_int maxvars ^ " allowed) exceeded.");
   12.42                "unknown")
   12.43  
   12.44 @@ -1179,14 +1179,14 @@
   12.45      maxtime>=0 orelse
   12.46        error ("\"maxtime\" is " ^ string_of_int maxtime ^ ", must be at least 0");
   12.47      (* enter loop with or without time limit *)
   12.48 -    priority ("Trying to find a model that "
   12.49 +    Output.urgent_message ("Trying to find a model that "
   12.50        ^ (if negate then "refutes" else "satisfies") ^ ": "
   12.51        ^ Syntax.string_of_term ctxt t);
   12.52      if maxtime > 0 then (
   12.53        TimeLimit.timeLimit (Time.fromSeconds maxtime)
   12.54          wrapper ()
   12.55        handle TimeLimit.TimeOut =>
   12.56 -        (priority ("Search terminated, time limit (" ^
   12.57 +        (Output.urgent_message ("Search terminated, time limit (" ^
   12.58              string_of_int maxtime
   12.59              ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.");
   12.60           check_expect "unknown")
   12.61 @@ -1273,7 +1273,7 @@
   12.62      val t = th |> prop_of
   12.63    in
   12.64      if Logic.count_prems t = 0 then
   12.65 -      priority "No subgoal!"
   12.66 +      Output.urgent_message "No subgoal!"
   12.67      else
   12.68        let
   12.69          val assms = map term_of (Assumption.all_assms_of ctxt)
    13.1 --- a/src/HOL/Tools/try.ML	Mon Oct 25 20:24:13 2010 +0200
    13.2 +++ b/src/HOL/Tools/try.ML	Mon Oct 25 21:06:56 2010 +0200
    13.3 @@ -96,7 +96,7 @@
    13.4                                      Pretty.markup Markup.hilite
    13.5                                                    [Pretty.str message]])
    13.6                      else
    13.7 -                      tap (fn _ => priority message)))
    13.8 +                      tap (fn _ => Output.urgent_message message)))
    13.9      end
   13.10  
   13.11  val invoke_try = fst oo do_try false
    14.1 --- a/src/Pure/General/output.ML	Mon Oct 25 20:24:13 2010 +0200
    14.2 +++ b/src/Pure/General/output.ML	Mon Oct 25 21:06:56 2010 +0200
    14.3 @@ -7,7 +7,6 @@
    14.4  signature BASIC_OUTPUT =
    14.5  sig
    14.6    val writeln: string -> unit
    14.7 -  val priority: string -> unit
    14.8    val tracing: string -> unit
    14.9    val warning: string -> unit
   14.10    val legacy_feature: string -> unit
   14.11 @@ -32,13 +31,14 @@
   14.12    val raw_stderr: output -> unit
   14.13    val raw_writeln: output -> unit
   14.14    val writeln_fn: (output -> unit) Unsynchronized.ref
   14.15 -  val priority_fn: (output -> unit) Unsynchronized.ref
   14.16 +  val urgent_message_fn: (output -> unit) Unsynchronized.ref
   14.17    val tracing_fn: (output -> unit) Unsynchronized.ref
   14.18    val warning_fn: (output -> unit) Unsynchronized.ref
   14.19    val error_fn: (output -> unit) Unsynchronized.ref
   14.20    val prompt_fn: (output -> unit) Unsynchronized.ref
   14.21    val status_fn: (output -> unit) Unsynchronized.ref
   14.22    val report_fn: (output -> unit) Unsynchronized.ref
   14.23 +  val urgent_message: string -> unit
   14.24    val error_msg: string -> unit
   14.25    val prompt: string -> unit
   14.26    val status: string -> unit
   14.27 @@ -86,7 +86,7 @@
   14.28  (* Isabelle output channels *)
   14.29  
   14.30  val writeln_fn = Unsynchronized.ref raw_writeln;
   14.31 -val priority_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
   14.32 +val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
   14.33  val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
   14.34  val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
   14.35  val error_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "*** ");
   14.36 @@ -95,7 +95,7 @@
   14.37  val report_fn = Unsynchronized.ref (fn _: string => ());
   14.38  
   14.39  fun writeln s = ! writeln_fn (output s);
   14.40 -fun priority s = ! priority_fn (output s);
   14.41 +fun urgent_message s = ! urgent_message_fn (output s);
   14.42  fun tracing s = ! tracing_fn (output s);
   14.43  fun warning s = ! warning_fn (output s);
   14.44  fun error_msg s = ! error_fn (output s);
    15.1 --- a/src/Pure/Isar/proof.ML	Mon Oct 25 20:24:13 2010 +0200
    15.2 +++ b/src/Pure/Isar/proof.ML	Mon Oct 25 21:06:56 2010 +0200
    15.3 @@ -972,7 +972,7 @@
    15.4        if ! testing then () else Proof_Display.print_results int ctxt res;
    15.5      fun print_rule ctxt th =
    15.6        if ! testing then rule := SOME th
    15.7 -      else if int then priority (Proof_Display.string_of_rule ctxt "Successful" th)
    15.8 +      else if int then Output.urgent_message (Proof_Display.string_of_rule ctxt "Successful" th)
    15.9        else ();
   15.10      val test_proof =
   15.11        try (local_skip_proof true)
    16.1 --- a/src/Pure/Isar/toplevel.ML	Mon Oct 25 20:24:13 2010 +0200
    16.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Oct 25 21:06:56 2010 +0200
    16.3 @@ -231,7 +231,8 @@
    16.4      (((fn () => body () handle exn => if Exn.is_interrupt exn then () else reraise exn)
    16.5          |> Runtime.debugging
    16.6          |> Runtime.toplevel_error
    16.7 -          (fn exn => priority ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
    16.8 +          (fn exn =>
    16.9 +            Output.urgent_message ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
   16.10        Simple_Thread.attributes interrupts);
   16.11  
   16.12  
    17.1 --- a/src/Pure/Proof/extraction.ML	Mon Oct 25 20:24:13 2010 +0200
    17.2 +++ b/src/Pure/Proof/extraction.ML	Mon Oct 25 21:06:56 2010 +0200
    17.3 @@ -119,7 +119,7 @@
    17.4  fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs));
    17.5  fun corr_name s vs = extr_name s vs ^ "_correctness";
    17.6  
    17.7 -fun msg d s = priority (Symbol.spaces d ^ s);
    17.8 +fun msg d s = Output.urgent_message (Symbol.spaces d ^ s);
    17.9  
   17.10  fun vars_of t = map Var (rev (Term.add_vars t []));
   17.11  fun frees_of t = map Free (rev (Term.add_frees t []));
    18.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Oct 25 20:24:13 2010 +0200
    18.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Oct 25 21:06:56 2010 +0200
    18.3 @@ -77,7 +77,7 @@
    18.4   (Output.writeln_fn := message "" "" "";
    18.5    Output.status_fn := (fn _ => ());
    18.6    Output.report_fn := (fn _ => ());
    18.7 -  Output.priority_fn := message (special "I") (special "J") "";
    18.8 +  Output.urgent_message_fn := message (special "I") (special "J") "";
    18.9    Output.tracing_fn := message (special "I" ^ special "V") (special "J") "";
   18.10    Output.warning_fn := message (special "K") (special "L") "### ";
   18.11    Output.error_fn := message (special "M") (special "N") "*** ";
   18.12 @@ -146,7 +146,7 @@
   18.13  
   18.14  (* restart top-level loop (keeps most state information) *)
   18.15  
   18.16 -val welcome = priority o Session.welcome;
   18.17 +val welcome = Output.urgent_message o Session.welcome;
   18.18  
   18.19  fun restart () =
   18.20   (sync_thy_loader ();
   18.21 @@ -227,7 +227,7 @@
   18.22            Output.default_output Output.default_escape;
   18.23           Markup.add_mode ProofGeneralPgip.proof_general_emacsN YXML.output_markup;
   18.24           setup_messages ();
   18.25 -         ProofGeneralPgip.pgip_channel_emacs (! Output.priority_fn);
   18.26 +         ProofGeneralPgip.pgip_channel_emacs (! Output.urgent_message_fn);
   18.27           setup_thy_loader ();
   18.28           setup_present_hook ();
   18.29           initialized := true);
    19.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Oct 25 20:24:13 2010 +0200
    19.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Oct 25 21:06:56 2010 +0200
    19.3 @@ -163,7 +163,7 @@
    19.4   (Output.writeln_fn := (fn s => normalmsg Message s);
    19.5    Output.status_fn := (fn _ => ());
    19.6    Output.report_fn := (fn _ => ());
    19.7 -  Output.priority_fn := (fn s => normalmsg Status s);
    19.8 +  Output.urgent_message_fn := (fn s => normalmsg Status s);
    19.9    Output.tracing_fn := (fn s => normalmsg Tracing s);
   19.10    Output.warning_fn := (fn s => errormsg Message Warning s);
   19.11    Output.error_fn := (fn s => errormsg Message Fatal s));
   19.12 @@ -231,7 +231,7 @@
   19.13  
   19.14  (* restart top-level loop (keeps most state information) *)
   19.15  
   19.16 -val welcome = priority o Session.welcome;
   19.17 +val welcome = Output.urgent_message o Session.welcome;
   19.18  
   19.19  fun restart () =
   19.20      (sync_thy_loader ();
   19.21 @@ -807,14 +807,15 @@
   19.22                                  PgipTypes.string_of_pgipurl url)
   19.23          | NONE => (openfile_retract filepath;
   19.24                     changecwd_dir filedir;
   19.25 -                   priority ("Working in file: " ^ PgipTypes.string_of_pgipurl url);
   19.26 +                   Output.urgent_message ("Working in file: " ^ PgipTypes.string_of_pgipurl url);
   19.27                     currently_open_file := SOME url)
   19.28    end
   19.29  
   19.30  fun closefile _ =
   19.31      case !currently_open_file of
   19.32          SOME f => (inform_file_processed f (Isar.state ());
   19.33 -                   priority ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f);
   19.34 +                   Output.urgent_message
   19.35 +                    ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f);
   19.36                     currently_open_file := NONE)
   19.37        | NONE => raise PGIP ("<closefile> when no file is open!")
   19.38  
   19.39 @@ -835,7 +836,7 @@
   19.40  fun abortfile _ =
   19.41      case !currently_open_file of
   19.42          SOME f => (isarcmd "init_toplevel";
   19.43 -                   priority ("Aborted working in file: " ^
   19.44 +                   Output.urgent_message ("Aborted working in file: " ^
   19.45                               PgipTypes.string_of_pgipurl f);
   19.46                     currently_open_file := NONE)
   19.47        | NONE => raise PGIP ("<abortfile> when no file is open!")
   19.48 @@ -846,7 +847,7 @@
   19.49      in
   19.50          case !currently_open_file of
   19.51              SOME f => raise PGIP ("<retractfile> when a file is open!")
   19.52 -          | NONE => (priority ("Retracting file: " ^ PgipTypes.string_of_pgipurl url);
   19.53 +          | NONE => (Output.urgent_message ("Retracting file: " ^ PgipTypes.string_of_pgipurl url);
   19.54                       (* TODO: next should be in thy loader, here just for testing *)
   19.55                       let
   19.56                           val name = thy_name url
    20.1 --- a/src/Pure/System/isabelle_process.ML	Mon Oct 25 20:24:13 2010 +0200
    20.2 +++ b/src/Pure/System/isabelle_process.ML	Mon Oct 25 21:06:56 2010 +0200
    20.3 @@ -106,14 +106,14 @@
    20.4      val _ = Simple_Thread.fork false (auto_flush TextIO.stdOut);
    20.5      val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr);
    20.6    in
    20.7 -    Output.status_fn   := standard_message out_stream false "B";
    20.8 -    Output.report_fn   := standard_message out_stream false "C";
    20.9 -    Output.writeln_fn  := standard_message out_stream true "D";
   20.10 -    Output.tracing_fn  := standard_message out_stream true "E";
   20.11 -    Output.warning_fn  := standard_message out_stream true "F";
   20.12 -    Output.error_fn    := standard_message out_stream true "G";
   20.13 -    Output.priority_fn := ! Output.writeln_fn;
   20.14 -    Output.prompt_fn   := ignore;
   20.15 +    Output.status_fn := standard_message out_stream false "B";
   20.16 +    Output.report_fn := standard_message out_stream false "C";
   20.17 +    Output.writeln_fn := standard_message out_stream true "D";
   20.18 +    Output.tracing_fn := standard_message out_stream true "E";
   20.19 +    Output.warning_fn := standard_message out_stream true "F";
   20.20 +    Output.error_fn := standard_message out_stream true "G";
   20.21 +    Output.urgent_message_fn := ! Output.writeln_fn;
   20.22 +    Output.prompt_fn := ignore;
   20.23      (in_stream, out_stream)
   20.24    end;
   20.25  
    21.1 --- a/src/Pure/Thy/thy_info.ML	Mon Oct 25 20:24:13 2010 +0200
    21.2 +++ b/src/Pure/Thy/thy_info.ML	Mon Oct 25 21:06:56 2010 +0200
    21.3 @@ -141,7 +141,7 @@
    21.4    else
    21.5      let
    21.6        val succs = thy_graph Graph.all_succs [name];
    21.7 -      val _ = priority (loader_msg "removing" succs);
    21.8 +      val _ = Output.urgent_message (loader_msg "removing" succs);
    21.9        val _ = List.app (perform Remove) succs;
   21.10        val _ = change_thys (Graph.del_nodes succs);
   21.11      in () end);
   21.12 @@ -222,7 +222,7 @@
   21.13  fun load_thy initiators update_time (deps: deps) text name parent_thys =
   21.14    let
   21.15      val _ = kill_thy name;
   21.16 -    val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators);
   21.17 +    val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
   21.18  
   21.19      val {master = (thy_path, _), ...} = deps;
   21.20      val dir = Path.dir thy_path;
   21.21 @@ -337,7 +337,7 @@
   21.22    in
   21.23      NAMED_CRITICAL "Thy_Info" (fn () =>
   21.24       (kill_thy name;
   21.25 -      priority ("Registering theory " ^ quote name);
   21.26 +      Output.urgent_message ("Registering theory " ^ quote name);
   21.27        map get_theory parents;
   21.28        change_thys (new_entry name parents (SOME deps, SOME theory));
   21.29        perform Update name))
    22.1 --- a/src/Tools/quickcheck.ML	Mon Oct 25 20:24:13 2010 +0200
    22.2 +++ b/src/Tools/quickcheck.ML	Mon Oct 25 21:06:56 2010 +0200
    22.3 @@ -188,8 +188,10 @@
    22.4            case iterate (fn () => tester (k - 1)) i empty_report
    22.5             of (NONE, report) => apsnd (cons report) (with_testers k testers)
    22.6              | (SOME q, report) => (SOME q, [report]);
    22.7 -    fun with_size k reports = if k > size then (NONE, reports)
    22.8 -      else (if quiet then () else priority ("Test data size: " ^ string_of_int k);
    22.9 +    fun with_size k reports =
   22.10 +      if k > size then (NONE, reports)
   22.11 +      else
   22.12 +       (if quiet then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
   22.13          let
   22.14            val (result, new_report) = with_testers k testers
   22.15            val reports = ((k, new_report) :: reports)
    23.1 --- a/src/Tools/solve_direct.ML	Mon Oct 25 20:24:13 2010 +0200
    23.2 +++ b/src/Tools/solve_direct.ML	Mon Oct 25 21:06:56 2010 +0200
    23.3 @@ -84,7 +84,7 @@
    23.4                     Pretty.markup Markup.hilite (message results)])
    23.5              else
    23.6                tap (fn _ =>
    23.7 -                priority (Pretty.string_of (Pretty.chunks (message results))))))
    23.8 +                Output.urgent_message (Pretty.string_of (Pretty.chunks (message results))))))
    23.9      | _ => (false, state))
   23.10    end;
   23.11