NEWS
changeset 14917 b54b11ebe220
parent 14897 577f95db94e4
child 14919 0f5fde03e2b5
     1.1 --- a/NEWS	Thu Jun 10 18:46:35 2004 +0200
     1.2 +++ b/NEWS	Thu Jun 10 20:11:51 2004 +0200
     1.3 @@ -55,14 +55,20 @@
     1.4    fold_commute}, for example.  Note that a proof context is escaped to
     1.5    the enclosing theory context first.
     1.6  
     1.7 -* ML: all output via channels of writeln/warning/error etc. is now
     1.8 -  passed through Output.output.  This gives interface builders a
     1.9 -  chance to adapt text encodings in arbitrary manners (say as XML
    1.10 -  entities); see the hook provided by Output.add_mode.  On the other
    1.11 -  hand, results of Pretty.string_of/str_of (including string_of_term,
    1.12 -  string_of_thm etc.) are still 'raw' (containing funny \<^raw...>
    1.13 -  symbols), which requires separate application of Output.output
    1.14 -  whenever strings are *not* passed on to writeln/warning/error etc.
    1.15 +* ML: output via the Isabelle channels of writeln/warning/error
    1.16 +  etc. is now passed through Output.output, with a hook for arbitrary
    1.17 +  transformations depending on the print_mode (cf. Output.add_mode --
    1.18 +  the first active mode that provides a output function wins).
    1.19 +  Already formatted output may be embedded into further text via
    1.20 +  Output.raw; the result of Pretty.string_of/str_of and derived
    1.21 +  functions (string_of_term/cterm/thm etc.) is already marked raw to
    1.22 +  accommodate easy composition of diagnostic messages etc.
    1.23 +  Programmers rarely need to care about Output.output or Output.raw at
    1.24 +  all, with some notable exceptions: Output.output is required when
    1.25 +  bypassing the standard channels (writeln etc.), or in token
    1.26 +  translations to produce properly formatted results; Output.raw is
    1.27 +  required when capturing already output material that will eventually
    1.28 +  be presented to the user a second time.
    1.29  
    1.30  
    1.31  *** HOL ***