Re: [isabelle] Output.warning_fn and pretty printing



On Mon, 6 Dec 2010, John Munroe wrote:

I'm having some rather strange behaviour while using Output.warning_fn.

val trm = @{term "(P::bool)"};

I get an YXML tree. How come ! Output.warning_fn inp and ! f inp return different results?

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





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