Re: [isabelle] Remaining reasons for Proof General

On Tue, 12 Nov 2013, Joachim Breitner wrote:

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?

That approach was basically at the very start of theory management some years ago, but it did not work out on the spot so I made the explicit flooding with jEdit buffers as intermediate solution. This worked better than anticipated, which explains why it is still there in its relatively crude way.

In the meantime isabelle build has become a formal part of Isabelle/Scala, and various jEdit "project" facilities have emerged. So it all needs to be all revisited to fit it nicely together, such that there is signicant conceptual progress as well.


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