src/Pure/PIDE/markup.scala
changeset 61660 78b371644654
parent 61598 ed4dad8823a4
child 61862 e2a9e46ac0fb
     1.1 --- a/src/Pure/PIDE/markup.scala	Fri Nov 13 17:48:33 2015 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Fri Nov 13 19:59:28 2015 +0100
     1.3 @@ -174,6 +174,9 @@
     1.4    val URL = "url"
     1.5    val Url = new Markup_String(URL, NAME)
     1.6  
     1.7 +  val DOC = "doc"
     1.8 +  val Doc = new Markup_String(DOC, NAME)
     1.9 +
    1.10  
    1.11    /* pretty printing */
    1.12