Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2018-RC2 request: jedit abbreviation f...

view this post on Zulip Email Gateway (Aug 22 2022 at 17:41):

From: Michal Wallace <michal.wallace@gmail.com>
Since "--" is no longer accepted as a comment syntax, it would be nice if
that
input mapped to a built-in jEdit shortcut for the new syntax (maybe
offering a
menu with the code comment symbol as well... Otherwise, how does one type
it?)

view this post on Zulip Email Gateway (Aug 22 2022 at 17:41):

From: Makarius <makarius@sketis.net>
I usually complete on \co (comment) or \ca (cancel).

Makarius

Last updated: Apr 17 2024 at 20:15 UTC