Email Gateway (Aug 18 2022 at 12:21): Email Gateway (Aug 18 2022 at 12:21):From: Makarius <makarius@sketis.net>
Some Isabelle users have asked about redirecting the message channels to a
separate file, e.g. to prevent Proof General from choking on massive
amounts of trace output.
The hooks for these message functions are in src/Pure/General/output.ML,
e.g. Output.tracing_fn for tracing. In principle they can be changed
arbitrarily, although Proof General needs some for internal control
(notably the "error" and "priority" channels). Moreover, Proof General
output will always be decorated according to the active print mode -- one
would normally want to strip that for logging to a file.
So the most basic Output.tracing_fn setup for the "PGASCII" mode of Proof
General (the one that works with UTF-8, c.f. option -U) looks like this:
val strip_specials =
let
fun strip ("\^A" :: _ :: cs) = strip cs
| strip (c :: cs) = c :: strip cs
| strip [] = [];
in implode o strip o explode end;
fun redirect_tracing stream =
Output.tracing_fn := (fn s =>
(TextIO.output (stream, (strip_specials s));
TextIO.output (stream, "\n");
TextIO.flushOut stream));
The next generation of Isabelle interfaces will cope with huge amounts of
messages by default ...
Makarius
Last updated: Nov 21 2024 at 12:39 UTC