src/Pure/PIDE/query_operation.scala
changeset 54640 bbd2fa353809
parent 54327 148903e47b26
child 55618 995162143ef4
     1.1 --- a/src/Pure/PIDE/query_operation.scala	Wed Nov 20 23:00:18 2013 +0100
     1.2 +++ b/src/Pure/PIDE/query_operation.scala	Thu Nov 21 21:55:29 2013 +0100
     1.3 @@ -18,7 +18,6 @@
     1.4      val WAITING = Value("waiting")
     1.5      val RUNNING = Value("running")
     1.6      val FINISHED = Value("finished")
     1.7 -    val REMOVED = Value("removed")
     1.8    }
     1.9  }
    1.10  
    1.11 @@ -38,7 +37,7 @@
    1.12    private var current_query: List[String] = Nil
    1.13    private var current_update_pending = false
    1.14    private var current_output: List[XML.Tree] = Nil
    1.15 -  private var current_status = Query_Operation.Status.REMOVED
    1.16 +  private var current_status = Query_Operation.Status.FINISHED
    1.17    private var current_exec_id = Document_ID.none
    1.18  
    1.19    private def reset_state()
    1.20 @@ -47,7 +46,7 @@
    1.21      current_query = Nil
    1.22      current_update_pending = false
    1.23      current_output = Nil
    1.24 -    current_status = Query_Operation.Status.REMOVED
    1.25 +    current_status = Query_Operation.Status.FINISHED
    1.26      current_exec_id = Document_ID.none
    1.27    }
    1.28  
    1.29 @@ -89,13 +88,40 @@
    1.30        } yield elem).toList
    1.31  
    1.32  
    1.33 +    /* resolve sendback: static command id */
    1.34 +
    1.35 +    def resolve_sendback(body: XML.Body): XML.Body =
    1.36 +    {
    1.37 +      current_location match {
    1.38 +        case None => body
    1.39 +        case Some(command) =>
    1.40 +          def resolve(body: XML.Body): XML.Body =
    1.41 +            body map {
    1.42 +              case XML.Wrapped_Elem(m, b1, b2) => XML.Wrapped_Elem(m, resolve(b1), resolve(b2))
    1.43 +              case XML.Elem(Markup(Markup.SENDBACK, props), b) =>
    1.44 +                val props1 =
    1.45 +                  props.map({
    1.46 +                    case (Markup.ID, Properties.Value.Long(id)) if id == current_exec_id =>
    1.47 +                      (Markup.ID, Properties.Value.Long(command.id))
    1.48 +                    case p => p
    1.49 +                  })
    1.50 +                XML.Elem(Markup(Markup.SENDBACK, props1), resolve(b))
    1.51 +              case XML.Elem(m, b) => XML.Elem(m, resolve(b))
    1.52 +              case t => t
    1.53 +            }
    1.54 +          resolve(body)
    1.55 +      }
    1.56 +    }
    1.57 +
    1.58 +
    1.59      /* output */
    1.60  
    1.61      val new_output =
    1.62        for {
    1.63          XML.Elem(_, List(XML.Elem(markup, body))) <- results
    1.64          if Markup.messages.contains(markup.name)
    1.65 -      } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body)
    1.66 +        body1 = resolve_sendback(body)
    1.67 +      } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body1)
    1.68  
    1.69  
    1.70      /* status */
    1.71 @@ -105,7 +131,7 @@
    1.72        results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status })
    1.73  
    1.74      val new_status =
    1.75 -      if (removed) Query_Operation.Status.REMOVED
    1.76 +      if (removed) Query_Operation.Status.FINISHED
    1.77        else
    1.78          get_status(Markup.FINISHED, Query_Operation.Status.FINISHED) orElse
    1.79          get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse
    1.80 @@ -133,7 +159,7 @@
    1.81          if (current_status != new_status) {
    1.82            current_status = new_status
    1.83            consume_status(new_status)
    1.84 -          if (new_status == Query_Operation.Status.REMOVED)
    1.85 +          if (new_status == Query_Operation.Status.FINISHED)
    1.86              remove_overlay()
    1.87          }
    1.88        }
    1.89 @@ -192,7 +218,7 @@
    1.90            current_location match {
    1.91              case Some(command)
    1.92              if current_update_pending ||
    1.93 -              (current_status != Query_Operation.Status.REMOVED &&
    1.94 +              (current_status != Query_Operation.Status.FINISHED &&
    1.95                  changed.commands.contains(command)) =>
    1.96                Swing_Thread.later { content_update() }
    1.97              case _ =>