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

The more such fine points become known, the better the chances that they can be sorted out eventually.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.