merged
authorwenzelm
Wed, 16 Dec 2020 15:47:33 +0100
changeset 73174 12baa337aee2
parent 73164 590608c05386 (current diff)
parent 73173 fbc1d5ff3683 (diff)
child 73177 686c7ee213e9
child 73178 bc88423eb0ad
merged
--- a/NEWS	Wed Dec 16 13:39:49 2020 +0100
+++ b/NEWS	Wed Dec 16 15:47:33 2020 +0100
@@ -16,6 +16,14 @@
 
 *** Isabelle/jEdit Prover IDE ***
 
+* Action "isabelle.goto-entity" (shortcut CS+d) jumps to the definition
+of the formal entity at the caret position.
+
+* The visual feedback on caret entity focus is normally restricted to
+definitions within the visible text area. The keyboard modifier "CS"
+overrides this: then all defining and referencing positions are shown.
+See also option "jedit_focus_modifier".
+
 * Auto nitpick is enabled by default: it is now reasonably fast due to
 Kodkod invocation within Isabelle/Scala.
 
--- a/etc/options	Wed Dec 16 13:39:49 2020 +0100
+++ b/etc/options	Wed Dec 16 15:47:33 2020 +0100
@@ -159,7 +159,7 @@
 public option editor_load_delay : real = 0.5
   -- "delay for file load operations (new buffers etc.)"
 
-public option editor_input_delay : real = 0.3
+public option editor_input_delay : real = 0.2
   -- "delay for user input (text edits, cursor movement etc.)"
 
 public option editor_generated_input_delay : real = 1.0
--- a/src/Doc/JEdit/JEdit.thy	Wed Dec 16 13:39:49 2020 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Wed Dec 16 15:47:33 2020 +0100
@@ -1287,8 +1287,9 @@
   defining position with all its referencing positions. This correspondence is
   highlighted in the text according to the cursor position, see also
   \figref{fig:scope1}. Here the referencing positions are rendered with an
-  additional border, in reminiscence to a hyperlink: clicking there moves the
-  cursor to the original defining position.
+  additional border, in reminiscence to a hyperlink. A mouse click with \<^verbatim>\<open>C\<close>
+  modifier, or the action @{action_def "isabelle.goto-entity"} (shortcut
+  \<^verbatim>\<open>CS+d\<close>) jumps to the original defining position.
 
   \begin{figure}[!htb]
   \begin{center}
@@ -1300,8 +1301,9 @@
 
   The action @{action_def "isabelle.select-entity"} (shortcut \<^verbatim>\<open>CS+ENTER\<close>)
   supports semantic selection of all occurrences of the formal entity at the
-  caret position. This facilitates systematic renaming, using regular jEdit
-  editing of a multi-selection, see also \figref{fig:scope2}.
+  caret position, with a defining position in the current editor buffer. This
+  facilitates systematic renaming, using regular jEdit editing of a
+  multi-selection, see also \figref{fig:scope2}.
 
   \begin{figure}[!htb]
   \begin{center}
@@ -1310,6 +1312,12 @@
   \caption{The result of semantic selection and systematic renaming}
   \label{fig:scope2}
   \end{figure}
+
+  By default, the visual feedback on scopes is restricted to definitions
+  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.
 \<close>
 
 
--- a/src/Pure/PIDE/markup.scala	Wed Dec 16 13:39:49 2020 +0100
+++ b/src/Pure/PIDE/markup.scala	Wed Dec 16 15:47:33 2020 +0100
@@ -119,7 +119,7 @@
       def unapply(markup: Markup): Option[Long] =
         if (markup.name == ENTITY) Markup.Ref.unapply(markup.properties) else None
     }
-    object Id
+    object Occ
     {
       def unapply(markup: Markup): Option[Long] =
         Def.unapply(markup) orElse Ref.unapply(markup)
--- a/src/Pure/PIDE/rendering.scala	Wed Dec 16 13:39:49 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala	Wed Dec 16 15:47:33 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])
@@ -439,14 +446,14 @@
           range, (List(Markup.Empty), None), elements,
           command_states =>
             {
-              case (((markups, color), Text.Info(_, XML.Elem(markup, _))))
+              case ((markups, color), Text.Info(_, XML.Elem(markup, _)))
               if markups.nonEmpty && Document_Status.Command_Status.proper_elements(markup.name) =>
                 Some((markup :: markups, color))
               case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
                 Some((Nil, Some(Rendering.Color.bad)))
               case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
                 Some((Nil, Some(Rendering.Color.intensify)))
-              case (_, Text.Info(_, XML.Elem(Markup.Entity.Id(i), _))) if focus(i) =>
+              case (_, Text.Info(_, XML.Elem(Markup.Entity.Occ(i), _))) if focus(i) =>
                 Some((Nil, Some(Rendering.Color.entity)))
               case (_, Text.Info(_, XML.Elem(Markup.Markdown_Bullet(depth), _))) =>
                 val color =
@@ -472,7 +479,7 @@
                 else None
             })
       color <-
