[isabelle-dev] NEWS: Isabelle/ML "build" combinators

[Makarius]

*** ML ***

* The "build" combinators of various data structures help to build
content from bottom-up, by applying an "add" function the "empty" value.
For example:

  - type 'a Symtab.table etc.: build
  - type 'a Names.table etc.: build
  - type 'a list: build and build_rev
  - type Buffer.T: build and build_content

For example, see src/Pure/PIDE/xml.ML:

  val content_of = Buffer.build_content o fold add_content;


This refers to Isabelle/4974c3697fee.

It may be seen as the final capstone for our approach to "canonical argument
order": it has turned out very beneficial to Isabelle/ML readability and
conciseness since 2005 (especially in contrast to the monadic bloat seen in
Haskell libraries).

We did not have "build" combinators in the past, because most applications
were for plain lists where "empty" is just []. For other data structures, it
does help to make the point more clear.


	Makarius