Email Gateway (Aug 19 2022 at 15:13): Email Gateway (Aug 19 2022 at 15:13):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Makarius,
while playing with Isabelle2014-RC0, the following behaviour of Isabelle/jEdit regularly
disrupted my work flow. 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?
Best,
Andreas
PS: Thanks for all the effort to build PIDE. I haven't used ProofGeneral for a while now
and I don't miss it much.
Email Gateway (Aug 19 2022 at 15:16):From: Makarius <makarius@sketis.net>
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
Last updated: Nov 21 2024 at 12:39 UTC