# HG changeset patch
# User wenzelm
# Date 1607882686 -3600
# Node ID 3c09adb4b04249336b061df07a1609eeefda45c9
# Parent  16fd39c9e31f4cdb82d810d77fa7f46fd777ed71
tuned signature;

diff -r 16fd39c9e31f -r 3c09adb4b042 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sun Dec 13 17:48:51 2020 +0100
+++ b/src/Pure/PIDE/markup.scala	Sun Dec 13 19:04:46 2020 +0100
@@ -104,11 +104,11 @@
   val BINDING = "binding"
   val ENTITY = "entity"
 
+  val Def = new Properties.Long("def")
+  val Ref = new Properties.Long("ref")
+
   object Entity
   {
-    val Def = new Properties.Long("def")
-    val Ref = new Properties.Long("ref")
-
     def unapply(markup: Markup): Option[(String, String)] =
       markup match {
         case Markup(ENTITY, props) =>
diff -r 16fd39c9e31f -r 3c09adb4b042 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Sun Dec 13 17:48:51 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala	Sun Dec 13 19:04:46 2020 +0100
@@ -447,8 +447,8 @@
                 Some((Nil, Some(Rendering.Color.intensify)))
               case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
                 props match {
-                  case Markup.Entity.Def(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity)))
-                  case Markup.Entity.Ref(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity)))
+                  case Markup.Def(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity)))
+                  case Markup.Ref(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity)))
                   case _ => None
                 }
               case (_, Text.Info(_, XML.Elem(Markup.Markdown_Bullet(depth), _))) =>
@@ -509,8 +509,8 @@
           {
             case (focus, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
               props match {
-                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 Markup.Def(i) if check(true, i) => Some(focus + i)
+                case Markup.Ref(i) if check(false, i) => Some(focus + i)
                 case _ => None
               }
             case _ => None
@@ -536,8 +536,8 @@
           {
             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 Markup.Def(i) if focus(i) => Some(true)
+                case Markup.Ref(i) if focus(i) => Some(true)
                 case _ => None
               }
           })
diff -r 16fd39c9e31f -r 3c09adb4b042 src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Sun Dec 13 17:48:51 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Sun Dec 13 19:04:46 2020 +0100
@@ -227,7 +227,7 @@
   def entity_ref(range: Text.Range, focus: Rendering.Focus): List[Text.Info[Color]] =
     snapshot.select(range, Rendering.entity_elements, _ =>
       {
-        case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Entity.Ref(i)), _))
+        case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Ref(i)), _))
         if focus(i) => Some(entity_ref_color)
         case _ => None
       })