* Lexical syntax (inner and outer) supports text cartouches with
arbitrary nesting, and without escapes of quotes etc.
This refers to Isabelle/3eb7bcca5b90.
LCF-style provers had funny quotes, backquotes, antiquotes etc. from early
on, and there were occasional attempts to get rid of them. Just dropping
quotes and pretending that there is just one big syntax ends up in a
melange that is hard to define, and sub-languages tend to fight over
different kinds of keywords versus identifiers etc. (Even some Coq
experts now regret that they had gone that way many years ago.)
Postmodern Isabelle/Isar has accumulated various alternative quotation
forms with slightly different rules for nesting and escapes:
{* ... *}
" ... "
` ... `
'' ... ''
Together with antiquotations this quickly runs into limitations of
syntactic expression, of what is conceptually no problem: the arbitrary
nesting of "domain-specific formal languages".
Examples:
lemma "A ⟶ A" by (tactic {* rtac @{thm impI} 1 *})
ML {* @{lemma "A ⟶ A" by (tactic "rtac @{thm impI} 1")} *}
text {* @{ML "@{lemma \"A ⟶ A\" by (tactic \"rtac @{thm impI} 1\")}"} *}
-- "!?!?!?"
Gladly the ancient Egyptians had a different way to "quote" the royal name
of the Pharao: http://en.wikipedia.org/wiki/Cartouches
An alternative explanation for the name for this syntactic device is
http://en.wikipedia.org/wiki/Cartouche_%28design%29
In Isabelle it looks like this: symbols \<open> ... \<close> define the
boundary of a text range, with arbitrary nesting and no escapes nor
special rules for the body. The unicode rendering uses the rarely used
codepoints ‹ ... › to make this look nice and non-intrusive. Both the
Isabelle symbols and unicode glyphs are sufficiently exotic to stay
outside of usual application languages.
A playground with an exploration of possibilities is in
$ISABELLE_HOME/src/HOL/ex/Cartouche_Examples.thy e.g. see the "Uniform
nesting of sub-languages" example:
text_cartouche
‹
@{ML_cartouche
‹
(
@{term_cartouche ‹STR ""›};
@{term_cartouche ‹STR "abc"›};
@{term_cartouche ‹STR "abc" @ STR "xyz"›};
@{term_cartouche ‹STR "⏎"›};
@{term_cartouche ‹STR "\001\010\100"›}
)
›
}
›
Here the inner quotes are Isabelle/HOL string literals!
Isabelle/jEdit already knows about these special parantheses, so the
ragular jEdit operations to work with "code blocks" can be used, e.g. to
select or navigate through the nested structure.
For the moment this is just some fresh air to get new ideas. I don't
propose any bigger reforms just now.
The only concrete change that is already active is a slightly simplified
syntax for the @{rail} antiquotation, which avoids escapes of backslashes
and quotes in the body. (See examples in $ISABELLE_HOME/src/Doc/IsarRef
and elsewhere.)
Makarius_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
