Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned signature;
authorwenzelm
Sun, 13 Dec 2020 19:04:46 +0100
changeset 72902 3c09adb4b042
parent 72901 16fd39c9e31f
child 72903 8f586c241071
tuned signature;
src/Pure/PIDE/markup.scala file | annotate | diff | comparison | revisions
src/Pure/PIDE/rendering.scala file | annotate | diff | comparison | revisions
src/Tools/jEdit/src/jedit_rendering.scala file | annotate | diff | comparison | revisions 
--- 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) =>
--- 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
               }
           })
--- 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
       })
isabelle