-        (result match {
+        result match {
           case (markups, opt_color) if markups.nonEmpty =>
             val status = Document_Status.Command_Status.make(markups.iterator)
             if (status.is_unprocessed) Some(Rendering.Color.unprocessed1)
@@ -480,7 +487,7 @@
             else if (status.is_canceled) Some(Rendering.Color.canceled)
             else opt_color
           case (_, opt_color) => opt_color
-        })
+        }
     } yield Text.Info(r, color)
   }
 
@@ -504,33 +511,38 @@
           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_defs = caret_focus(caret_range, visible_range)
-    if (focus_defs.defined) {
-      snapshot.cumulate[Boolean](visible_range, false, Rendering.entity_elements, _ =>
+    val focus = caret_focus(caret_range, defs_range)
+    if (focus.defined) {
+      snapshot.cumulate[Boolean](defs_range, false, Rendering.entity_elements, _ =>
         {
-          case (_, Text.Info(_, XML.Elem(Markup.Entity.Id(i), _)))
-          if focus_defs(i) => Some(true)
+          case (_, Text.Info(_, XML.Elem(Markup.Entity.Occ(i), _))) if focus(i) => Some(true)
           case _ => None
         }).flatMap(info => if (info.info) Some(info.range) else None)
     }
--- a/src/Tools/jEdit/etc/options	Wed Dec 16 13:39:49 2020 +0100
+++ b/src/Tools/jEdit/etc/options	Wed Dec 16 15:47:33 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/actions.xml	Wed Dec 16 13:39:49 2020 +0100
+++ b/src/Tools/jEdit/src/actions.xml	Wed Dec 16 15:47:33 2020 +0100
@@ -67,6 +67,11 @@
 	    isabelle.jedit.Isabelle.newline(textArea);
 	  </CODE>
 	</ACTION>
+	<ACTION NAME="isabelle.goto-entity">
+	  <CODE>
+	    isabelle.jedit.Isabelle.goto_entity(view);
+	  </CODE>
+	</ACTION>
 	<ACTION NAME="isabelle.select-entity">
 	  <CODE>
 	    isabelle.jedit.Isabelle.select_entity(textArea);
--- a/src/Tools/jEdit/src/isabelle.scala	Wed Dec 16 13:39:49 2020 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Wed Dec 16 15:47:33 2020 +0100
@@ -352,7 +352,18 @@
   }
 
 
-  /* selection */
+  /* formal entities */
+
+  def goto_entity(view: View)
+  {
+    val text_area = view.getTextArea
+    for {
+      doc_view <- Document_View.get(text_area)
+      rendering = doc_view.get_rendering()
+      caret_range = JEdit_Lib.caret_range(text_area)
+      link <- rendering.hyperlink_entity(caret_range)
+    } link.info.follow(view)
+  }
 
   def select_entity(text_area: JEditTextArea)
   {
--- a/src/Tools/jEdit/src/jEdit.props	Wed Dec 16 13:39:49 2020 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Wed Dec 16 15:47:33 2020 +0100
@@ -225,6 +225,8 @@
 isabelle.exclude-word.label=Exclude word
 isabelle.first-error.label=Go to first error
 isabelle.first-error.shortcut=CS+a
+isabelle.goto-entity.label=Go to definition of formal entity at caret
+isabelle.goto-entity.shortcut=CS+d
 isabelle.include-word-permanently.label=Include word permanently
 isabelle.include-word.label=Include word
 isabelle.increase-font-size.label=Increase font size
--- a/src/Tools/jEdit/src/jedit_lib.scala	Wed Dec 16 13:39:49 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Wed Dec 16 15:47:33 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/jedit_rendering.scala	Wed Dec 16 13:39:49 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Wed Dec 16 15:47:33 2020 +0100
@@ -285,6 +285,18 @@
         }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None }
   }
 
+  def hyperlink_entity(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
+  {
+    snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
+      range, Vector.empty, Rendering.entity_elements, _ =>
+        {
+          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
+            val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props)
+            opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
+          case _ => None
+        }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None }
+  }
+
 
   /* active elements */
 
--- a/src/Tools/jEdit/src/rich_text_area.scala	Wed Dec 16 13:39:49 2020 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Wed Dec 16 15:47:33 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)