[isabelle-dev] Preferences on Mac OS X

[Jasmin Christian Blanchette]

Am 24.09.2013 um 23:43 schrieb Makarius <makarius at sketis.net>:

> This is a question to hard-core users of Mac OS X.
> 
> How important is the canonical key sequence "COMMAND comma" as defined by Apple?

It's probably important, but I don't use it (for lack of having memorized it).

> Alternatively, I am open to suggestions for a replacement key for the default keymap, one that works on English, German, French keyboards, or lets say 2 out of these 3.

Cmd comma currently pops up an inline search. To me something like Alt Cmd F or Shift Cmd F would make sense, since it can be seen as a variation of Cmd F.

Jasmin