src/Pure/PIDE/markup.scala
changeset 62986 9d2fae6b31cc
parent 62806 de9bf8171626
child 63337 ae9330fdbc16
--- a/src/Pure/PIDE/markup.scala	Thu Apr 14 20:47:44 2016 +0200
+++ b/src/Pure/PIDE/markup.scala	Thu Apr 14 22:55:53 2016 +0200
@@ -86,11 +86,12 @@
 
   val BINDING = "binding"
   val ENTITY = "entity"
-  val DEF = "def"
-  val REF = "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) =>