Re: [isabelle] Remaining reasons for Proof General
On Tue, 12 Nov 2013, Peter Lammich wrote:
* In PG, I have some open buffers, these are the buffers that I'm
interested in. jEdit opens all dependent theories (approx 50 to 100 in
my typical use-case). So using cycle-buffer or similar functions makes
How can I efficiently switch between the theories that I'm currently
editing/interested in, without having to search them among dozens of
I've occasionally seen jEdit plugins to organize buffer groups or
"projects", but have not used any myself so far.
* I have no control when theories are processed. I loaded a theory, and
saw in the theory-panel all these purple bars slowly disappearing, until
no purple was left. Also for the theory that was currently displayed in
the main window. However, the theory in the main window was NOT
completely processed. When moving down the cursor, the purple bar
You can give some declarative hints in the "Theories" panel, namely for
global "Continuous checking" and individual "Mark as required for
continuous checking". There are also actions and keyboard shortcuts for
To get a general overview of specific actions and shortcuts of
Isabelle/jEdit, you can go to "Global Options / Shortcuts / Edit
Shortcuts: Plugin: Isabelle".
So how can I be sure that my theories are all correct?
By making a batch build in the old-fashioned manner.
An approximation in Isabelle/jEdit is to look closely at the Theories
panel overview, but with hundreds of theories it might be a bit difficult.
What is missing here is a general "wrapup" of the editor session similar
to the batch build session. This non-uniformity is one of these spots
where Proof General legacy support is in the way.
You have already noticed a subtle breakdown in this department in one of
the release candidates. Doing things once right is better than doing it
3-4 times slightly differently (Isabelle/jEdit, isabelle build, Proof
This archive was generated by a fusion of
Pipermail (Mailman edition) and