[isabelle-dev] Remaining uses of Proof General?

[Jasmin Christian Blanchette]

> (For now the list of Remaining uses of Proof General / Emacs seems to be empty.  If there is anything remaining, this thread is still open to submissions.)

Let me make this list nonempty again.

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

This is not a big issue, and I presume that if Proof General stopped to exist, I would adapt my workflow accordingly -- e.g. by getting into the habit of rebuilding HOL after each pull. But the above observation is connected with Andrei's "corridor full of smart people". 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.

Jasmin