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