src/Pure/PIDE/protocol.scala
changeset 50501 6f41f1646617
parent 50500 c94bba7906d2
child 50507 9605b0d93d1e
     1.1 --- a/src/Pure/PIDE/protocol.scala	Thu Dec 13 13:52:18 2012 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Thu Dec 13 17:29:23 2012 +0100
     1.3 @@ -209,13 +209,15 @@
     1.4  
     1.5    object Dialog_Result
     1.6    {
     1.7 -    def apply(serial: Long, result: String): XML.Elem =
     1.8 -      XML.Elem(Markup(Markup.RESULT, Markup.Serial(serial)), List(XML.Text(result)))
     1.9 +    def apply(id: Document.ID, serial: Long, result: String): XML.Elem =
    1.10 +    {
    1.11 +      val props = Position.Id(id) ::: Markup.Serial(serial)
    1.12 +      XML.Elem(Markup(Markup.RESULT, props), List(XML.Text(result)))
    1.13 +    }
    1.14  
    1.15 -    def unapply(tree: XML.Tree): Option[(Long, String)] =
    1.16 +    def unapply(tree: XML.Tree): Option[String] =
    1.17        tree match {
    1.18 -        case XML.Elem(Markup(Markup.RESULT, Markup.Serial(serial)), List(XML.Text(result))) =>
    1.19 -          Some((serial, result))
    1.20 +        case XML.Elem(Markup(Markup.RESULT, _), List(XML.Text(result))) => Some(result)
    1.21          case _ => None
    1.22        }
    1.23    }