[isabelle-dev] Remaining uses of Proof General?

[Makarius]

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