clarified signature: more explicit types;

--- a/src/Pure/PIDE/rendering.scala	Sun Dec 13 16:00:52 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala	Sun Dec 13 16:35:37 2020 +0100
@@ -170,6 +170,27 @@
       Markup.TVAR -> "schematic type variable")
 
 
+  /* entity focus */
+
+  object Focus
+  {
+    def apply(ids: Set[Long]): Focus = new Focus(ids)
+    val empty: Focus = apply(Set.empty)
+  }
+
+  sealed class Focus private[Rendering](protected val rep: Set[Long])
+  {
+    def defined: Boolean = rep.nonEmpty
+    def apply(id: Long): Boolean = rep.contains(id)
+    def + (id: Long): Focus = if (rep.contains(id)) this else new Focus(rep + id)
+    def ++ (other: Focus): Focus =
+      if (this eq other) this
+      else if (rep.isEmpty) other
+      else (this /: other.rep.iterator)(_ + _)
+    override def toString: String = rep.mkString("Focus(", ",", ")")
+  }
+
+
   /* markup elements */
 
   val position_elements =
@@ -218,7 +239,7 @@
   val warning_elements = Markup.Elements(Markup.WARNING, Markup.LEGACY)
   val error_elements = Markup.Elements(Markup.ERROR)
 
-  val caret_focus_elements = Markup.Elements(Markup.ENTITY)
+  val entity_focus_elements = Markup.Elements(Markup.ENTITY)
 
   val antiquoted_elements = Markup.Elements(Markup.ANTIQUOTED)
 
@@ -407,7 +428,7 @@
 
   /* text background */
 
-  def background(elements: Markup.Elements, range: Text.Range, focus: Set[Long])
+  def background(elements: Markup.Elements, range: Text.Range, focus: Rendering.Focus)
     : List[Text.Info[Rendering.Color.Value]] =
   {
     for {
@@ -478,38 +499,41 @@
   /* caret focus */
 
   private def entity_focus(range: Text.Range,
-    check: (Boolean, Long) => Boolean = (is_def: Boolean, i: Long) => is_def): Set[Long] =
+      check: (Boolean, Long) => Boolean = (is_def: Boolean, i: Long) => is_def)
+    : Rendering.Focus =
   {
     val results =
-      snapshot.cumulate[Set[Long]](range, Set.empty, Rendering.caret_focus_elements, _ =>
+      snapshot.cumulate[Rendering.Focus](range, Rendering.Focus.empty,
+        Rendering.entity_focus_elements, _ =>
           {
-            case (serials, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
+            case (focus, 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 Markup.Entity.Def(i) if check(true, i) => Some(focus + i)
+                case Markup.Entity.Ref(i) if check(false, i) => Some(focus + i)
                 case _ => None
               }
             case _ => None
           })
-    (Set.empty[Long] /: results){ case (s1, Text.Info(_, s2)) => s1 ++ s2 }
+    (Rendering.Focus.empty /: results){
+      case (focus1, Text.Info(_, focus2)) => focus1 ++ focus2 }
   }
 
-  def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Set[Long] =
+  def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Rendering.Focus =
   {
     val focus_defs = entity_focus(caret_range)
-    if (focus_defs.nonEmpty) focus_defs
+    if (focus_defs.defined) focus_defs
     else {
       val visible_defs = entity_focus(visible_range)
-      entity_focus(caret_range, (is_def: Boolean, i: Long) => !is_def && visible_defs.contains(i))
+      entity_focus(caret_range, (is_def: Boolean, i: Long) => !is_def && visible_defs(i))
     }
   }
 
   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) {
+    if (focus.defined) {
       val results =
-        snapshot.cumulate[Boolean](visible_range, false, Rendering.caret_focus_elements, _ =>
+        snapshot.cumulate[Boolean](visible_range, false, Rendering.entity_focus_elements, _ =>
           {
             case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
               props match {

--- a/src/Tools/VSCode/src/vscode_rendering.scala	Sun Dec 13 16:00:52 2020 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Sun Dec 13 16:35:37 2020 +0100
@@ -218,7 +218,8 @@
       List(
         () =>
           VSCode_Rendering.color_decorations("background_", VSCode_Rendering.background_colors,
-            background(VSCode_Rendering.background_elements, model.content.text_range, Set.empty)),
+            background(VSCode_Rendering.background_elements, model.content.text_range,
+              Rendering.Focus.empty)),
         () =>
           VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground_colors,
             foreground(model.content.text_range)),

--- a/src/Tools/jEdit/src/jedit_rendering.scala	Sun Dec 13 16:00:52 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Sun Dec 13 16:35:37 2020 +0100
@@ -224,11 +224,11 @@
 
   /* caret focus */
 
-  def entity_ref(range: Text.Range, focus: Set[Long]): List[Text.Info[Color]] =
-    snapshot.select(range, Rendering.caret_focus_elements, _ =>
+  def entity_ref(range: Text.Range, focus: Rendering.Focus): List[Text.Info[Color]] =
+    snapshot.select(range, Rendering.entity_focus_elements, _ =>
       {
-        case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Entity.Ref(i)), _)) if focus(i) =>
-          Some(entity_ref_color)
+        case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Entity.Ref(i)), _))
+        if focus(i) => Some(entity_ref_color)
         case _ => None
       })
 

--- a/src/Tools/jEdit/src/rich_text_area.scala	Sun Dec 13 16:00:52 2020 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sun Dec 13 16:35:37 2020 +0100
@@ -75,7 +75,7 @@
 
   @volatile private var painter_rendering: JEdit_Rendering = null
   @volatile private var painter_clip: Shape = null
-  @volatile private var caret_focus: Set[Long] = Set.empty
+  @volatile private var caret_focus = Rendering.Focus.empty
 
   private val set_state = new TextAreaExtension
   {
@@ -89,7 +89,7 @@
         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 _ => Set.empty[Long]
+          case _ => Rendering.Focus.empty
         }
     }
   }
@@ -102,7 +102,7 @@
     {
       painter_rendering = null
       painter_clip = null
-      caret_focus = Set.empty
+      caret_focus = Rendering.Focus.empty
     }
   }