NEWS
changeset 14816 b77cebcd7e6e
parent 14795 b702848de41f
child 14854 61bdf2ae4dc5
     1.1 --- a/NEWS	Sat May 29 14:54:10 2004 +0200
     1.2 +++ b/NEWS	Sat May 29 14:54:58 2004 +0200
     1.3 @@ -24,24 +24,34 @@
     1.4    show_structs controls printing of implicit structures.  Typical
     1.5    applications of these concepts involve record types and locales.
     1.6  
     1.7 -* Pure: syntax of terms, types etc. includes (*(*nested*) comments*).
     1.8 -
     1.9 -* Pure: 'advanced' translation functions (parse_translation etc.) may
    1.10 -  depend on the signature of the theory context being presently used
    1.11 -  for parsing/printing, see also isar-ref manual.
    1.12 -
    1.13 -* Pure: tuned internal renaming of symbolic identifiers -- attach
    1.14 -  primes instead of base 26 numbers.
    1.15 -
    1.16  * Pure: clear separation of logical types and nonterminals, where the
    1.17    latter may only occur in 'syntax' specifications or type
    1.18    abbreviations.  Before that distinction was only partially
    1.19    implemented via type class "logic" vs. "{}".  Potential
    1.20    INCOMPATIBILITY in rare cases of improper use of 'types'/'consts'
    1.21    instead of 'nonterminals'/'syntax'.  Some very exotic syntax
    1.22 -  specifications requiring additional non-logical non-syntactic types
    1.23 -  (apart from 'prop' vs. 'logic') may need to be reformulated with
    1.24 -  duplicated 'consts'/'syntax' declarations (e.g. see Cube/Base.thy).
    1.25 +  specifications may require further adaption (e.g. Cube/Base.thy).
    1.26 +
    1.27 +* Pure/Syntax: inner syntax includes (*(*nested*) comments*).
    1.28 +
    1.29 +* Pure/Syntax: pretty pinter now supports unbreakable blocks,
    1.30 +  specified in mixfix annotations as "(00...)".
    1.31 +
    1.32 +* Pure/Syntax: 'advanced' translation functions (parse_translation
    1.33 +  etc.) may depend on the signature of the theory context being
    1.34 +  presently used for parsing/printing, see also isar-ref manual.
    1.35 +
    1.36 +* Pure: tuned internal renaming of symbolic identifiers -- attach
    1.37 +  primes instead of base 26 numbers.
    1.38 +
    1.39 +* ML: all output via channels of writeln/warning/error etc. is now
    1.40 +  passed through Output.output.  This gives interface builders a
    1.41 +  chance to adapt text encodings in arbitrary manners (say as XML
    1.42 +  entities); see the hook provided by Output.add_mode.  On the other
    1.43 +  hand, results of Pretty.string_of/str_of (including string_of_term,
    1.44 +  string_of_thm etc.) are still 'raw' (containing funny \<^raw...>
    1.45 +  symbols), which requires separate application of Output.output
    1.46 +  whenever strings are *not* passed on to writeln/warning/error etc.
    1.47  
    1.48  
    1.49  *** HOL ***