src/Pure/PIDE/markup.scala
changeset 50499 f496b2b7bafb
parent 50498 6647ba2775c1
child 50500 c94bba7906d2
     1.1 --- a/src/Pure/PIDE/markup.scala	Wed Dec 12 21:50:42 2012 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Wed Dec 12 23:36:07 2012 +0100
     1.3 @@ -215,16 +215,24 @@
     1.4  
     1.5    /* active areas */
     1.6  
     1.7 +  val GRAPHVIEW = "graphview"
     1.8 +
     1.9    val SENDBACK = "sendback"
    1.10 +  val PADDING = "padding"
    1.11 +  val PADDING_LINE = (PADDING, LINE)
    1.12  
    1.13    val DIALOG = "dialog"
    1.14    val DIALOG_RESULT = "dialog_result"
    1.15    val Result = new Properties.String("result")
    1.16  
    1.17 -  val GRAPHVIEW = "graphview"
    1.18 -
    1.19 -  val PADDING = "padding"
    1.20 -  val PADDING_LINE = (PADDING, LINE)
    1.21 +  object Dialog_Args
    1.22 +  {
    1.23 +    def unapply(props: Properties.T): Option[(String, String)] =
    1.24 +      (props, props) match {
    1.25 +        case (Markup.Name(name), Markup.Result(result)) => Some((name, result))
    1.26 +        case _ => None
    1.27 +      }
    1.28 +  }
    1.29  
    1.30    val INTENSIFY = "intensify"
    1.31