Re: [isabelle] where to post jedit 4.3.2 bugs/feature requests?



On Tue, 3 May 2011, Nils Jähnig wrote:

The continous checking that is always enabled is a corollary of the absence of session manament.  I hope to have that in better shape for the next Isabelle release -- it also affects the way traditional batch-processing works, so it all takes a bit longer than anticipated.

I'm not sure, if I got you right (maybe due to me writing "auto-trace"). my idea was to get back to the not-enabled checking, without any options. pressing three keys to activate the parsing is no big deal. on the other hand I don't see a big advantage in having all theories parsed without pressing a button (please correct me, if I'm wrong). how does the absence of session management intefere here?

In the old Proof General model, the user "schedules" everything by hand -- individual commands and theory buffers. This is convenient for experts who want to control every aspect of the system themselves, but it is also a bit inefficient. A modern operating system also does the scheduling for the user, not the user for the operating system.

Session management above means dependency management and scheduling of checking. For Isabelle/Scala/jEdit in Isabelle2011 I've successfully removed the old stuff (which was also a lot of work), but managed to implement only little of the new world order when the release deadline was approaching. This is why it is still a bit awkward to work with files in Isabelle/jEdit right now, but you can expect it to get better again next time.


	Makarius


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