[isabelle-dev] NEWS: formal comments

[Makarius]

*** General ***

* Marginal comments need to be written exclusively in the new-style form
"― ‹text›", old ASCII variants like "-- {* ... *}" are no longer
supported. INCOMPATIBILITY, use the command-line tool "isabelle
update_comments" to update existing theory files.

* Old-style inner comments (* ... *) within the term language are legacy
and will be discontinued soon: use formal comments "― ‹...›" or "⌦‹...›"
instead.


*** Document preparation ***

* Formal comments work uniformly in outer syntax, inner syntax (term
language), Isabelle/ML and some other embedded languages of Isabelle.
See also "Document comments" in the isar-ref manual. The following forms
are supported:

  - marginal text comment: ― ‹…›
  - canceled source: ⌦‹…›
  - raw LaTeX: \<^latex>‹…›


*** System ***

* The command-line tool "isabelle update_comments" normalizes formal
comments in outer syntax as follows: ― ‹text› (whith a single space to
approximate the appearance in document output). This is more specific
than former "isabelle update_cartouches -c": the latter tool option has
been discontinued.



This refers to Isabelle/5db077cfe1b2: it is a summary of all
comment-related updates, simplifications, and clarifications of the past
few weeks.

I have already updated the visible Isabelle universe including AFP. When
old-style inner comments (* ... *) are finally discontinued, we can
reunify infix notation for (+) vs. (*) etc. without extra spaces.


	Makarius