[isabelle-dev] Preferences on Mac OS X

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Tue Sep 24 23:58:15 CEST 2013

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.


More information about the isabelle-dev mailing list