I am new to Isabelle/jEdit. I am accustomed to Emacs, so I'd like to set the shortcuts in Emacs style. It went well in most cases, but the command Emacs Set Mark does not work. When I invoke the command, the message "Input/output complete" appears in the minibuffer, and nothing happens in the text area.
Does anyone have an idea to fix it? I tried the various shortcut keys but all fail. I use macOS Big Sur (version 11.5.2), Isabelle2021. (The keyboard is Japanese style.)
Both jEdit and the jEdit Isabelle plugin have a bunch of defaults which conflict with Emacs-style keys, so you have to make sure to unbind any existing keybindings that conflict with the ones you want to add and make sure they are removed from both primary and secondary. You have to do this by hand starting with the standard keybindings, because the Emacs keybinding set provided with jEdit sucks--and even worse, none of the default Isabelle keybindings are in it. Next time you start jEdit, it will open a dialog saying that there are keybinding conflicts, and you'll have to confirm the ones you just added.
Since this is kind of 面倒くさい both to explain and to do yourself, and there's not an easy way to show what I've changed vs. the defaults, here's my jEdit properties and Emacs-like keymap file. To use them:
Quit jEdit.
Copy the keymap file to $JEDIT_SETTINGS/keymaps/ (run isabelle getenv JEDIT_SETTINGS from your shell).
If you want to just use all my settings, copy the properties file to $JEDIT_SETTINGS/ (why wouldn't you, I have great taste :) ). Otherwise, grep -E '(^keymap\.current|\.shortcut2?\.ignore)=' properties and add the lines to $JEDIT_SETTINGS/properties yourself.
Start jEdit and resolve any keybinding conflicts it complains about.
My settings are Emacs-like with as many of the default Isabelle keys preserved, but Emacs stuff mostly takes priority: for example, Ctrl+b is backward-char instead of Isabelle completion, and Ctrl+e is move-end-of-line instead of being stolen by jEdit for a bunch of its key sequences.
Ctrl+SPC should activate the mark, but note that the region will NOT be highlighted until you perform some other command--try Emacs kill ring save (bound to M+w; that will probably be Opt+w on your Mac keyboard).
I haven't ran macOS in ages--I currently use Isabelle/jEdit on Linux over remote X11 with the X server running on Windows--but it shouldn't be any different on macOS, even with the Japanese layout, unless some other program you have is eating keys before they get to jEdit. (I think Ctrl+SPC switches the IME/keyboard layout on macOS by default, right? You might want to change either the macOS setting or the set mark binding in jEdit.)
On Java SE 16 and 17, you will probably get an error from jEdit saying something like:
unknown error: Unable to make public java.lang.AbstractStringBuilder java.lang.AbstractStringBuilder.append(java.lang.String) accessible: module java.base does not "opens java.lang" to unnamed module
To fix this, add this to your $ISABELLE_HOME_USER/etc/settings:
JEDIT_JAVA_OPTIONS="$JEDIT_JAVA_OPTIONS --add-opens=java.base/java.lang=ALL-UNNAMED"
(The --add-opens stuff is related to this Java runtime change, though you don't need to care about any of this to use Isabelle.)