Email Gateway (Aug 22 2022 at 18:46): Email Gateway (Aug 22 2022 at 18:46):From: Peter Lammich <lammich@in.tum.de>
From the NEWS file (Isabelle2014)
Unfortunately, this seems not to work in Isabelle2018, and I cannot
find a NEWS entry that this had been discontinued.
e.g. in Isabelle 2018:
term ‹''a''›
*** OK
term ‹"a"›
*** Inner syntax error⌂
Failed to parse term
Do I misunderstand this news entry? Or has this feature (silently)
disappeared again?
Email Gateway (Aug 22 2022 at 18:46):From: Peter Lammich <lammich@in.tum.de>
Update:
I just realized that the actual translation of string literals is, of
course, HOL-specific.
The "..." syntax for string literals is actually hidden in
HOL/ex/Cartouche_Examples.thy.
Should we include this to HOL/Main by default? Or make this easy to
activate, e.g., by importing some theory HOL-Library.String_Quotes?
Or have I, again, missed something and it is already there?
Email Gateway (Aug 22 2022 at 18:46):From: Makarius <makarius@sketis.net>
The inner token language is there, but not used/usable in regular
Isabelle/HOL applications. It requires a general move away from "..." as
delimiter from outer vs. inner syntax, always using cartouches here.
Not much has happened in recent years with such pending reforms:
presently I am trying to get rid of obsolete {* ... *} syntax -- I am
surprised how many users still have that in new theories.
Makarius
Last updated: Apr 20 2024 at 01:05 UTC