[isabelle-dev] Remaining uses of {* ... *} quotation?

[Makarius]

On 09/11/2018 00:03, Peter Lammich wrote:
> I sometimes see {* *} in old theory files, and find it funny to be
> reminded that this was standard only 5 years ago ... from my side there
> are no uses of this quotation remaining that I'd know of

Indeed. Do you want to apply "isabelle update_cartouches" yourself on
various AFP entries, e.g. the Automatic_Refinement stack?


> However, (* *) is still very important for informally andquickly
> commenting things out, also in inner syntax!

That is only a historic footnote. It was actually very confusing to have
the same notation (* ... *) in two different meanings:

  * outer syntax: material that is not part of the formal document, but
treated like white space; exception: slightly odd meta-comments (*<*)
... (*>*)

  * inner syntax: material that is not considered part of the term
language, but shown in the document source in the text style of the term
language

At some point there will more Prover IDE support to add/remove the
various formal comments (with control symbols and cartouches) that have
emerged recently. But the old inner syntax is not coming back.


	Makarius