[isabelle-dev] Remaining uses of Proof General?

[Makarius]

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
     update state.

   * The Output / Detach button to produce an unchanging Info window on the
     spot.

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


 	Makarius