changeset 52697 | 6fb98a20c349 |
parent 52643 | 34c29356930e |
child 52800 | 1baa5d19ac44 |
--- 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)