tuned;
authorwenzelm
Thu May 09 15:56:14 2019 +0200 (6 months ago)
changeset 7025662a6c1257c05
parent 70255 81c6a9a9a791
child 70257 6778fdbd6c5d
tuned;
src/Doc/JEdit/JEdit.thy
     1.1 --- a/src/Doc/JEdit/JEdit.thy	Thu May 09 15:47:27 2019 +0200
     1.2 +++ b/src/Doc/JEdit/JEdit.thy	Thu May 09 15:56:14 2019 +0200
     1.3 @@ -305,7 +305,7 @@
     1.4    Connect to already running Isabelle/jEdit instance and open FILES\<close>}
     1.5  
     1.6    The \<^verbatim>\<open>-c\<close> option merely checks the presence of the server, producing a
     1.7 -  process return code accordingly.
     1.8 +  process return-code.
     1.9  
    1.10    The \<^verbatim>\<open>-n\<close> option reports the server name, and the \<^verbatim>\<open>-s\<close> option provides a
    1.11    different server name. The default server name is the official distribution
    1.12 @@ -2168,8 +2168,8 @@
    1.13    \<^emph>\<open>Preferences\<close> is in conflict with the jEdit default keyboard shortcut for
    1.14    \<^emph>\<open>Incremental Search Bar\<close> (action @{action_ref "quick-search"}).
    1.15  
    1.16 -  \<^bold>\<open>Workaround:\<close> Rebind key via \<^emph>\<open>Global Options~/ Shortcuts\<close> according to
    1.17 -  national keyboard, e.g.\ \<^verbatim>\<open>COMMAND+SLASH\<close> on English ones.
    1.18 +  \<^bold>\<open>Workaround:\<close> Rebind key via \<^emph>\<open>Global Options~/ Shortcuts\<close> according to the
    1.19 +  national keyboard layout, e.g.\ \<^verbatim>\<open>COMMAND+SLASH\<close> on English ones.
    1.20  
    1.21    \<^item> \<^bold>\<open>Problem:\<close> On Mac OS X with native Apple look-and-feel, some exotic
    1.22    national keyboards may cause a conflict of menu accelerator keys with