--- 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)