| 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"