Email Gateway (Aug 22 2022 at 17:31): Email Gateway (Aug 22 2022 at 17:31):From: Dominique Unruh <unruh@ut.ee>
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.
Email Gateway (Aug 22 2022 at 17:42):From: Makarius <makarius@sketis.net>
The editing mode provides a proper noWordSep for characters that should
be treated like letters for certain word-oriented operations (including
doubleclick selection).
I have changed that for the next Isabelle2018 release candidate, see
https://isabelle.sketis.net/repos/isabelle-release/rev/2e31887d9664
That means \ < ^ > will be treated as word consituents. Consequently,
the following will be a single word:
\<^term>
\foobar
abc<xyz
abc^xyz
The latter two occur within the term language (or ML) as infixes, but
normally there is space around that.
Makarius
Email Gateway (Aug 22 2022 at 17:51):From: Makarius <makarius@sketis.net>
I have now published Isabelle2018-RC1 without looking at this again, but
I will do so before the final release.
Makarius
Last updated: Apr 25 2024 at 16:19 UTC