[isabelle-dev] NEWS

[Makarius]

*** ML ***

* 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 targets), as well as 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.