clarified caret focus modifier, depending on option "jedit_focus_modifier";

--- a/src/Pure/PIDE/rendering.scala	Mon Dec 14 16:51:12 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala	Mon Dec 14 22:01:54 2020 +0100
@@ -178,6 +178,13 @@
     val empty: Focus = apply(Set.empty)
     def make(args: List[Text.Info[Focus]]): Focus =
       (empty /: args)({ case (focus1, Text.Info(_, focus2)) => focus1 ++ focus2 })
+
+    val full: Focus =
+      new Focus(Set.empty)
+      {
+        override def apply(id: Long): Boolean = true
+        override def toString: String = "Focus.full"
+      }
   }
 
   sealed class Focus private[Rendering](protected val rep: Set[Long])
@@ -504,30 +511,36 @@
           case _ => None
         }))
 
-  def entity_focus(range: Text.Range, visible_defs: Rendering.Focus): Rendering.Focus =
+  def entity_focus(range: Text.Range, defs_focus: Rendering.Focus): Rendering.Focus =
     Rendering.Focus.make(
       snapshot.cumulate(range, Rendering.Focus.empty, Rendering.entity_elements, _ =>
         {
           case (focus, Text.Info(_, XML.Elem(Markup.Entity.Ref(i), _)))
-          if visible_defs(i) => Some(focus + i)
+          if defs_focus(i) => Some(focus + i)
           case _ => None
         }))
 
 
   /* caret focus */
 
-  def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Rendering.Focus =
+  def caret_focus(caret_range: Text.Range, defs_range: Text.Range): Rendering.Focus =
   {
     val focus = entity_focus_defs(caret_range)
     if (focus.defined) focus
-    else entity_focus(caret_range, entity_focus_defs(visible_range))
+    else if (defs_range == Text.Range.offside) Rendering.Focus.empty
+    else {
+      val defs_focus =
+        if (defs_range == Text.Range.full) Rendering.Focus.full
+        else entity_focus_defs(defs_range)
+      entity_focus(caret_range, defs_focus)
+    }
   }
 
