On 02/05/14 16:16, Makarius wrote:
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.
I have used such templating mechanism with Eclipse and finally disabled them, because they
caused me more work than what they saved. I usually prefer to enter both delimiters
separately and to just see the matching parenthesis highlighted.
The reason is that I often add the delimiters only later. For example, when I write a
single-identifier term, I use
text {* @{term my_constant} *}
and some time later, I figure out that I have to add something, e.g., a type constraint.
Hence, I produce the following sequence of edits (the # denotes the position of the cursor)
text {* @{term #my_constant} *}
text {* @{term "#my_constant} *}
text {* @{term "my_constant#} *}
text {* @{term "my_constant :: my_type#} *}
text {* @{term "my_constant :: my_type"#} *}
With the template mechanisms that I have seen so far, I get the following
sequence:
text {* @{term #my_constant} *}
text {* @{term "#"my_constant} *}
text {* @{term "#my_constant} *}
text {* @{term "my_constant#} *}
text {* @{term "my_constant :: my_type#} *}
text {* @{term "my_constant :: my_type"#"} *}
text {* @{term "my_constant :: my_type"#} *}
Andreas
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
