1.1 --- a/NEWS	Mon Mar 09 20:34:11 2009 +0100
     1.2 +++ b/NEWS	Mon Mar 09 21:12:14 2009 +0100
     1.3 @@ -75,18 +75,6 @@
     1.4  
     1.5      class foo = ...     instead of      class foo = type + ...
     1.6  
     1.7 -* Type binding gradually replaces formerly used type bstring for names
     1.8 -to be bound.  Name space interface for declarations has been simplified:
     1.9 -
    1.10 -  NameSpace.declare: NameSpace.naming
    1.11 -    -> binding -> NameSpace.T -> string * NameSpace.T
    1.12 -  NameSpace.bind: NameSpace.naming
    1.13 -    -> binding * 'a -> 'a NameSpace.table -> string * 'a NameSpace.table
    1.14 -         (*exception Symtab.DUP*)
    1.15 -
    1.16 -See further modules src/Pure/General/binding.ML and
    1.17 -src/Pure/General/name_space.ML
    1.18 -
    1.19  * Module moves in repository:
    1.20      src/Pure/Tools/value.ML ~> src/Tools/
    1.21      src/Pure/Tools/quickcheck.ML ~> src/Tools/
    1.22 @@ -634,13 +622,22 @@
    1.23  for theorem dependency output of transactions resulting in a new
    1.24  theory state.
    1.25  
    1.26 -* Name bindings in higher specification mechanisms (notably
    1.27 -LocalTheory.define, LocalTheory.note, and derived packages) are now
    1.28 -formalized as type Name.binding, replacing old bstring.
    1.29 -INCOMPATIBILITY, need to wrap strings via Name.binding function, see
    1.30 -also Name.name_of.  Packages should pass name bindings given by the
    1.31 -user to underlying specification mechanisms; this enables precise
    1.32 -tracking of source positions, for example.
    1.33 +* More systematic treatment of long names, abstract name bindings, and
    1.34 +name space operations.  Basic operations on qualified names have been
    1.35 +move from structure NameSpace to Long_Name, e.g.  Long_Name.base_name,
    1.36 +Long_Name.append.  Old type bstring has been mostly replaced by
    1.37 +abstract type binding (see structure Binding), which supports precise
    1.38 +qualification (by packages and local theory), and proper tracking of
    1.39 +source positions.  INCOMPATIBILITY, need to wrap old bstring values
    1.40 +into Binding.name, or better pass through abstract bindings
    1.41 +everywhere.  See further src/Pure/General/long_name.ML,
    1.42 +src/Pure/General/binding.ML and src/Pure/General/name_space.ML
    1.43 +
    1.44 +* Simplified interface for defining document antiquotations via
    1.45 +ThyOutput.antiquotation, ThyOutput.output, and optionally
    1.46 +ThyOutput.maybe_pretty_source.  INCOMPATIBILITY, need to simplify user
    1.47 +antiquotations accordingly, see src/Pure/Thy/thy_output.ML for common
    1.48 +examples.
    1.49  
    1.50  * Result facts (from PureThy.note_thms, ProofContext.note_thms,
    1.51  LocalTheory.note etc.) now refer to the *full* internal name, not the