--- a/src/Pure/PIDE/markup.scala Wed Dec 12 21:50:42 2012 +0100
+++ b/src/Pure/PIDE/markup.scala Wed Dec 12 23:36:07 2012 +0100
@@ -215,16 +215,24 @@
/* active areas */
+ val GRAPHVIEW = "graphview"
+
val SENDBACK = "sendback"
+ val PADDING = "padding"
+ val PADDING_LINE = (PADDING, LINE)
val DIALOG = "dialog"
val DIALOG_RESULT = "dialog_result"
val Result = new Properties.String("result")
- val GRAPHVIEW = "graphview"
-
- val PADDING = "padding"
- val PADDING_LINE = (PADDING, LINE)
+ object Dialog_Args
+ {
+ def unapply(props: Properties.T): Option[(String, String)] =
+ (props, props) match {
+ case (Markup.Name(name), Markup.Result(result)) => Some((name, result))
+ case _ => None
+ }
+ }
val INTENSIFY = "intensify"