# HG changeset patch # User wenzelm # Date 1608130053 -3600 # Node ID 12baa337aee290cf28c547d62c3865d459f6d26d # Parent 590608c05386815e616296d8dfd60ac6b7cc3d02# Parent fbc1d5ff3683429bbe76899b8ef01a3227d29f2d merged diff -r 590608c05386 -r 12baa337aee2 NEWS --- 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. diff -r 590608c05386 -r 12baa337aee2 etc/options --- 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 diff -r 590608c05386 -r 12baa337aee2 src/Doc/JEdit/JEdit.thy --- 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>\C\ + modifier, or the action @{action_def "isabelle.goto-entity"} (shortcut + \<^verbatim>\CS+d\) jumps to the original defining position. \begin{figure}[!htb] \begin{center} @@ -1300,8 +1301,9 @@ The action @{action_def "isabelle.select-entity"} (shortcut \<^verbatim>\CS+ENTER\) 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>\CS\ 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. \ diff -r 590608c05386 -r 12baa337aee2 src/Pure/PIDE/markup.scala --- 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) diff -r 590608c05386 -r 12baa337aee2 src/Pure/PIDE/rendering.scala --- 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) } diff -r 590608c05386 -r 12baa337aee2 src/Tools/jEdit/etc/options --- 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)" diff -r 590608c05386 -r 12baa337aee2 src/Tools/jEdit/src/actions.xml --- 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); + + + isabelle.jedit.Isabelle.goto_entity(view); + + isabelle.jedit.Isabelle.select_entity(textArea); diff -r 590608c05386 -r 12baa337aee2 src/Tools/jEdit/src/isabelle.scala --- 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) { diff -r 590608c05386 -r 12baa337aee2 src/Tools/jEdit/src/jEdit.props --- 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 diff -r 590608c05386 -r 12baa337aee2 src/Tools/jEdit/src/jedit_lib.scala --- 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 + } } diff -r 590608c05386 -r 12baa337aee2 src/Tools/jEdit/src/jedit_rendering.scala --- 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 */ diff -r 590608c05386 -r 12baa337aee2 src/Tools/jEdit/src/rich_text_area.scala --- 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)