--- a/src/Doc/JEdit/JEdit.thy Thu Dec 17 13:51:37 2020 +0000
+++ b/src/Doc/JEdit/JEdit.thy Fri Dec 18 11:44:34 2020 +0100
@@ -1317,7 +1317,8 @@
within the visible text area. The keyboard modifier \<^verbatim>\<open>CS\<close> overrides this:
then all defining and referencing positions are shown. This modifier may be
configured via option @{system_option jedit_focus_modifier}; the default
- coincides with the modifier for the above keyboard actions.
+ coincides with the modifier for the above keyboard actions. The empty string
+ means to disable this additional visual feedback.
\<close>