src/Pure/PIDE/markup.scala
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 */