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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
