Email Gateway (Aug 18 2022 at 16:34): Email Gateway (Aug 18 2022 at 16:34):From: John Munroe <munddr@gmail.com>
Hi all,
I'm having some rather strange behaviour while using
Output.warning_fn. For example, if I have:
val trm = @{term "(P::bool)"};
val (Free(_,T)) = trm;
val typ_str = Syntax.string_of_typ @{context} T;
val inp = Output.output typ_str;
! Output.warning_fn inp;
I get a pretty "### bool" shown in the response. However, if I try:
val f = Unsynchronized.ref (Output.std_output o suffix "\n" o
prefix_lines "### ");
! f inp;
I get an YXML tree. How come ! Output.warning_fn inp and ! f inp
return different results?
Thanks for any help in advance.
John
Email Gateway (Aug 18 2022 at 16:36):From: Makarius <makarius@sketis.net>
These hooks for Isabelle output channels are definitely private aspects of
the system implementation and should never be touched in user space. To
emphasize this further, they are called something like
Output.Private_Hooks.warning_fn in the coming release, and will become
fully private at some later stage.
Moreover, having seen more discussion of accidental implementation details
in Christian Urban's cookbook, I have recently made some efforts to adapt
the pretty printing of formatted output to reflect the idea of an abstract
datatype of Isabelle messages, even if it is all just concrete strings for
historical reasons.
To cut a long story short: in user code the only thing that can be done
with formatted formal entities (Syntx.pretty_term etc.) is to paste them
together and pass them on to writeln etc. without guessing at further
implementation details.
Makarius
Last updated: Apr 26 2024 at 20:16 UTC