# 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