src/Pure/PIDE/markup.scala
changeset 50498 6647ba2775c1
parent 50450 358b6020f8b6
child 50499 f496b2b7bafb
--- a/src/Pure/PIDE/markup.scala	Wed Dec 12 19:03:49 2012 +0100
+++ b/src/Pure/PIDE/markup.scala	Wed Dec 12 21:50:42 2012 +0100
@@ -216,6 +216,11 @@
   /* active areas */
 
   val SENDBACK = "sendback"
+
+  val DIALOG = "dialog"
+  val DIALOG_RESULT = "dialog_result"
+  val Result = new Properties.String("result")
+
   val GRAPHVIEW = "graphview"
 
   val PADDING = "padding"