On Fri, 2 May 2014, Andreas Lochbihler wrote:
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"#} *}
I think the second form is not proper templating yet, just an escape hatch
of the IDE to produce balanced quotes by default, since it is more often
correct that the other way round.
The Isabelle text cartouches are an attempt to get rid of unbalanced
quotes altogether, and reduce the problem to one of balanced parentheses.
My ` completion is already better than the above, because it allows to
select all 3 cases: balance template, left side, right side.
jEdit has already nice actions to select a "code block", depending on the
structure of parentheses. What is missing are ways to add or remove an
outermost pair of parentheses, which should not be too difficult to add.
Independently of code blocks, the Isabelle/jEdit actions to modify control
symbols already work with selections in a structured way. The completion
mechanism also knows a bit about the various forms of selection, and tries
to do something sensible with them.
The abobe example could be also handled by a double-click to select the
"word" of my_constant, and then perform a still hypothetical operation to
enclose it in quotes of some form.
Note that when I say "jEdit" it refers to the jEdit text editor, while the
Prover IDE is called Isabelle/jEdit. Getting the basic terminology right
helps to avoid confusion about what happens where, and who is ultimately
responsible for it.
We have an increasingly complex situation of many Isabelle sub-languages
and sub-systems, but being explicit about that is better than sweeping it
under the carpet. In contrast, the Coq guys have upheld the illusion of
one main language longer, and actually removed their quotes around the
term language long ago, and thus introduced many problems that persist
until today.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
