[isabelle] Isabelle2018-RC0: Confusing cursor behavior with control sequences in jEdit



Hi,

Given a term of the form:

val _ = \<^term>‹123›

which looks like

val _ = *term*‹123›

it is confusing to navigate through it via (e.g.) ctrl-left. For example if
the cursor is on 123, and I push ctrl-left until the cursor is at the
beginning of *term*, and then I press backspace, I would (given the
visuals) expect the space to vanish. Instead, *term* becomes \<term> (the ^
goes away). This is logical given that *term* is actually \<^term>, but
since it is not visually represented that way, I would expect ctrl-left to
jump before the \.

I don't know anything about jEdit interna, so perhaps this is very hard to
change. But if it can be changed, I think editing would be smoother if
*term* were interpreted as a single word for the purpose of ctrl-left,
ctrl-right.

Similar problems happen when highlighting *term* via a doubleclick.

Best wishes,
Dominique.



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