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

[Makarius]

On 08/11/2018 21:32, Makarius wrote:
> Over the decades we have accumulated funny quotation forms in Isabelle
> syntax that are often hard to explain to new users (also to old users).

I don't have a full overview of all the fine points yet, but the general
idea is like this:

  * cartouches are the main mechanism to embed/nest languages, e.g.
outer syntax -> document source -> inner syntax -> formal comment ->
antiquotation -> ...

  * retain " ... " as a way to quote names and other small bits of text;
its main use to embed inner syntax might eventually be superseded by
cartouches (which some users already do routinely)

  * keep the status-quo of (* ... *) as outer comments (source text that
is not part of the document)


The following can be probably phased out right now:

  * verbatim quotations {* ... *}

  * alt_string `...`

Both become cartouches; this is done by "isabelle update_cartouches"
already.


Rather soon there should be more advanced maintenance tools based on
semantic PIDE markup. E.g. it would allow to replace deeply nested
quotations reliably thanks to formal markup, say as a type/term within
ML. It would also allow to replace ":" by "\<in>" systematically, when
that is formal notation of the term language.


	Makarius