[isabelle-dev] NEWS: Improved management of dockable windows

Makarius makarius at sketis.net
Wed May 21 21:34:31 CEST 2014


On Wed, 21 May 2014, Lars Noschinski wrote:

>  * Sometimes, I use a detached window to see the proof state at a
>    certain position in my theory, regardless on where my cursor is.
>    If I successfully changed (i.e. not in between) some lemmas before,
>    I want to see the updated proof state at the same position as before
>    (for example by clicking some "update" button).

You could try with a floating version of "Query / Proof Context / state" 
and then use the "Apply" button or its "ENTER" shortcut.  I've recently 
played with the focus a bit, so you can move the cursor in the inactive 
text area and press ENTER to update the output.  (E.g. in 362c8c64ec83.)

At the moment this is somewhat overlapping accidental functionality of 
Output vs. Info vs. Query.  Hopefully it will at some point become more 
clear what is really needed.  The "Preview" slot is still unused, and will 
remain so as a wildcard for some time.


 	Makarius




More information about the isabelle-dev mailing list