[isabelle-dev] Remaining uses of Proof General?
makarius at sketis.net
Fri May 2 16:27:54 CEST 2014
On Tue, 29 Apr 2014, Andreas Lochbihler wrote:
> There are hardly any performance problems in terms of computing power,
> possibly except for Isabelle processing a slow call to auto over and
> over again. The efficiency problem is the interaction with the IDE. I
> use the Find panel a lot, but then my output panel is not visible at the
> same time (that's why I would like to split the right dock in two). And
> when I scroll upwards to find a snippet of tactic script that I want to
> copy, the output updates and my current goal state is gone.
The mechanics of the Output panel are a bit old-fashioned, still assuming
a "single-focus" proof script model. At some point I would like to see a
proper "Preview" of a certain part of proof document, with state output
just in the right spots (zero or more depending on proof structure).
Until then there are various approximations:
* Multiple floating instances of Output, with different Update / Auto
* The Output / Detach button to produce an unchanging Info window on the
* The more flexible docking framework provided by the MyDoggy plugin,
although it is unclear if that is more than a nice experiment by one
of the old-time jEdit developers.
More information about the isabelle-dev