[isabelle] Redirecting message channels



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.