[isabelle-dev] Remaining uses of Proof General?

[Andreas Lochbihler]

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