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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
