[isabelle] String inner syntax

[Peter Lammich]

From the NEWS file (Isabelle2014)

* Inner syntax token language allows regular quoted strings "..."
(only makes sense in practice, if outer syntax is delimited
differently, e.g. via cartouches).


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?

--
  Peter

[Peter Lammich]

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?

--
  Peter

From the NEWS file (Isabelle2014)
* Inner syntax token language allows regular quoted strings "..."
(only makes sense in practice, if outer syntax is delimited
differently, e.g. via cartouches).
Unfortunately, this seems not to work in Isabelle2018, and I cannot
find a NEWS entry that this had been discontinued.
  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?
--
  Peter

[Makarius]

Post by Peter Lammich
  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?

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