On Tue, 29 Apr 2014, Andreas Lochbihler wrote:
text ‹
@{term ‹A \un B›}
›
Here the \un works as expected -- the cartouche remains intact
independently of its
content, as long as the funny parentheses are nested properly.
But this correct nesting is exactly the problem. When I type \un while
writing the above, the closing parenthesis are not there yet. The prover sees
something like
text {* @{term "A \un
lemma foo: "..." by ...
But why? In the ancient times, input was always sequential, as depth-first
traversal of the intended tree structure. In less ancient times, some
people proposed rigid structural editors to make it impossible to escape
from nested boxes (still seen today in TeXmacs), although that is a bit
awkward. In the past 10 years or so, the standard IDE approach has
arrived somewhere in the middle: the user is free to type intermediate
non-sense, but the editor makes it easy to get it right by default.
Isabelle/jEdit still lacks serious templating, but there are beginnings of
it in the completion mechanism. The outer quotations and antiquotations
have specific support already: a single keystroke ` offers a template for
a well-formed cartouche, and the @{ prefix completes to a well-formed @{}
with the cursor in the middle. Even Proof General had C-c C-a C-a for
isar-antiquote already.
Makarius_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
