--- a/NEWS Mon Jun 06 15:52:25 2016 +0200
+++ b/NEWS Mon Jun 06 16:04:26 2016 +0200
@@ -59,6 +59,10 @@
* Highlighting of entity def/ref positions wrt. cursor.
+* Action "isabelle.select-entity" (shortcut CS+ENTER) selects all
+occurences of the formal entity at the caret position. This facilitates
+systematic renaming.
+
* Document markup works across multiple Isar commands, e.g. the results
established at the end of a proof are properly identified in the theorem
statement.
--- a/src/Tools/jEdit/src/actions.xml Mon Jun 06 15:52:25 2016 +0200
+++ b/src/Tools/jEdit/src/actions.xml Mon Jun 06 16:04:26 2016 +0200
@@ -62,6 +62,11 @@
isabelle.jedit.Isabelle.decrease_font_size();
</CODE>
</ACTION>
+ <ACTION NAME="isabelle.select-entity">
+ <CODE>
+ isabelle.jedit.Isabelle.select_entity(textArea);
+ </CODE>
+ </ACTION>
<ACTION NAME="isabelle.complete">
<CODE>
isabelle.jedit.Isabelle.complete(view, false);
--- a/src/Tools/jEdit/src/isabelle.scala Mon Jun 06 15:52:25 2016 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Mon Jun 06 16:04:26 2016 +0200
@@ -16,7 +16,7 @@
import org.gjt.sp.jedit.{jEdit, View, Buffer}
import org.gjt.sp.jedit.buffer.JEditBuffer
-import org.gjt.sp.jedit.textarea.{JEditTextArea, StructureMatcher}
+import org.gjt.sp.jedit.textarea.{JEditTextArea, StructureMatcher, Selection}
import org.gjt.sp.jedit.syntax.TokenMarker
import org.gjt.sp.jedit.gui.{DockableWindowManager, CompleteWord}
import org.jedit.options.CombinedOptions
@@ -292,6 +292,26 @@
}
+ /* selection */
+
+ def select_entity(text_area: JEditTextArea)
+ {
+ for {
+ doc_view <- PIDE.document_view(text_area)
+ 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)
+ if (active_focus.nonEmpty) {
+ text_area.selectNone()
+ for (r <- active_focus)
+ text_area.addToSelection(new Selection.Range(r.start, r.stop))
+ }
+ }
+ }
+
+
/* completion */
def complete(view: View, word_only: Boolean)
--- a/src/Tools/jEdit/src/jEdit.props Mon Jun 06 15:52:25 2016 +0200
+++ b/src/Tools/jEdit/src/jEdit.props Mon Jun 06 16:04:26 2016 +0200
@@ -227,6 +227,8 @@
isabelle.reset-font-size.label=Reset font size
isabelle.reset-node-required.label=Reset node required
isabelle.reset-words.label=Reset non-permanent words
+isabelle.select-entity.label=Select all occurences of formal entity at caret
+isabelle.select-entity.shortcut=CS+ENTER
isabelle.set-continuous-checking.label=Set continuous checking
isabelle.set-node-required.label=Set node required
isabelle.toggle-breakpoint.label=Toggle Breakpoint
--- a/src/Tools/jEdit/src/rendering.scala Mon Jun 06 15:52:25 2016 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Mon Jun 06 16:04:26 2016 +0200
@@ -436,6 +436,25 @@
}
}
+ def caret_focus_ranges(caret_range: Text.Range, visible_range: Text.Range): List[Text.Range] =
+ {
+ val focus = caret_focus(caret_range, visible_range)
+ if (focus.nonEmpty) {
+ val results =
+ snapshot.cumulate[Boolean](visible_range, false, Rendering.caret_focus_elements, _ =>
+ {
+ case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
+ props match {
+ case Markup.Entity.Def(i) if focus(i) => Some(true)
+ case Markup.Entity.Ref(i) if focus(i) => Some(true)
+ case _ => None
+ }
+ })
+ for (info <- results if info.info) yield info.range
+ }
+ else Nil
+ }
+
def entity_ref(range: Text.Range, focus: Set[Long]): List[Text.Info[Color]] =
snapshot.select(range, Rendering.caret_focus_elements, _ =>
{