src/Pure/PIDE/markup.scala
changeset 62986 9d2fae6b31cc
parent 62806 de9bf8171626
child 63337 ae9330fdbc16
     1.1 --- a/src/Pure/PIDE/markup.scala	Thu Apr 14 20:47:44 2016 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Thu Apr 14 22:55:53 2016 +0200
     1.3 @@ -86,11 +86,12 @@
     1.4  
     1.5    val BINDING = "binding"
     1.6    val ENTITY = "entity"
     1.7 -  val DEF = "def"
     1.8 -  val REF = "ref"
     1.9  
    1.10    object Entity
    1.11    {
    1.12 +    val Def = new Properties.Long("def")
    1.13 +    val Ref = new Properties.Long("ref")
    1.14 +
    1.15      def unapply(markup: Markup): Option[(String, String)] =
    1.16        markup match {
    1.17          case Markup(ENTITY, props) =>