[isabelle] Isabelle2014-RC0: keyboard focus during incremental search



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.





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