On Sun, 25 May 2014, Jasmin Christian Blanchette wrote:
In the course of a day, I typically find myself pulling from the
Isabelle repository several times. I am encouraged in this by my use of
Mercurial queues. So it's not untypical that my HOL image is slightly
out of date, usually in a harmless way. Sometimes I fire up Proof
General just because I know it will take the image as is instead of
forcing me to rebuild it (and waste 4 minutes of my time).
There is already "isabelle jedit -n" to bypass the automatic build. I
never use that myself, because I no longer do the bootstrap dependency
management in my head.
When I do have to step out of the self-build chain of the tool
infrastructure, e.g. when working on the sources of Isabelle/Pure or
Isabelle/jEdit sources, I use a separate jEdit editor process that is not
Isabelle/jEdit. Another option is to use the last official release of
Isabelle/jEdit to edit a few files elsewhere.
Sometimes I would just wish Isabelle/jEdit could allow me to do the
quick-and-dirty things the more primitive Proof General allowed -- a "I
know what I'm doing" flag so to speak.
I guess it is more "I knew how it used to be done in the old times with
Proof General end Emacs". Isabelle/jEdit does allow much more things than
was possible before, it only needs to be discovered.
Sometimes my impression is that it would be better to discard Proof
General on the spot, so that people have free mental energies to work in a
more productive way with slightly more up-to-date tools.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
