[isabelle-dev] Remaining uses of Proof General?

[Andreas Lochbihler]

Hi Makarius,

Over the past weeks, I've been using Isabelle/jEdit about half of my Isabelle time (and 
ProofGeneral 3.7.1.1 with XEmacs the other half). Isabelle/jEdit is great when it comes to 
working on small projects or refactoring existing sources. I really like the negative line 
spacing setting and completion of fact names! Thanks!

My main usage of PG is when I want to construct a complicated proof method call like

(fastforce intro: ... dest: ... elim: ... simp add: ... cong: ... del: ... simp del: ...)+

that collapses an apply script of a hundred lines. I haven't yet found a convenient way to 
write the apply script in Isabelle/jEdit, because of reactivity issues (see item 2 below) 
and the continuous updates of the output window (when I scroll to some other part of the 
apply script using the cursor keys). Are there key bindings for scrolling that do not move 
the cursor?


Here are some things that could be improved in Isabelle/jEdit (I am currently on 
Isabelle/4e2a0d4e7a82):

1. Symbol completion in PG was absolutely deterministic. The immediate symbol completion 
in jEdit works great, too, I merely had to learn new sequences of key strokes. Symbol 
completion of non-unique results is not satisfactory.

a) Given some text like

definition foo where "foo = ..."

when I add an attribute like [simp]: after the where, I get a symbol completion popup to 
replace the : with the element sign. Usually, my next thing is to move the cursor with the 
cursor keys. But the popup gobbles all the key strokes until I explicitly close it with 
ESC. As colons are used everywhere in Isabelle's outer syntax, it would really be great if 
the popup only appears when I am in inner syntax.

b) Sometimes, when I write a HOL term, I used to not get the completion popup when I enter 
something like \un if there were sufficiently many parse errors in that partial term. Even 
Ctrl-b did not help. However, I cannot reproduce it in a small example at the moment.


2. Reactivity when processing large files

With PG, I knew how to control the Isabelle prover. When I edit a large file in a larger 
project like JinjaThreads, every now and then, Isabelle changes the background colour from 
red to gray and then, apparently nothing happens for minutes before Isabelle turns it red 
again and starts reprocessing. Is there some way to explicitly tell Isabelle that it 
should now start to check again. Toggling "continuous checking" does not help. Sometimes, 
I even have to close the theory file and reopen it again.


3. Navigation between theories files

In PG, I usually have only a small subset of the loaded theories and ML files open as 
buffers, and I conveniently switch between them with Ctrl-x b. In jEdit, I use Ctrl-` to 
go to the previous file, but going to a different one is a pain, because I have to search 
it in the complete list of open files.

It would be great if there was a list of just those files that I had on my screen 
previously, not all loaded files.

Moreover, when I close a file and then press Ctrl-` in the file that shows up, I do not 
get to the file I have visited before the two, but to some arbitrary other. Can jEdit 
remember the order in which files have been visited? XEmacs at least does this.


Maybe there are already solutions to the above annoyances, I just don't know them. There's 
another thing I would like to see in jEdit: The window layout has three columns (one dock 
on the left and one on the right) and the middle column (with the editor area) can be 
divided in three rows (dock - text - dock). Is there some way that I can split the right 
column into two rows to show two information areas at the same time (e.g. Output at the 
top and Find below)?


Andreas


On 27/04/14 20:14, Makarius wrote:
> Are there any remaining uses of Proof General, e.g. in the situation of current
> Isabelle/5b6f4655e2f2 ?
>
> This is neither a joke nor a running gag -- I just can't think of anything myself after
> the introduction of the spell checker.
>
>
>      Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev