changeset 50215 | 97959912840a |
parent 50201 | c26369c9eda6 |
child 50255 | d0ec1f0d1d7d |
--- a/src/Pure/PIDE/markup.scala Mon Nov 26 14:43:28 2012 +0100 +++ b/src/Pure/PIDE/markup.scala Mon Nov 26 16:16:47 2012 +0100 @@ -211,7 +211,11 @@ val STATE = "state" val SUBGOAL = "subgoal" + + val PADDING = "padding" + val PADDING_LINE = (PADDING, LINE) val SENDBACK = "sendback" + val INTENSIFY = "intensify"