[isabelle] Output.warning_fn and pretty printing



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





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