-  def caret_focus_ranges(caret_range: Text.Range, visible_range: Text.Range): List[Text.Range] =
+  def caret_focus_ranges(caret_range: Text.Range, defs_range: Text.Range): List[Text.Range] =
   {
-    val focus = caret_focus(caret_range, visible_range)
+    val focus = caret_focus(caret_range, defs_range)
     if (focus.defined) {
-      snapshot.cumulate[Boolean](visible_range, false, Rendering.entity_elements, _ =>
+      snapshot.cumulate[Boolean](defs_range, false, Rendering.entity_elements, _ =>
         {
           case (_, Text.Info(_, XML.Elem(Markup.Entity.Id(i), _))) if focus(i) => Some(true)
           case _ => None

--- a/src/Tools/jEdit/etc/options	Mon Dec 14 16:51:12 2020 +0100
+++ b/src/Tools/jEdit/etc/options	Mon Dec 14 22:01:54 2020 +0100
@@ -39,6 +39,9 @@
 public option jedit_text_overview : bool = true
   -- "paint text overview column"
 
+public option jedit_focus_modifier : string = "CS"
+  -- "keyboard modifier to enable entity focus regardless of def visibility"
+
 public option isabelle_fonts_hinted : bool = true
   -- "use hinted Isabelle DejaVu fonts (change requires restart)"
 

--- a/src/Tools/jEdit/src/isabelle.scala	Mon Dec 14 16:51:12 2020 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Mon Dec 14 22:01:54 2020 +0100
@@ -359,8 +359,7 @@
     for (doc_view <- Document_View.get(text_area)) {
       val rendering = doc_view.get_rendering()
       val caret_range = JEdit_Lib.caret_range(text_area)
-      val buffer_range = JEdit_Lib.buffer_range(text_area.getBuffer)
-      val active_focus = rendering.caret_focus_ranges(caret_range, buffer_range)
+      val active_focus = rendering.caret_focus_ranges(caret_range, Text.Range.full)
       if (active_focus.nonEmpty) {
         text_area.selectNone()
         for (r <- active_focus)

--- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Dec 14 16:51:12 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Dec 14 22:01:54 2020 +0100
@@ -17,8 +17,8 @@
 import scala.util.parsing.input.CharSequenceReader
 
 import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug, EditPane}
-import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
-import org.gjt.sp.jedit.gui.KeyEventWorkaround
+import org.gjt.sp.jedit.io.{FileVFS, VFSManager}
+import org.gjt.sp.jedit.gui.{KeyEventWorkaround, KeyEventTranslator}
 import org.gjt.sp.jedit.buffer.{JEditBuffer, LineManager}
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter}
 
@@ -400,4 +400,10 @@
 
   def shift_modifier(evt: InputEvent): Boolean =
     (evt.getModifiersEx & InputEvent.SHIFT_DOWN_MASK) != 0
+
+  def modifier_string(evt: InputEvent): String =
+    KeyEventTranslator.getModifierString(evt) match {
+      case null => ""
+      case s => s
+    }
 }

--- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Dec 14 16:51:12 2020 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Dec 14 22:01:54 2020 +0100
@@ -10,9 +10,9 @@
 
 import isabelle._
 
-import java.awt.{Graphics2D, Shape, Color, Point, Toolkit, Cursor, MouseInfo}
+import java.awt.{Graphics2D, Shape, Color, Point, Cursor, MouseInfo}
 import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
-  FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
+  FocusAdapter, FocusEvent, WindowEvent, WindowAdapter, KeyEvent}
 import java.awt.font.TextAttribute
 import javax.swing.SwingUtilities
 import java.text.AttributedString
@@ -71,6 +71,32 @@
     pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText")
 
 
+  /* caret focus modifier */
+
+  @volatile private var caret_focus_modifier = false
+
+  def caret_focus_range: Text.Range =
+    if (caret_focus_modifier) Text.Range.full
+    else JEdit_Lib.visible_range(text_area) getOrElse Text.Range.offside
+
+  private val key_listener =
+    JEdit_Lib.key_listener(
+      key_pressed = (evt: KeyEvent) =>
+      {
+        val mod = PIDE.options.string("jedit_focus_modifier")
+        val old = caret_focus_modifier
+        caret_focus_modifier = (mod.nonEmpty && mod == JEdit_Lib.modifier_string(evt))
+        if (caret_focus_modifier != old) caret_update()
+      },
+      key_released = _ =>
+      {
+        if (caret_focus_modifier) {
+          caret_focus_modifier = false
+          caret_update()
+        }
+      })
+
+
   /* common painter state */
 
   @volatile private var painter_rendering: JEdit_Rendering = null
@@ -86,11 +112,10 @@
       painter_rendering = get_rendering()
       painter_clip = gfx.getClip
       caret_focus =
-        JEdit_Lib.visible_range(text_area) match {
-          case Some(visible_range) if caret_enabled && !painter_rendering.snapshot.is_outdated =>
-            painter_rendering.caret_focus(JEdit_Lib.caret_range(text_area), visible_range)
-          case _ => Rendering.Focus.empty
+        if (caret_enabled && !painter_rendering.snapshot.is_outdated) {
+          painter_rendering.caret_focus(JEdit_Lib.caret_range(text_area), caret_focus_range)
         }
+        else Rendering.Focus.empty
     }
   }
 
@@ -674,6 +699,7 @@
     painter.removeExtension(orig_text_painter)
     painter.addMouseListener(mouse_listener)
     painter.addMouseMotionListener(mouse_motion_listener)
+    text_area.addKeyListener(key_listener)
     text_area.addFocusListener(focus_listener)
     view.addWindowListener(window_listener)
   }
@@ -684,6 +710,7 @@
     val painter = text_area.getPainter
     view.removeWindowListener(window_listener)
     text_area.removeFocusListener(focus_listener)
+    text_area.removeKeyListener(key_listener)
     painter.removeMouseMotionListener(mouse_motion_listener)
     painter.removeMouseListener(mouse_listener)
     painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)