Re: [isabelle] Isabelle2014-RC0: keyboard focus during incremental search
On Mon, 7 Jul 2014, Andreas Lochbihler wrote:
Suppose that I use the incremental search bar to search for something in
the current buffer. For example, I'd like to jump to the first
"lift_definition" command in a theory. After typing lift_d, the view
already shows what I was looking for. Having read the information I was
interested in (without pressing any further keys), I then press some
other keys to navigate in the theory file (such as PgUp and PgDn). This
tricks me into thinking that the keyboard focus now is back in the main
text area. However, as soon as I press Key-Up, I end up scrolling
through the history of incremental search, which causes the text area to
jump around wildly. Can I somehow set that one I start scrolling with
keys, the focus is transferred back to the main text area?
jEdit has many tricks of keyboard focus change that I don't understand in
all details, but I have adapted to some of its aspects in Isabelle/jEdit
as of the Isabelle2014-RC0 snapshot.
For example, the main text area cursor is now always visible, but changes
color depending on focus: without focus it is rendered via
caret_invisible_color, which is a very pale and greyish version of the
original red. So when the cursor becomes pale in that sense, it means
special tricks apply: only those key events are passed to the text area
that are presently uninterpreted by the GUI component that does have the
focus. This can be the search bar, action bar, completion popup etc.
I did not know the search bar incident yet, and put it on my list of
things to keep in mind, whenever I revisit this very delicate topic of
focus and event propagation again.
Note that Isabelle2014-RC0 it is already a bit more smooth than in
Isabelle2013-2 concerning keyboard focus and event propagation. This was
the result of myself spending 3 days as actual user (for the AFP entry
Roy_Floyd_Warshall) and watching closely for snags, to iron them out
The more such fine points become known, the better the chances that they
can be sorted out eventually.
This archive was generated by a fusion of
Pipermail (Mailman edition) and