Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] [Isabelle2017-RC1] Removing shortcut is not pe...


view this post on Zulip Email Gateway (Aug 22 2022 at 16:00):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
As I have not been able to abide the "ENTER -> Newline with indentation of Isabelle keywords"
shortcut in jEdit, I have adopted the habit of visiting Utilities>Global Options>Shortcuts,
searching "indent", clicking on this command, and selecting "remove current".
The problem is that this selection does not persist across invocations, so I have to make
this change each time I start Isabelle/jEdit. This was true in Isabelle2016-1, and it again
appears to be true in Isabelle2017-RC1. Presumably these selections are supposed to be
persistent, and it would be nice if they were.

I am running Isabelle under Ubuntu 16.04 LTS.


Last updated: Apr 25 2024 at 20:15 UTC