--- a/doc-src/IsarImplementation/Thy/Integration.thy Tue Oct 26 11:20:14 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Integration.thy Tue Oct 26 11:23:27 2010 +0200
@@ -92,7 +92,7 @@
\item @{ML "Toplevel.timing := true"} makes the toplevel print timing
information for each Isar command being executed.
- \item @{ML Toplevel.profiling}~@{verbatim ":="}~@{text "n"} controls
+ \item @{ML Toplevel.profiling}~@{ML_text ":="}~@{text "n"} controls
low-level profiling of the underlying ML runtime system. For
Poly/ML, @{text "n = 1"} means time and @{text "n = 2"} space
profiling.
@@ -260,7 +260,7 @@
@{index_ML Thy_Info.get_theory: "string -> theory"} \\
@{index_ML Thy_Info.remove_thy: "string -> unit"} \\[1ex]
@{index_ML Thy_Info.register_thy: "theory -> unit"} \\[1ex]
- @{verbatim "datatype action = Update | Remove"} \\
+ @{ML_text "datatype action = Update | Remove"} \\
@{index_ML Thy_Info.add_hook: "(Thy_Info.action -> string -> unit) -> unit"} \\
\end{mldecls}
--- a/doc-src/IsarImplementation/Thy/Isar.thy Tue Oct 26 11:20:14 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Isar.thy Tue Oct 26 11:23:27 2010 +0200
@@ -361,7 +361,7 @@
\medskip The following toy examples illustrate how the goal facts
and state are passed to proof methods. The pre-defined proof method
called ``@{method tactic}'' wraps ML source of type @{ML_type
- tactic} (abstracted over @{verbatim facts}). This allows immediate
+ tactic} (abstracted over @{ML_text facts}). This allows immediate
experimentation without parsing of concrete syntax. *}
example_proof
@@ -398,7 +398,7 @@
The @{ML Attrib.thms} parser produces a list of theorems from the
usual Isar syntax involving attribute expressions etc.\ (syntax
category @{syntax thmrefs}) \cite{isabelle-isar-ref}. The resulting
- @{verbatim thms} are added to @{ML HOL_basic_ss} which already
+ @{ML_text thms} are added to @{ML HOL_basic_ss} which already
contains the basic Simplifier setup for HOL.
The tactic @{ML asm_full_simp_tac} is the one that is also used in
--- a/doc-src/IsarImplementation/Thy/ML.thy Tue Oct 26 11:20:14 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy Tue Oct 26 11:23:27 2010 +0200
@@ -112,14 +112,14 @@
\medskip
\begin{tabular}{lll}
variant & example & ML categories \\\hline
- lower-case & @{verbatim foo_bar} & values, types, record fields \\
- capitalized & @{verbatim Foo_Bar} & datatype constructors, structures, functors \\
- upper-case & @{verbatim FOO_BAR} & special values, exception constructors, signatures \\
+ lower-case & @{ML_text foo_bar} & values, types, record fields \\
+ capitalized & @{ML_text Foo_Bar} & datatype constructors, structures, functors \\
+ upper-case & @{ML_text FOO_BAR} & special values, exception constructors, signatures \\
\end{tabular}
\medskip
For historical reasons, many capitalized names omit underscores,
- e.g.\ old-style @{verbatim FooBar} instead of @{verbatim Foo_Bar}.
+ e.g.\ old-style @{ML_text FooBar} instead of @{ML_text Foo_Bar}.
Genuine mixed-case names are \emph{not} used, bacause clear division
of words is essential for readability.\footnote{Camel-case was
invented to workaround the lack of underscore in some early
@@ -128,12 +128,12 @@
A single (capital) character does not count as ``word'' in this
respect: some Isabelle/ML names are suffixed by extra markers like
- this: @{verbatim foo_barT}.
+ this: @{ML_text foo_barT}.
- Name variants are produced by adding 1--3 primes, e.g.\ @{verbatim
- foo'}, @{verbatim foo''}, or @{verbatim foo'''}, but not @{verbatim
+ Name variants are produced by adding 1--3 primes, e.g.\ @{ML_text
+ foo'}, @{ML_text foo''}, or @{ML_text foo'''}, but not @{ML_text
foo''''} or more. Decimal digits scale better to larger numbers,
- e.g.\ @{verbatim foo0}, @{verbatim foo1}, @{verbatim foo42}.
+ e.g.\ @{ML_text foo0}, @{ML_text foo1}, @{ML_text foo42}.
\paragraph{Scopes.} Apart from very basic library modules, ML
structures are not ``opened'', but names are referenced with
@@ -147,7 +147,7 @@
Local names of function abstraction or case/let bindings are
typically shorter, sometimes using only rudiments of ``words'',
while still avoiding cryptic shorthands. An auxiliary function
- called @{verbatim helper}, @{verbatim aux}, or @{verbatim f} is
+ called @{ML_text helper}, @{ML_text aux}, or @{ML_text f} is
considered bad style.
Example:
@@ -187,18 +187,18 @@
\begin{itemize}
- \item A function that maps @{verbatim foo} to @{verbatim bar} is
- called @{verbatim foo_to_bar} or @{verbatim bar_of_foo} (never
- @{verbatim foo2bar}, @{verbatim bar_from_foo}, @{verbatim
- bar_for_foo}, or @{verbatim bar4foo}).
+ \item A function that maps @{ML_text foo} to @{ML_text bar} is
+ called @{ML_text foo_to_bar} or @{ML_text bar_of_foo} (never
+ @{ML_text foo2bar}, @{ML_text bar_from_foo}, @{ML_text
+ bar_for_foo}, or @{ML_text bar4foo}).
- \item The name component @{verbatim legacy} means that the operation
+ \item The name component @{ML_text legacy} means that the operation
is about to be discontinued soon.
- \item The name component @{verbatim old} means that this is historic
+ \item The name component @{ML_text old} means that this is historic
material that might disappear at some later stage.
- \item The name component @{verbatim global} means that this works
+ \item The name component @{ML_text global} means that this works
with the background theory instead of the regular local context
(\secref{sec:context}), sometimes for historical reasons, sometimes
due a genuine lack of locality of the concept involved, sometimes as
@@ -213,23 +213,23 @@
\begin{itemize}
- \item theories are called @{verbatim thy}, rarely @{verbatim theory}
- (never @{verbatim thry})
+ \item theories are called @{ML_text thy}, rarely @{ML_text theory}
+ (never @{ML_text thry})
- \item proof contexts are called @{verbatim ctxt}, rarely @{verbatim
- context} (never @{verbatim ctx})
+ \item proof contexts are called @{ML_text ctxt}, rarely @{ML_text
+ context} (never @{ML_text ctx})
- \item generic contexts are called @{verbatim context}, rarely
- @{verbatim ctxt}
+ \item generic contexts are called @{ML_text context}, rarely
+ @{ML_text ctxt}
- \item local theories are called @{verbatim lthy}, except for local
+ \item local theories are called @{ML_text lthy}, except for local
theories that are treated as proof context (which is a semantic
super-type)
\end{itemize}
Variations with primed or decimal numbers are always possible, as
- well as sematic prefixes like @{verbatim foo_thy} or @{verbatim
+ well as sematic prefixes like @{ML_text foo_thy} or @{ML_text
bar_ctxt}, but the base conventions above need to be preserved.
This allows to visualize the their data flow via plain regular
expressions in the editor.
@@ -239,28 +239,28 @@
\begin{itemize}
- \item sorts are called @{verbatim S}
+ \item sorts are called @{ML_text S}
- \item types are called @{verbatim T}, @{verbatim U}, or @{verbatim
- ty} (never @{verbatim t})
+ \item types are called @{ML_text T}, @{ML_text U}, or @{ML_text
+ ty} (never @{ML_text t})
- \item terms are called @{verbatim t}, @{verbatim u}, or @{verbatim
- tm} (never @{verbatim trm})
+ \item terms are called @{ML_text t}, @{ML_text u}, or @{ML_text
+ tm} (never @{ML_text trm})
- \item certified types are called @{verbatim cT}, rarely @{verbatim
+ \item certified types are called @{ML_text cT}, rarely @{ML_text
T}, with variants as for types
- \item certified terms are called @{verbatim ct}, rarely @{verbatim
+ \item certified terms are called @{ML_text ct}, rarely @{ML_text
t}, with variants as for terms
- \item theorems are called @{verbatim th}, or @{verbatim thm}
+ \item theorems are called @{ML_text th}, or @{ML_text thm}
\end{itemize}
Proper semantic names override these conventions completely. For
example, the left-hand side of an equation (as a term) can be called
- @{verbatim lhs} (not @{verbatim lhs_tm}). Or a term that is known
- to be a variable can be called @{verbatim v} or @{verbatim x}.
+ @{ML_text lhs} (not @{ML_text lhs_tm}). Or a term that is known
+ to be a variable can be called @{ML_text v} or @{ML_text x}.
\end{itemize}
*}
@@ -309,17 +309,17 @@
c);
\end{verbatim}
- Some special infixes (e.g.\ @{verbatim "|>"}) work better at the
+ Some special infixes (e.g.\ @{ML_text "|>"}) work better at the
start of the line, but punctuation is always at the end.
Function application follows the tradition of @{text "\<lambda>"}-calculus,
- not informal mathematics. For example: @{verbatim "f a b"} for a
- curried function, or @{verbatim "g (a, b)"} for a tupled function.
- Note that the space between @{verbatim g} and the pair @{verbatim
+ not informal mathematics. For example: @{ML_text "f a b"} for a
+ curried function, or @{ML_text "g (a, b)"} for a tupled function.
+ Note that the space between @{ML_text g} and the pair @{ML_text
"(a, b)"} follows the important principle of
- \emph{compositionality}: the layout of @{verbatim "g p"} does not
- change when @{verbatim "p"} is refined to the concrete pair
- @{verbatim "(a, b)"}.
+ \emph{compositionality}: the layout of @{ML_text "g p"} does not
+ change when @{ML_text "p"} is refined to the concrete pair
+ @{ML_text "(a, b)"}.
\paragraph{Indentation} uses plain spaces, never hard
tabulators.\footnote{Tabulators were invented to move the carriage
@@ -366,13 +366,13 @@
avoided.
\paragraph{Complex expressions} that consist of multi-clausal
- function definitions, @{verbatim handle}, @{verbatim case},
- @{verbatim let} (and combinations) require special attention. The
+ function definitions, @{ML_text handle}, @{ML_text case},
+ @{ML_text let} (and combinations) require special attention. The
syntax of Standard ML is quite ambitious and admits a lot of
variance that can distort the meaning of the text.
- Clauses of @{verbatim fun}, @{verbatim fn}, @{verbatim handle},
- @{verbatim case} get extra indentation to indicate the nesting
+ Clauses of @{ML_text fun}, @{ML_text fn}, @{ML_text handle},
+ @{ML_text case} get extra indentation to indicate the nesting
clearly. Example:
\begin{verbatim}
@@ -392,7 +392,7 @@
expr2
\end{verbatim}
- Body expressions consisting of @{verbatim case} or @{verbatim let}
+ Body expressions consisting of @{ML_text case} or @{ML_text let}
require care to maintain compositionality, to prevent loss of
logical indentation where it is especially important to see the
structure of the text. Example:
@@ -425,7 +425,7 @@
end
\end{verbatim}
- Extra parentheses around @{verbatim case} expressions are optional,
+ Extra parentheses around @{ML_text case} expressions are optional,
but help to analyse the nesting based on character matching in the
editor.
@@ -434,7 +434,7 @@
\begin{enumerate}
- \item @{verbatim "if"} expressions are iterated as if there would be
+ \item @{ML_text "if"} expressions are iterated as if there would be
a multi-branch conditional in SML, e.g.
\begin{verbatim}
@@ -445,7 +445,7 @@
else e3
\end{verbatim}
- \item @{verbatim fn} abstractions are often layed-out as if they
+ \item @{ML_text fn} abstractions are often layed-out as if they
would lack any structure by themselves. This traditional form is
motivated by the possibility to shift function arguments back and
forth wrt.\ additional combinators. Example:
@@ -457,13 +457,13 @@
expr)
\end{verbatim}
- Here the visual appearance is that of three arguments @{verbatim x},
- @{verbatim y}, @{verbatim z}.
+ Here the visual appearance is that of three arguments @{ML_text x},
+ @{ML_text y}, @{ML_text z}.
\end{enumerate}
Such weakly structured layout should be use with great care. Here
- is a counter-example involving @{verbatim let} expressions:
+ is a counter-example involving @{ML_text let} expressions:
\begin{verbatim}
(* WRONG *)
@@ -945,7 +945,7 @@
again.
The incremental @{ML add_content} avoids this by operating on a
- buffer that is passed through in a linear fashion. Using @{verbatim
+ buffer that is passed through in a linear fashion. Using @{ML_text
"#>"} and contraction over the actual buffer argument saves some
additional boiler-plate. Of course, the two @{ML "Buffer.add"}
invocations with concatenated strings could have been split into
@@ -1106,7 +1106,7 @@
Traditionally, the (short) exception message would include the name
of an ML function, although this is no longer necessary, because the
ML runtime system prints a detailed source position of the
- corresponding @{verbatim raise} keyword.
+ corresponding @{ML_text raise} keyword.
\medskip User modules can always introduce their own custom
exceptions locally, e.g.\ to organize internal failures robustly
@@ -1163,8 +1163,8 @@
\item @{ML try}~@{text "f x"} makes the partiality of evaluating
@{text "f x"} explicit via the option datatype. Interrupts are
\emph{not} handled here, i.e.\ this form serves as safe replacement
- for the \emph{unsafe} version @{verbatim "(SOME"}~@{text "f
- x"}~@{verbatim "handle _ => NONE)"} that is occasionally seen in
+ for the \emph{unsafe} version @{ML_text "(SOME"}~@{text "f
+ x"}~@{ML_text "handle _ => NONE)"} that is occasionally seen in
books about SML.
\item @{ML can} is similar to @{ML try} with more abstract result.
@@ -1183,8 +1183,8 @@
while preserving its implicit position information (if possible,
depending on the ML platform).
- \item @{ML exception_trace}~@{verbatim "(fn () =>"}~@{text
- "e"}@{verbatim ")"} evaluates expression @{text "e"} while printing
+ \item @{ML exception_trace}~@{ML_text "(fn () =>"}~@{text
+ "e"}@{ML_text ")"} evaluates expression @{text "e"} while printing
a full trace of its stack of nested exceptions (if possible,
depending on the ML platform).\footnote{In versions of Poly/ML the
trace will appear on raw stdout of the Isabelle process.}
--- a/src/HOL/Mutabelle/MutabelleExtra.thy Tue Oct 26 11:20:14 2010 +0200
+++ b/src/HOL/Mutabelle/MutabelleExtra.thy Tue Oct 26 11:23:27 2010 +0200
@@ -19,10 +19,11 @@
"mutabelle_extra.ML"
begin
-ML {* val old_tr = !Output.tracing_fn *}
-ML {* val old_wr = !Output.writeln_fn *}
-ML {* val old_pr = !Output.priority_fn *}
-ML {* val old_wa = !Output.warning_fn *}
+(* FIXME !?!?! *)
+ML {* val old_tr = !Output.Private_Hooks.tracing_fn *}
+ML {* val old_wr = !Output.Private_Hooks.writeln_fn *}
+ML {* val old_ur = !Output.Private_Hooks.urgent_message_fn *}
+ML {* val old_wa = !Output.Private_Hooks.warning_fn *}
quickcheck_params [size = 5, iterations = 1000]
(*
@@ -48,9 +49,10 @@
*)
*}
-ML {* Output.tracing_fn := old_tr *}
-ML {* Output.writeln_fn := old_wr *}
-ML {* Output.priority_fn := old_pr *}
-ML {* Output.warning_fn := old_wa *}
+(* FIXME !?!?! *)
+ML {* Output.Private_Hooks.tracing_fn := old_tr *}
+ML {* Output.Private_Hooks.writeln_fn := old_wr *}
+ML {* Output.Private_Hooks.urgent_message_fn := old_ur *}
+ML {* Output.Private_Hooks.warning_fn := old_wa *}
end
--- a/src/HOL/Mutabelle/mutabelle.ML Tue Oct 26 11:20:14 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle.ML Tue Oct 26 11:23:27 2010 +0200
@@ -499,14 +499,14 @@
fun is_executable thy insts th =
(Quickcheck.test_term
(ProofContext.init_global thy) false (SOME (!testgen_name)) 1 1 (preprocess thy insts (prop_of th));
- priority "executable"; true) handle ERROR s =>
- (priority ("not executable: " ^ s); false);
+ Output.urgent_message "executable"; true) handle ERROR s =>
+ (Output.urgent_message ("not executable: " ^ s); false);
fun qc_recursive usedthy [] insts sz qciter acc = rev acc
| qc_recursive usedthy (x::xs) insts sz qciter acc = qc_recursive usedthy xs insts sz qciter
- (priority ("qc_recursive: " ^ string_of_int (length xs)); ((x, pretty (the_default [] (Quickcheck.test_term
+ (Output.urgent_message ("qc_recursive: " ^ string_of_int (length xs)); ((x, pretty (the_default [] (Quickcheck.test_term
(ProofContext.init_global usedthy) false (SOME (!testgen_name)) sz qciter (preprocess usedthy insts x)))) :: acc))
- handle ERROR msg => (priority msg; qc_recursive usedthy xs insts sz qciter acc);
+ handle ERROR msg => (Output.urgent_message msg; qc_recursive usedthy xs insts sz qciter acc);
(*quickcheck-test the mutants created by function mutate with type-instantiation insts,
@@ -721,11 +721,11 @@
fun mutqc_thystat option p mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename =
let
val thmlist = filter
- (fn (s, th) => not (p s th) andalso (priority s; is_executable mutthy insts th)) (thms_of mutthy)
+ (fn (s, th) => not (p s th) andalso (Output.urgent_message s; is_executable mutthy insts th)) (thms_of mutthy)
fun mutthmrec [] = ()
| mutthmrec ((name,thm)::xs) =
let
- val _ = priority ("mutthmrec: " ^ name);
+ val _ = Output.urgent_message ("mutthmrec: " ^ name);
val mutated = mutate option (prop_of thm) usedthy
commutatives forbidden_funs iter
val (passednum,_,cenum,_) = qc_test mutated insts usedthy sz qciter
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Tue Oct 26 11:20:14 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Tue Oct 26 11:23:27 2010 +0200
@@ -109,7 +109,7 @@
fun invoke_refute thy t =
let
val res = MyRefute.refute_term thy [] t
- val _ = priority ("Refute: " ^ res)
+ val _ = Output.urgent_message ("Refute: " ^ res)
in
case res of
"genuine" => GenuineCex
@@ -137,7 +137,7 @@
in
let
val (res, _) = Nitpick.pick_nits_in_term state (Nitpick_Isar.default_params thy []) false [] t
- val _ = priority ("Nitpick: " ^ res)
+ val _ = Output.urgent_message ("Nitpick: " ^ res)
in
case res of
"genuine" => GenuineCex
@@ -182,7 +182,7 @@
(error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^
"."))
| Exn.Interrupt => raise Exn.Interrupt
- | _ => (priority ("Unknown error in Nitpick"); Error)
+ | _ => (Output.urgent_message ("Unknown error in Nitpick"); Error)
end
val nitpick_mtd = ("nitpick", invoke_nitpick)
*)
@@ -281,13 +281,13 @@
fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t =
let
- val _ = priority ("Invoking " ^ mtd_name)
+ val _ = Output.urgent_message ("Invoking " ^ mtd_name)
val ((res, (timing, reports)), time) = cpu_time "total time"
(fn () => case try (invoke_mtd thy) t of
SOME (res, (timing, reports)) => (res, (timing, reports))
- | NONE => (priority ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
+ | NONE => (Output.urgent_message ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
(Error , ([], NONE))))
- val _ = priority (" Done")
+ val _ = Output.urgent_message (" Done")
in (res, (time :: timing, reports)) end
(* theory -> term list -> mtd -> subentry *)
@@ -316,7 +316,7 @@
fun mutate_theorem create_entry thy mtds thm =
let
val exec = is_executable_thm thy thm
- val _ = priority (if exec then "EXEC" else "NOEXEC")
+ val _ = Output.urgent_message (if exec then "EXEC" else "NOEXEC")
val mutants =
(if num_mutations = 0 then
[Thm.prop_of thm]
@@ -327,7 +327,7 @@
val mutants =
if exec then
let
- val _ = priority ("BEFORE PARTITION OF " ^
+ val _ = Output.urgent_message ("BEFORE PARTITION OF " ^
Int.toString (length mutants) ^ " MUTANTS")
val (execs, noexecs) = List.partition (is_executable_term thy) (take_random (20 * max_mutants) mutants)
val _ = tracing ("AFTER PARTITION (" ^ Int.toString (length execs) ^
@@ -342,7 +342,7 @@
|> map Mutabelle.freeze |> map freezeT
(* |> filter (not o is_forbidden_mutant) *)
|> List.mapPartial (try (Sign.cert_term thy))
- val _ = map (fn t => priority ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
+ val _ = map (fn t => Output.urgent_message ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
in
create_entry thy thm exec mutants mtds
end
@@ -421,7 +421,7 @@
(* theory -> mtd list -> thm list -> string -> unit *)
fun mutate_theorems_and_write_report thy mtds thms file_name =
let
- val _ = priority "Starting Mutabelle..."
+ val _ = Output.urgent_message "Starting Mutabelle..."
val path = Path.explode file_name
(* for normal report: *)
(*val (gen_create_entry, gen_string_for_entry) = (create_entry, string_for_entry)*)
--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Oct 26 11:20:14 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Oct 26 11:23:27 2010 +0200
@@ -216,7 +216,7 @@
o Pretty.chunks o cons (Pretty.str "") o single
o Pretty.mark Markup.hilite
else
- (fn s => (priority s; if debug then tracing s else ()))
+ (fn s => (Output.urgent_message s; if debug then tracing s else ()))
o Pretty.string_of
fun pprint_m f = () |> not auto ? pprint o f
fun pprint_v f = () |> verbose ? pprint o f
@@ -989,7 +989,7 @@
raise Interrupt
else
if passed_deadline deadline then
- (priority "Nitpick ran out of time."; ("unknown", state))
+ (Output.urgent_message "Nitpick ran out of time."; ("unknown", state))
else
error "Nitpick was interrupted."
@@ -1040,7 +1040,7 @@
val t = state |> Proof.raw_goal |> #goal |> prop_of
in
case Logic.count_prems t of
- 0 => (priority "No subgoal!"; ("none", state))
+ 0 => (Output.urgent_message "No subgoal!"; ("none", state))
| n =>
let
val t = Logic.goal_params t i |> fst
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Oct 26 11:20:14 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Oct 26 11:23:27 2010 +0200
@@ -2054,7 +2054,7 @@
map (wf_constraint_for_triple rel) triples
|> foldr1 s_conj |> HOLogic.mk_Trueprop
val _ = if debug then
- priority ("Wellfoundedness goal: " ^
+ Output.urgent_message ("Wellfoundedness goal: " ^
Syntax.string_of_term ctxt prop ^ ".")
else
()
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Oct 26 11:20:14 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Oct 26 11:23:27 2010 +0200
@@ -1043,7 +1043,7 @@
(fn (s, []) => TFree (s, HOLogic.typeS)
| x => TFree x))
val _ = if debug then
- priority ((if negate then "Genuineness" else "Spuriousness") ^
+ Output.urgent_message ((if negate then "Genuineness" else "Spuriousness") ^
" goal: " ^ Syntax.string_of_term ctxt prop ^ ".")
else
()
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Tue Oct 26 11:20:14 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Tue Oct 26 11:23:27 2010 +0200
@@ -327,7 +327,7 @@
fun try' j =
if j <= i then
let
- val _ = if quiet then () else priority ("Executing depth " ^ string_of_int j)
+ val _ = if quiet then () else Output.urgent_message ("Executing depth " ^ string_of_int j)
in
case f j handle Match => (if quiet then ()
else warning "Exception Match raised during quickcheck"; NONE)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Oct 26 11:20:14 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Oct 26 11:23:27 2010 +0200
@@ -169,7 +169,7 @@
sort_strings (available_atps thy) @ smt_prover_names
|> List.partition (String.isPrefix remote_prefix)
in
- priority ("Available provers: " ^ commas (local_provers @ remote_provers) ^
+ Output.urgent_message ("Available provers: " ^ commas (local_provers @ remote_provers) ^
".")
end
@@ -481,7 +481,7 @@
end
else if blocking then
let val (success, message) = TimeLimit.timeLimit timeout go () in
- List.app priority
+ List.app Output.urgent_message
(Async_Manager.break_into_chunks [desc ^ "\n" ^ message]);
(success, state)
end
@@ -497,7 +497,7 @@
if null provers then
error "No prover is set."
else case subgoal_count state of
- 0 => (priority "No subgoal!"; (false, state))
+ 0 => (Output.urgent_message "No subgoal!"; (false, state))
| n =>
let
val _ = Proof.assert_backward state
@@ -505,7 +505,7 @@
val {context = ctxt, facts = chained_ths, goal} = Proof.goal state
val (_, hyp_ts, concl_t) = strip_subgoal goal i
val _ = () |> not blocking ? kill_provers
- val _ = if auto then () else priority "Sledgehammering..."
+ val _ = if auto then () else Output.urgent_message "Sledgehammering..."
val (smts, atps) = provers |> List.partition is_smt_prover
fun run_provers full_types irrelevant_consts relevance_fudge
maybe_translate provers (res as (success, state)) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Oct 26 11:20:14 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Oct 26 11:23:27 2010 +0200
@@ -47,7 +47,7 @@
explicit_apply timeout i n state axioms =
let
val _ =
- priority ("Testing " ^ n_facts (map fst axioms) ^ "...")
+ Output.urgent_message ("Testing " ^ n_facts (map fst axioms) ^ "...")
val params =
{blocking = true, debug = debug, verbose = verbose, overlord = overlord,
provers = provers, full_types = full_types,
@@ -62,7 +62,7 @@
axioms = axioms, only = true}
val result as {outcome, used_axioms, ...} = prover params (K "") problem
in
- priority (case outcome of
+ Output.urgent_message (case outcome of
SOME failure => string_for_failure failure
| NONE =>
if length used_axioms = length axioms then "Found proof."
@@ -94,7 +94,7 @@
val thy = Proof.theory_of state
val prover = get_prover thy false prover_name
val msecs = Time.toMilliseconds timeout
- val _ = priority ("Sledgehammer minimize: " ^ quote prover_name ^ ".")
+ val _ = Output.urgent_message ("Sledgehammer minimize: " ^ quote prover_name ^ ".")
val {goal, ...} = Proof.goal state
val (_, hyp_ts, concl_t) = strip_subgoal goal i
val explicit_apply =
@@ -115,7 +115,7 @@
sublinear_minimize (do_test new_timeout)
(filter_used_axioms used_axioms axioms) ([], result)
val n = length min_thms
- val _ = priority (cat_lines
+ val _ = Output.urgent_message (cat_lines
["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^
(case length (filter (curry (op =) Chained o snd o fst) min_thms) of
0 => ""
@@ -145,10 +145,10 @@
o name_thm_pairs_from_ref ctxt reserved chained_ths) refs
in
case subgoal_count state of
- 0 => priority "No subgoal!"
+ 0 => Output.urgent_message "No subgoal!"
| n =>
(kill_provers ();
- priority (#2 (minimize_facts params i n state axioms)))
+ Output.urgent_message (#2 (minimize_facts params i n state axioms)))
end
end;
--- a/src/HOL/Tools/async_manager.ML Tue Oct 26 11:20:14 2010 +0200
+++ b/src/HOL/Tools/async_manager.ML Tue Oct 26 11:23:27 2010 +0200
@@ -105,7 +105,7 @@
[] => ()
| msgs as (tool, _) :: _ =>
let val ss = break_into_chunks (map snd msgs) in
- List.app priority (tool ^ ": " ^ hd ss :: tl ss)
+ List.app Output.urgent_message (tool ^ ": " ^ hd ss :: tl ss)
end
fun check_thread_manager () = Synchronized.change global_state
@@ -185,7 +185,7 @@
if tool' = tool then SOME (th, (tool', Time.now (), desc))
else NONE) active
val state' = make_state manager timeout_heap [] (killing @ canceling) messages store;
- val _ = if null killing then () else priority ("Killed active " ^ workers ^ ".")
+ val _ = if null killing then () else Output.urgent_message ("Killed active " ^ workers ^ ".")
in state' end);
@@ -218,7 +218,7 @@
case map_filter canceling_info canceling of
[] => []
| ss => "Trying to interrupt the following " ^ workers ^ ":" :: ss
- in priority (space_implode "\n\n" (running @ interrupting)) end
+ in Output.urgent_message (space_implode "\n\n" (running @ interrupting)) end
fun thread_messages tool worker opt_limit =
let
@@ -230,7 +230,7 @@
(if length tool_store <= limit then ":"
else " (" ^ string_of_int limit ^ " displayed):");
in
- List.app priority (header :: break_into_chunks
+ List.app Output.urgent_message (header :: break_into_chunks
(map snd (#1 (chop limit tool_store))))
end
--- a/src/HOL/Tools/inductive_codegen.ML Tue Oct 26 11:20:14 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Tue Oct 26 11:23:27 2010 +0200
@@ -844,7 +844,7 @@
val test_fn' = !test_fn;
val dummy_report = ([], false)
fun test k = (deepen bound (fn i =>
- (priority ("Search depth: " ^ string_of_int i);
+ (Output.urgent_message ("Search depth: " ^ string_of_int i);
test_fn' (i, values, k+offset))) start, dummy_report);
in test end;
--- a/src/HOL/Tools/refute.ML Tue Oct 26 11:20:14 2010 +0200
+++ b/src/HOL/Tools/refute.ML Tue Oct 26 11:23:27 2010 +0200
@@ -1133,31 +1133,31 @@
". Available solvers: " ^
commas (map (quote o fst) (!SatSolver.solvers)) ^ ".")
in
- priority "Invoking SAT solver...";
+ Output.urgent_message "Invoking SAT solver...";
(case solver fm of
SatSolver.SATISFIABLE assignment =>
- (priority ("*** Model found: ***\n" ^ print_model ctxt model
+ (Output.urgent_message ("*** Model found: ***\n" ^ print_model ctxt model
(fn i => case assignment i of SOME b => b | NONE => true));
if maybe_spurious then "potential" else "genuine")
| SatSolver.UNSATISFIABLE _ =>
- (priority "No model exists.";
+ (Output.urgent_message "No model exists.";
case next_universe universe sizes minsize maxsize of
SOME universe' => find_model_loop universe'
- | NONE => (priority
- "Search terminated, no larger universe within the given limits.";
- "none"))
+ | NONE => (Output.urgent_message
+ "Search terminated, no larger universe within the given limits.";
+ "none"))
| SatSolver.UNKNOWN =>
- (priority "No model found.";
+ (Output.urgent_message "No model found.";
case next_universe universe sizes minsize maxsize of
SOME universe' => find_model_loop universe'
- | NONE => (priority
+ | NONE => (Output.urgent_message
"Search terminated, no larger universe within the given limits.";
"unknown"))) handle SatSolver.NOT_CONFIGURED =>
(error ("SAT solver " ^ quote satsolver ^ " is not configured.");
"unknown")
end
handle MAXVARS_EXCEEDED =>
- (priority ("Search terminated, number of Boolean variables ("
+ (Output.urgent_message ("Search terminated, number of Boolean variables ("
^ string_of_int maxvars ^ " allowed) exceeded.");
"unknown")
@@ -1179,14 +1179,14 @@
maxtime>=0 orelse
error ("\"maxtime\" is " ^ string_of_int maxtime ^ ", must be at least 0");
(* enter loop with or without time limit *)
- priority ("Trying to find a model that "
+ Output.urgent_message ("Trying to find a model that "
^ (if negate then "refutes" else "satisfies") ^ ": "
^ Syntax.string_of_term ctxt t);
if maxtime > 0 then (
TimeLimit.timeLimit (Time.fromSeconds maxtime)
wrapper ()
handle TimeLimit.TimeOut =>
- (priority ("Search terminated, time limit (" ^
+ (Output.urgent_message ("Search terminated, time limit (" ^
string_of_int maxtime
^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.");
check_expect "unknown")
@@ -1273,7 +1273,7 @@
val t = th |> prop_of
in
if Logic.count_prems t = 0 then
- priority "No subgoal!"
+ Output.urgent_message "No subgoal!"
else
let
val assms = map term_of (Assumption.all_assms_of ctxt)
--- a/src/HOL/Tools/try.ML Tue Oct 26 11:20:14 2010 +0200
+++ b/src/HOL/Tools/try.ML Tue Oct 26 11:23:27 2010 +0200
@@ -96,7 +96,7 @@
Pretty.markup Markup.hilite
[Pretty.str message]])
else
- tap (fn _ => priority message)))
+ tap (fn _ => Output.urgent_message message)))
end
val invoke_try = fst oo do_try false
--- a/src/Pure/General/markup.ML Tue Oct 26 11:20:14 2010 +0200
+++ b/src/Pure/General/markup.ML Tue Oct 26 11:23:27 2010 +0200
@@ -120,11 +120,11 @@
val reportN: string val report: T
val no_reportN: string val no_report: T
val badN: string val bad: T
- val no_output: output * output
- val default_output: T -> output * output
- val add_mode: string -> (T -> output * output) -> unit
- val output: T -> output * output
- val enclose: T -> output -> output
+ val no_output: Output.output * Output.output
+ val default_output: T -> Output.output * Output.output
+ val add_mode: string -> (T -> Output.output * Output.output) -> unit
+ val output: T -> Output.output * Output.output
+ val enclose: T -> Output.output -> Output.output
val markup: T -> string -> string
end;
--- a/src/Pure/General/output.ML Tue Oct 26 11:20:14 2010 +0200
+++ b/src/Pure/General/output.ML Tue Oct 26 11:23:27 2010 +0200
@@ -6,9 +6,7 @@
signature BASIC_OUTPUT =
sig
- type output = string
val writeln: string -> unit
- val priority: string -> unit
val tracing: string -> unit
val warning: string -> unit
val legacy_feature: string -> unit
@@ -22,6 +20,7 @@
signature OUTPUT =
sig
include BASIC_OUTPUT
+ type output = string
val default_output: string -> output * int
val default_escape: output -> string
val add_mode: string -> (string -> output * int) -> (output -> string) -> unit
@@ -31,14 +30,18 @@
val raw_stdout: output -> unit
val raw_stderr: output -> unit
val raw_writeln: output -> unit
- val writeln_fn: (output -> unit) Unsynchronized.ref
- val priority_fn: (output -> unit) Unsynchronized.ref
- val tracing_fn: (output -> unit) Unsynchronized.ref
- val warning_fn: (output -> unit) Unsynchronized.ref
- val error_fn: (output -> unit) Unsynchronized.ref
- val prompt_fn: (output -> unit) Unsynchronized.ref
- val status_fn: (output -> unit) Unsynchronized.ref
- val report_fn: (output -> unit) Unsynchronized.ref
+ structure Private_Hooks:
+ sig
+ val writeln_fn: (output -> unit) Unsynchronized.ref
+ val urgent_message_fn: (output -> unit) Unsynchronized.ref
+ val tracing_fn: (output -> unit) Unsynchronized.ref
+ val warning_fn: (output -> unit) Unsynchronized.ref
+ val error_fn: (output -> unit) Unsynchronized.ref
+ val prompt_fn: (output -> unit) Unsynchronized.ref
+ val status_fn: (output -> unit) Unsynchronized.ref
+ val report_fn: (output -> unit) Unsynchronized.ref
+ end
+ val urgent_message: string -> unit
val error_msg: string -> unit
val prompt: string -> unit
val status: string -> unit
@@ -85,23 +88,26 @@
(* Isabelle output channels *)
-val writeln_fn = Unsynchronized.ref raw_writeln;
-val priority_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
-val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
-val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
-val error_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "*** ");
-val prompt_fn = Unsynchronized.ref raw_stdout;
-val status_fn = Unsynchronized.ref (fn _: string => ());
-val report_fn = Unsynchronized.ref (fn _: string => ());
+structure Private_Hooks =
+struct
+ val writeln_fn = Unsynchronized.ref raw_writeln;
+ val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
+ val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
+ val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
+ val error_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "*** ");
+ val prompt_fn = Unsynchronized.ref raw_stdout;
+ val status_fn = Unsynchronized.ref (fn _: string => ());
+ val report_fn = Unsynchronized.ref (fn _: string => ());
+end;
-fun writeln s = ! writeln_fn (output s);
-fun priority s = ! priority_fn (output s);
-fun tracing s = ! tracing_fn (output s);
-fun warning s = ! warning_fn (output s);
-fun error_msg s = ! error_fn (output s);
-fun prompt s = ! prompt_fn (output s);
-fun status s = ! status_fn (output s);
-fun report s = ! report_fn (output s);
+fun writeln s = ! Private_Hooks.writeln_fn (output s);
+fun urgent_message s = ! Private_Hooks.urgent_message_fn (output s);
+fun tracing s = ! Private_Hooks.tracing_fn (output s);
+fun warning s = ! Private_Hooks.warning_fn (output s);
+fun error_msg s = ! Private_Hooks.error_fn (output s);
+fun prompt s = ! Private_Hooks.prompt_fn (output s);
+fun status s = ! Private_Hooks.status_fn (output s);
+fun report s = ! Private_Hooks.report_fn (output s);
fun legacy_feature s = warning ("Legacy feature! " ^ s);
--- a/src/Pure/General/pretty.ML Tue Oct 26 11:20:14 2010 +0200
+++ b/src/Pure/General/pretty.ML Tue Oct 26 11:23:27 2010 +0200
@@ -21,8 +21,8 @@
signature PRETTY =
sig
- val default_indent: string -> int -> output
- val add_mode: string -> (string -> int -> output) -> unit
+ val default_indent: string -> int -> Output.output
+ val add_mode: string -> (string -> int -> Output.output) -> unit
type T
val str: string -> T
val brk: int -> T
@@ -55,7 +55,7 @@
val margin_default: int Unsynchronized.ref
val symbolicN: string
val output_buffer: int option -> T -> Buffer.T
- val output: int option -> T -> output
+ val output: int option -> T -> Output.output
val string_of_margin: int -> T -> string
val string_of: T -> string
val str_of: T -> string
@@ -103,9 +103,10 @@
(** printing items: compound phrases, strings, and breaks **)
abstype T =
- Block of (output * output) * T list * int * int | (*markup output, body, indentation, length*)
- String of output * int | (*text, length*)
- Break of bool * int (*mandatory flag, width if not taken*)
+ Block of (Output.output * Output.output) * T list * int * int
+ (*markup output, body, indentation, length*)
+ | String of Output.output * int (*text, length*)
+ | Break of bool * int (*mandatory flag, width if not taken*)
with
fun length (Block (_, _, _, len)) = len
--- a/src/Pure/General/symbol.ML Tue Oct 26 11:20:14 2010 +0200
+++ b/src/Pure/General/symbol.ML Tue Oct 26 11:23:27 2010 +0200
@@ -66,7 +66,7 @@
val bump_string: string -> string
val length: symbol list -> int
val xsymbolsN: string
- val output: string -> output * int
+ val output: string -> Output.output * int
end;
structure Symbol: SYMBOL =
--- a/src/Pure/General/xml.ML Tue Oct 26 11:20:14 2010 +0200
+++ b/src/Pure/General/xml.ML Tue Oct 26 11:23:27 2010 +0200
@@ -16,7 +16,7 @@
val header: string
val text: string -> string
val element: string -> attributes -> string list -> string
- val output_markup: Markup.T -> output * output
+ val output_markup: Markup.T -> Output.output * Output.output
val string_of: tree -> string
val output: tree -> TextIO.outstream -> unit
val parse_comments: string list -> unit * string list
--- a/src/Pure/Isar/proof.ML Tue Oct 26 11:20:14 2010 +0200
+++ b/src/Pure/Isar/proof.ML Tue Oct 26 11:23:27 2010 +0200
@@ -972,7 +972,7 @@
if ! testing then () else Proof_Display.print_results int ctxt res;
fun print_rule ctxt th =
if ! testing then rule := SOME th
- else if int then priority (Proof_Display.string_of_rule ctxt "Successful" th)
+ else if int then Output.urgent_message (Proof_Display.string_of_rule ctxt "Successful" th)
else ();
val test_proof =
try (local_skip_proof true)
--- a/src/Pure/Isar/toplevel.ML Tue Oct 26 11:20:14 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Tue Oct 26 11:23:27 2010 +0200
@@ -231,7 +231,8 @@
(((fn () => body () handle exn => if Exn.is_interrupt exn then () else reraise exn)
|> Runtime.debugging
|> Runtime.toplevel_error
- (fn exn => priority ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
+ (fn exn =>
+ Output.urgent_message ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
Simple_Thread.attributes interrupts);
--- a/src/Pure/Proof/extraction.ML Tue Oct 26 11:20:14 2010 +0200
+++ b/src/Pure/Proof/extraction.ML Tue Oct 26 11:23:27 2010 +0200
@@ -119,7 +119,7 @@
fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs));
fun corr_name s vs = extr_name s vs ^ "_correctness";
-fun msg d s = priority (Symbol.spaces d ^ s);
+fun msg d s = Output.urgent_message (Symbol.spaces d ^ s);
fun vars_of t = map Var (rev (Term.add_vars t []));
fun frees_of t = map Free (rev (Term.add_frees t []));
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Oct 26 11:20:14 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Oct 26 11:23:27 2010 +0200
@@ -74,14 +74,14 @@
| s => Output.raw_writeln (enclose bg en (prefix_lines prfx s)));
fun setup_messages () =
- (Output.writeln_fn := message "" "" "";
- Output.status_fn := (fn _ => ());
- Output.report_fn := (fn _ => ());
- Output.priority_fn := message (special "I") (special "J") "";
- Output.tracing_fn := message (special "I" ^ special "V") (special "J") "";
- Output.warning_fn := message (special "K") (special "L") "### ";
- Output.error_fn := message (special "M") (special "N") "*** ";
- Output.prompt_fn := (fn s => Output.raw_stdout (render s ^ special "S")));
+ (Output.Private_Hooks.writeln_fn := message "" "" "";
+ Output.Private_Hooks.status_fn := (fn _ => ());
+ Output.Private_Hooks.report_fn := (fn _ => ());
+ Output.Private_Hooks.urgent_message_fn := message (special "I") (special "J") "";
+ Output.Private_Hooks.tracing_fn := message (special "I" ^ special "V") (special "J") "";
+ Output.Private_Hooks.warning_fn := message (special "K") (special "L") "### ";
+ Output.Private_Hooks.error_fn := message (special "M") (special "N") "*** ";
+ Output.Private_Hooks.prompt_fn := (fn s => Output.raw_stdout (render s ^ special "S")));
fun panic s =
(message (special "M") (special "N") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1);
@@ -146,7 +146,7 @@
(* restart top-level loop (keeps most state information) *)
-val welcome = priority o Session.welcome;
+val welcome = Output.urgent_message o Session.welcome;
fun restart () =
(sync_thy_loader ();
@@ -227,7 +227,7 @@
Output.default_output Output.default_escape;
Markup.add_mode ProofGeneralPgip.proof_general_emacsN YXML.output_markup;
setup_messages ();
- ProofGeneralPgip.pgip_channel_emacs (! Output.priority_fn);
+ ProofGeneralPgip.pgip_channel_emacs (! Output.Private_Hooks.urgent_message_fn);
setup_thy_loader ();
setup_present_hook ();
initialized := true);
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Oct 26 11:20:14 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Oct 26 11:23:27 2010 +0200
@@ -160,13 +160,13 @@
add new lines explicitly in PGIP: they are left implicit. It means that PGIP messages
can't be written without newlines. *)
fun setup_messages () =
- (Output.writeln_fn := (fn s => normalmsg Message s);
- Output.status_fn := (fn _ => ());
- Output.report_fn := (fn _ => ());
- Output.priority_fn := (fn s => normalmsg Status s);
- Output.tracing_fn := (fn s => normalmsg Tracing s);
- Output.warning_fn := (fn s => errormsg Message Warning s);
- Output.error_fn := (fn s => errormsg Message Fatal s));
+ (Output.Private_Hooks.writeln_fn := (fn s => normalmsg Message s);
+ Output.Private_Hooks.status_fn := (fn _ => ());
+ Output.Private_Hooks.report_fn := (fn _ => ());
+ Output.Private_Hooks.urgent_message_fn := (fn s => normalmsg Status s);
+ Output.Private_Hooks.tracing_fn := (fn s => normalmsg Tracing s);
+ Output.Private_Hooks.warning_fn := (fn s => errormsg Message Warning s);
+ Output.Private_Hooks.error_fn := (fn s => errormsg Message Fatal s));
(* immediate messages *)
@@ -231,7 +231,7 @@
(* restart top-level loop (keeps most state information) *)
-val welcome = priority o Session.welcome;
+val welcome = Output.urgent_message o Session.welcome;
fun restart () =
(sync_thy_loader ();
@@ -807,14 +807,15 @@
PgipTypes.string_of_pgipurl url)
| NONE => (openfile_retract filepath;
changecwd_dir filedir;
- priority ("Working in file: " ^ PgipTypes.string_of_pgipurl url);
+ Output.urgent_message ("Working in file: " ^ PgipTypes.string_of_pgipurl url);
currently_open_file := SOME url)
end
fun closefile _ =
case !currently_open_file of
SOME f => (inform_file_processed f (Isar.state ());
- priority ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f);
+ Output.urgent_message
+ ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f);
currently_open_file := NONE)
| NONE => raise PGIP ("<closefile> when no file is open!")
@@ -835,7 +836,7 @@
fun abortfile _ =
case !currently_open_file of
SOME f => (isarcmd "init_toplevel";
- priority ("Aborted working in file: " ^
+ Output.urgent_message ("Aborted working in file: " ^
PgipTypes.string_of_pgipurl f);
currently_open_file := NONE)
| NONE => raise PGIP ("<abortfile> when no file is open!")
@@ -846,7 +847,7 @@
in
case !currently_open_file of
SOME f => raise PGIP ("<retractfile> when a file is open!")
- | NONE => (priority ("Retracting file: " ^ PgipTypes.string_of_pgipurl url);
+ | NONE => (Output.urgent_message ("Retracting file: " ^ PgipTypes.string_of_pgipurl url);
(* TODO: next should be in thy loader, here just for testing *)
let
val name = thy_name url
--- a/src/Pure/System/isabelle_process.ML Tue Oct 26 11:20:14 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML Tue Oct 26 11:23:27 2010 +0200
@@ -57,42 +57,33 @@
end;
-(* message markup *)
+(* message channels *)
local
-fun chunk s = string_of_int (size s) ^ "\n" ^ s;
+fun chunk s = [string_of_int (size s), "\n", s];
fun message _ _ _ "" = ()
- | message out_stream ch raw_props body =
+ | message mbox ch raw_props body =
let
val robust_props = map (pairself YXML.escape_controls) raw_props;
val header = YXML.string_of (XML.Elem ((ch, robust_props), []));
- in TextIO.output (out_stream, chunk header ^ chunk body) (*atomic output!*) end;
+ in Mailbox.send mbox (chunk header @ chunk body) end;
-in
-
-fun standard_message out_stream with_serial ch body =
- message out_stream ch
+fun standard_message mbox with_serial ch body =
+ message mbox ch
((if with_serial then cons (Markup.serialN, serial_string ()) else I)
(Position.properties_of (Position.thread_data ()))) body;
-fun init_message out_stream =
- message out_stream "A" [] (Session.welcome ());
-
-end;
-
-
-(* channels *)
-
-local
-
-fun auto_flush stream =
+fun message_output mbox out_stream =
let
- val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream stream, IO.BLOCK_BUF);
- fun loop () =
- (OS.Process.sleep (Time.fromMilliseconds 20); try TextIO.flushOut stream; loop ());
- in loop end;
+ fun loop receive =
+ (case receive mbox of
+ SOME msg =>
+ (List.app (fn s => TextIO.output (out_stream, s)) msg;
+ loop (Mailbox.receive_timeout (Time.fromMilliseconds 20)))
+ | NONE => (try TextIO.flushOut out_stream; loop (SOME o Mailbox.receive)));
+ in fn () => loop (SOME o Mailbox.receive) end;
in
@@ -102,19 +93,22 @@
val in_stream = TextIO.openIn in_fifo;
val out_stream = TextIO.openOut out_fifo;
- val _ = Simple_Thread.fork false (auto_flush out_stream);
- val _ = Simple_Thread.fork false (auto_flush TextIO.stdOut);
- val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr);
+ val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
+ val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
+
+ val mbox = Mailbox.create () : string list Mailbox.T;
+ val _ = Simple_Thread.fork false (message_output mbox out_stream);
in
- Output.status_fn := standard_message out_stream false "B";
- Output.report_fn := standard_message out_stream false "C";
- Output.writeln_fn := standard_message out_stream true "D";
- Output.tracing_fn := standard_message out_stream true "E";
- Output.warning_fn := standard_message out_stream true "F";
- Output.error_fn := standard_message out_stream true "G";
- Output.priority_fn := ! Output.writeln_fn;
- Output.prompt_fn := ignore;
- (in_stream, out_stream)
+ Output.Private_Hooks.status_fn := standard_message mbox false "B";
+ Output.Private_Hooks.report_fn := standard_message mbox false "C";
+ Output.Private_Hooks.writeln_fn := standard_message mbox true "D";
+ Output.Private_Hooks.tracing_fn := standard_message mbox true "E";
+ Output.Private_Hooks.warning_fn := standard_message mbox true "F";
+ Output.Private_Hooks.error_fn := standard_message mbox true "G";
+ Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
+ Output.Private_Hooks.prompt_fn := ignore;
+ message mbox "A" [] (Session.welcome ());
+ in_stream
end;
end;
@@ -179,8 +173,7 @@
val _ = Unsynchronized.change print_mode
(fold (update op =) [isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
- val (in_stream, out_stream) = setup_channels in_fifo out_fifo;
- val _ = init_message out_stream;
+ val in_stream = setup_channels in_fifo out_fifo;
val _ = Keyword.status ();
val _ = Output.status (Markup.markup Markup.ready "process ready");
in loop in_stream end));
--- a/src/Pure/Thy/thy_info.ML Tue Oct 26 11:20:14 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML Tue Oct 26 11:23:27 2010 +0200
@@ -141,7 +141,7 @@
else
let
val succs = thy_graph Graph.all_succs [name];
- val _ = priority (loader_msg "removing" succs);
+ val _ = Output.urgent_message (loader_msg "removing" succs);
val _ = List.app (perform Remove) succs;
val _ = change_thys (Graph.del_nodes succs);
in () end);
@@ -222,7 +222,7 @@
fun load_thy initiators update_time (deps: deps) text name parent_thys =
let
val _ = kill_thy name;
- val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators);
+ val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
val {master = (thy_path, _), ...} = deps;
val dir = Path.dir thy_path;
@@ -337,7 +337,7 @@
in
NAMED_CRITICAL "Thy_Info" (fn () =>
(kill_thy name;
- priority ("Registering theory " ^ quote name);
+ Output.urgent_message ("Registering theory " ^ quote name);
map get_theory parents;
change_thys (new_entry name parents (SOME deps, SOME theory));
perform Update name))
--- a/src/Pure/Thy/thy_syntax.ML Tue Oct 26 11:20:14 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.ML Tue Oct 26 11:23:27 2010 +0200
@@ -10,7 +10,7 @@
(Token.T, (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, 'a)
Source.source) Source.source) Source.source) Source.source
val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
- val present_token: Token.T -> output
+ val present_token: Token.T -> Output.output
val report_token: Token.T -> unit
datatype span_kind = Command of string | Ignored | Malformed
type span
@@ -19,7 +19,7 @@
val span_range: span -> Position.range
val span_source: (Token.T, 'a) Source.source -> (span, (Token.T, 'a) Source.source) Source.source
val parse_spans: Scan.lexicon * Scan.lexicon -> Position.T -> string -> span list
- val present_span: span -> output
+ val present_span: span -> Output.output
val report_span: span -> unit
val atom_source: (span, 'a) Source.source ->
(span * span list * bool, (span, 'a) Source.source) Source.source
--- a/src/Tools/quickcheck.ML Tue Oct 26 11:20:14 2010 +0200
+++ b/src/Tools/quickcheck.ML Tue Oct 26 11:23:27 2010 +0200
@@ -188,8 +188,10 @@
case iterate (fn () => tester (k - 1)) i empty_report
of (NONE, report) => apsnd (cons report) (with_testers k testers)
| (SOME q, report) => (SOME q, [report]);
- fun with_size k reports = if k > size then (NONE, reports)
- else (if quiet then () else priority ("Test data size: " ^ string_of_int k);
+ fun with_size k reports =
+ if k > size then (NONE, reports)
+ else
+ (if quiet then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
let
val (result, new_report) = with_testers k testers
val reports = ((k, new_report) :: reports)
--- a/src/Tools/solve_direct.ML Tue Oct 26 11:20:14 2010 +0200
+++ b/src/Tools/solve_direct.ML Tue Oct 26 11:23:27 2010 +0200
@@ -84,7 +84,7 @@
Pretty.markup Markup.hilite (message results)])
else
tap (fn _ =>
- priority (Pretty.string_of (Pretty.chunks (message results))))))
+ Output.urgent_message (Pretty.string_of (Pretty.chunks (message results))))))
| _ => (false, state))
end;