# HG changeset patch
# User wenzelm
# Date 1469207070 -7200
# Node ID e0cd6469a6b84e744c52617c9a767404def4e968
# Parent  e6e057c0140122b230440091d12b9672dec40608
clarified def vs. ref focus, e.g. for calculation vs. command refs;

diff -r e6e057c01401 -r e0cd6469a6b8 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Fri Jul 22 14:45:32 2016 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Fri Jul 22 19:04:30 2016 +0200
@@ -413,40 +413,30 @@
 
   /* caret focus */
 
+  def entity_focus(range: Text.Range,
+    check: (Boolean, Long) => Boolean = (is_def: Boolean, i: Long) => is_def): Set[Long] =
+  {
+    val results =
+      snapshot.cumulate[Set[Long]](range, Set.empty, Rendering.caret_focus_elements, _ =>
+          {
+            case (serials, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
+              props match {
+                case Markup.Entity.Def(i) if check(true, i) => Some(serials + i)
+                case Markup.Entity.Ref(i) if check(false, i) => Some(serials + i)
+                case _ => None
+              }
+            case _ => None
+          })
+    (Set.empty[Long] /: results){ case (s1, Text.Info(_, s2)) => s1 ++ s2 }
+  }
+
   def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Set[Long] =
   {
-    def focus(is_def: Boolean): Set[Long] =
-    {
-      val results =
-        snapshot.cumulate[Set[Long]](caret_range, Set.empty, Rendering.caret_focus_elements, _ =>
-            {
-              case (serials, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
-                props match {
-                  case Markup.Entity.Def(i) if is_def => Some(serials + i)
-                  case Markup.Entity.Ref(i) if !is_def => Some(serials + i)
-                  case _ => None
-                }
-              case _ => None
-            })
-      (Set.empty[Long] /: results){ case (s1, Text.Info(_, s2)) => s1 ++ s2 }
-    }
-
-    val focus_defs = focus(true)
-
+    val focus_defs = entity_focus(caret_range)
     if (focus_defs.nonEmpty) focus_defs
     else {
-      val focus_refs = focus(false)
-      def visible_def: Boolean =
-        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_refs(i) => Some(true)
-                case _ => None
-              }
-          }).exists(info => info.info)
-      if (focus_refs.nonEmpty && visible_def) focus_refs
-      else Set.empty[Long]
+      val visible_defs = entity_focus(visible_range)
+      entity_focus(caret_range, (is_def: Boolean, i: Long) => !is_def && visible_defs.contains(i))
     }
   }