| 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) =>