# HG changeset patch
# User wenzelm
# Date 1086891111 -7200
# Node ID b54b11ebe22022ab28085b71e438ed03d22b167e
# Parent  ae1daa6016381564feacf11a4465bb831898dc9c
tuned;

diff -r ae1daa601638 -r b54b11ebe220 NEWS
--- a/NEWS	Thu Jun 10 18:46:35 2004 +0200
+++ b/NEWS	Thu Jun 10 20:11:51 2004 +0200
@@ -55,14 +55,20 @@
   fold_commute}, for example.  Note that a proof context is escaped to
   the enclosing theory context first.
 
-* ML: all output via channels of writeln/warning/error etc. is now
-  passed through Output.output.  This gives interface builders a
-  chance to adapt text encodings in arbitrary manners (say as XML
-  entities); see the hook provided by Output.add_mode.  On the other
-  hand, results of Pretty.string_of/str_of (including string_of_term,
-  string_of_thm etc.) are still 'raw' (containing funny \<^raw...>
-  symbols), which requires separate application of Output.output
-  whenever strings are *not* passed on to writeln/warning/error etc.
+* ML: output via the Isabelle channels of writeln/warning/error
+  etc. is now passed through Output.output, with a hook for arbitrary
+  transformations depending on the print_mode (cf. Output.add_mode --
+  the first active mode that provides a output function wins).
+  Already formatted output may be embedded into further text via
+  Output.raw; the result of Pretty.string_of/str_of and derived
+  functions (string_of_term/cterm/thm etc.) is already marked raw to
+  accommodate easy composition of diagnostic messages etc.
+  Programmers rarely need to care about Output.output or Output.raw at
+  all, with some notable exceptions: Output.output is required when
+  bypassing the standard channels (writeln etc.), or in token
+  translations to produce properly formatted results; Output.raw is
+  required when capturing already output material that will eventually
+  be presented to the user a second time.
 
 
 *** HOL ***