can we use cartouches instead of quotation marks to delineate inner syntax in jEdit Isabelle/HOL sessions

Question

In typing statements of a proof into an Isabelle (2020) theory file, e.g.,

from ?prime p ? have p: "1 < p "

the jEdit interface application pops up a tooltip offering to insert an open cartouche command <open> when I type a quotation mark. As you can see in the line above, I have been allowing this and it seems to be permitted. The Isabelle documentation seems to view inner syntax as category embedded, which seems to permit delineation with quotation marks or with the cartouche enclosure <open ... <close>.

Is there a down side to doing this? The imports statement requires quoting a reference to a theory file "HOL-Computational_Algebra.Primes" with module.theory format and will not accept cartouche there, but in theory statements it certainly appears to be equivalent.

question from:https://stackoverflow.com/questions/65830578/can-we-use-cartouches-instead-of-quotation-marks-to-delineate-inner-syntax-in-je

Answer 1

Cartouches vs quotes is currently a matter of style, except for imports, syntax definitions, and for some command arguments (like nitpick[eval=".."]).

Remark that some keyboard layouts make it possible to type them directly (e.g., mac US international).

I believe that Makarius would like to deprecate the quotes eventually. This would allow users to write "a" instead of ''a'' for strings). But don't expect that to happen anytime soon.

So: Write what you like most!