src/Pure/PIDE/markup.scala
changeset 51570 3633828d80fc
parent 50975 73ec6ad6700e
child 51574 2b58d7b139d6
     1.1 --- a/src/Pure/PIDE/markup.scala	Thu Mar 28 15:00:27 2013 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Thu Mar 28 15:36:45 2013 +0100
     1.3 @@ -82,9 +82,12 @@
     1.4  
     1.5    val Indent = new Properties.Int("indent")
     1.6    val BLOCK = "block"
     1.7 +
     1.8    val Width = new Properties.Int("width")
     1.9    val BREAK = "break"
    1.10  
    1.11 +  val ITEM = "item"
    1.12 +
    1.13    val SEPARATOR = "separator"
    1.14  
    1.15