changeset 50450 | 358b6020f8b6 |
parent 50255 | d0ec1f0d1d7d |
child 50498 | 6647ba2775c1 |
--- a/src/Pure/PIDE/markup.scala Mon Dec 10 10:41:29 2012 +0100 +++ b/src/Pure/PIDE/markup.scala Mon Dec 10 13:52:33 2012 +0100 @@ -212,9 +212,14 @@ val STATE = "state" val SUBGOAL = "subgoal" + + /* active areas */ + + val SENDBACK = "sendback" + val GRAPHVIEW = "graphview" + val PADDING = "padding" val PADDING_LINE = (PADDING, LINE) - val SENDBACK = "sendback" val INTENSIFY = "intensify" @@ -280,8 +285,6 @@ val BAD = "bad" - val GRAPHVIEW = "graphview" - /* protocol message functions */