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
no sense.

How can I efficiently switch between the theories that I'm currently
editing/interested in, without having to search them among dozens of
uninteresting theories?

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 appeared again.

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 that.

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 General, TTY).


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.