# HG changeset patch
# User wenzelm
# Date 1465221866 -7200
# Node ID 48bc9045866e547236447530968ba3695a459d0a
# Parent  bf98cc9e6e0647ec4474ddfc91c4eef7bb23e88d
added action "isabelle.select-entity";

diff -r bf98cc9e6e06 -r 48bc9045866e NEWS
--- 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.
diff -r bf98cc9e6e06 -r 48bc9045866e src/Tools/jEdit/src/actions.xml
--- 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);
diff -r bf98cc9e6e06 -r 48bc9045866e src/Tools/jEdit/src/isabelle.scala
--- 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)
diff -r bf98cc9e6e06 -r 48bc9045866e src/Tools/jEdit/src/jEdit.props
--- 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
diff -r bf98cc9e6e06 -r 48bc9045866e src/Tools/jEdit/src/rendering.scala
--- 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, _ =>
       {