# HG changeset patch
# User wenzelm
# Date 1236629534 -3600
# Node ID f3103bd2b167c5ea2ceca4f79ede69c0b4d68b9a
# Parent  c11a1e65a2ed9141a731fcf850a5b53a78b7725a
* More systematic treatment of long names, abstract name bindings, and name space operations.
* Simplified interface for defining document antiquotations via ThyOutput.antiquotation.

diff -r c11a1e65a2ed -r f3103bd2b167 NEWS
--- a/NEWS	Mon Mar 09 20:34:11 2009 +0100
+++ b/NEWS	Mon Mar 09 21:12:14 2009 +0100
@@ -75,18 +75,6 @@
 
     class foo = ...     instead of      class foo = type + ...
 
-* Type binding gradually replaces formerly used type bstring for names
-to be bound.  Name space interface for declarations has been simplified:
-
-  NameSpace.declare: NameSpace.naming
-    -> binding -> NameSpace.T -> string * NameSpace.T
-  NameSpace.bind: NameSpace.naming
-    -> binding * 'a -> 'a NameSpace.table -> string * 'a NameSpace.table
-         (*exception Symtab.DUP*)
-
-See further modules src/Pure/General/binding.ML and
-src/Pure/General/name_space.ML
-
 * Module moves in repository:
     src/Pure/Tools/value.ML ~> src/Tools/
     src/Pure/Tools/quickcheck.ML ~> src/Tools/
@@ -634,13 +622,22 @@
 for theorem dependency output of transactions resulting in a new
 theory state.
 
-* Name bindings in higher specification mechanisms (notably
-LocalTheory.define, LocalTheory.note, and derived packages) are now
-formalized as type Name.binding, replacing old bstring.
-INCOMPATIBILITY, need to wrap strings via Name.binding function, see
-also Name.name_of.  Packages should pass name bindings given by the
-user to underlying specification mechanisms; this enables precise
-tracking of source positions, for example.
+* More systematic treatment of long names, abstract name bindings, and
+name space operations.  Basic operations on qualified names have been
+move from structure NameSpace to Long_Name, e.g.  Long_Name.base_name,
+Long_Name.append.  Old type bstring has been mostly replaced by
+abstract type binding (see structure Binding), which supports precise
+qualification (by packages and local theory), and proper tracking of
+source positions.  INCOMPATIBILITY, need to wrap old bstring values
+into Binding.name, or better pass through abstract bindings
+everywhere.  See further src/Pure/General/long_name.ML,
+src/Pure/General/binding.ML and src/Pure/General/name_space.ML
+
+* Simplified interface for defining document antiquotations via
+ThyOutput.antiquotation, ThyOutput.output, and optionally
+ThyOutput.maybe_pretty_source.  INCOMPATIBILITY, need to simplify user
+antiquotations accordingly, see src/Pure/Thy/thy_output.ML for common
+examples.
 
 * Result facts (from PureThy.note_thms, ProofContext.note_thms,
 LocalTheory.note etc.) now refer to the *full* internal name, not the