clarified def vs. ref focus, e.g. for calculation vs. command refs;
authorwenzelm
Fri, 22 Jul 2016 19:04:30 +0200
changeset 63544 e0cd6469a6b8
parent 63543 e6e057c01401
child 63545 c2f69dac0353
clarified def vs. ref focus, e.g. for calculation vs. command refs;
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))
     }
   }