[isabelle-dev] Remaining uses of Proof General?

[Makarius]

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