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

[Gerwin.Klein at data61.csiro.au]

We probably still have a few occurrences of these, but no problem phasing them out.

Cheers,
Gerwin

On 09.11.2018, at 10:03, Peter Lammich <lammich at in.tum.de<mailto:lammich at in.tum.de>> 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

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


Peter


-------- Original Message --------
Subject: [isabelle-dev] Remaining uses of {* ... *} quotation?
From: Makarius
To: isabelle-dev
CC:


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).

In particular, what are the remaining uses of {* ... *}?

It should already be superseded by cartouches. There is also "isabelle
update_cartouches" to get rid of it (as well as `alt_string`).


The long-term trend is to converge to cartouches or double-quotes almost
everywhere. Cartouches are for nested languages, and double quotes for
string literals or names that are in conflict with other syntax.


Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-dev at in.tum.de<mailto:isabelle-dev at in.tum.de>
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-dev at in.tum.de<mailto:isabelle-dev at in.tum.de>
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20181108/7643098a/attachment-0002.html>