[isabelle-dev] Remaining uses of Proof General?

[Makarius]

On Fri, 2 May 2014, 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.

See also:

changeset:   56842:b6e266574b26
user:        wenzelm
date:        Sat May 03 20:31:29 2014 +0200
files:       src/Tools/jEdit/etc/options 
src/Tools/jEdit/src/completion_popup.scala
description:
yet another completion option, to imitate old less ambitious behavior;


It allows to ignore the language context of the prover.

This is also an attempt to retain sanity, when masses of users complain 
about having to learn new things in the coming release.  Hopefully some 
will do some actual testing of this big space of features, and report 
problems before the release and not after it.


 	Makarius