src/Pure/PIDE/markup.scala

   val PATH = "path"
   val Path = new Markup_String(PATH, NAME)
 
   val URL = "url"
   val Url = new Markup_String(URL, NAME)
+
+  val DOC = "doc"
+  val Doc = new Markup_String(DOC, NAME)
 
 
   /* pretty printing */
 
   val Block = new Markup_Int("block", "indent")