diff -r 38466f4f3483 -r 6fb98a20c349 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Thu Jul 18 13:12:54 2013 +0200 +++ b/src/Pure/PIDE/markup.scala Thu Jul 18 20:53:22 2013 +0200 @@ -303,7 +303,8 @@ val SENDBACK = "sendback" val PADDING = "padding" - val PADDING_LINE = (PADDING, LINE) + val PADDING_LINE = (PADDING, "line") + val PADDING_COMMAND = (PADDING, "command") val DIALOG = "dialog" val Result = new Properties.String(RESULT)