Re: [isabelle] Remaining reasons for Proof General



Hi,

Am Dienstag, den 12.11.2013, 18:12 +0100 schrieb Makarius:
> 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.

as a suggestion, would it be possible to decouple the question of
whether a theory appears in the Theories panel from the question of
whether a buffer exists for it?

In detail, given Theories A and B, where B imports A. If I import A.thy,
I will be asked if I want to load theory B as well. Obviously I press
Yes. Now B appears in the Theories panel, and will be processes as a
prerequisite for A, but the file B.thy will not be (visibly) opened.

If I now want to edit B.thy as well, I can either double-click on B in
the Theories panel, or File→Open it as usual. When I’m done with it, I
can even close it; it will stay in the Theories panel (as a dependency
of A).

This way, I have full control over what files I have open, and what I
can cycle with Ctrl-PgUp. In fact, I was expecting this behavior when I
first fired up jEdit. Possible, it could also speed up things, as no UI
elements would have be generated for the files that do not have buffers.

Greetings,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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