src/Pure/General/markup.scala
changeset 34046 8e743ca417b9
parent 33985 1d33e85a3fa9
child 34119 ae92efb48784
equal deleted inserted replaced
34045:bc71778a327d 34046:8e743ca417b9
   183 
   183 
   184 
   184 
   185   /* content */
   185   /* content */
   186 
   186 
   187   val ROOT = "root"
   187   val ROOT = "root"
   188   val RAW = "raw"
       
   189   val BAD = "bad"
   188   val BAD = "bad"
       
   189   val DATA = "data"
   190 }
   190 }