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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
