src/Pure/PIDE/query_operation.scala
changeset 53872 6e69f9ca8f1c
parent 53844 71f103629327
child 54310 6ddeb83eb67a
     1.1 --- a/src/Pure/PIDE/query_operation.scala	Wed Sep 25 10:26:04 2013 +0200
     1.2 +++ b/src/Pure/PIDE/query_operation.scala	Wed Sep 25 11:12:59 2013 +0200
     1.3 @@ -18,6 +18,7 @@
     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 @@ -37,7 +38,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.FINISHED
    1.16 +  private var current_status = Query_Operation.Status.REMOVED
    1.17    private var current_exec_id = Document_ID.none
    1.18  
    1.19    private def reset_state()
    1.20 @@ -46,7 +47,7 @@
    1.21      current_query = Nil
    1.22      current_update_pending = false
    1.23      current_output = Nil
    1.24 -    current_status = Query_Operation.Status.FINISHED
    1.25 +    current_status = Query_Operation.Status.REMOVED
    1.26      current_exec_id = Document_ID.none
    1.27    }
    1.28  
    1.29 @@ -100,7 +101,7 @@
    1.30        results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status })
    1.31  
    1.32      val new_status =
    1.33 -      if (removed) Query_Operation.Status.FINISHED
    1.34 +      if (removed) Query_Operation.Status.REMOVED
    1.35        else
    1.36          get_status(Markup.FINISHED, Query_Operation.Status.FINISHED) orElse
    1.37          get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse
    1.38 @@ -128,7 +129,7 @@
    1.39          if (current_status != new_status) {
    1.40            current_status = new_status
    1.41            consume_status(new_status)
    1.42 -          if (new_status == Query_Operation.Status.FINISHED) {
    1.43 +          if (new_status == Query_Operation.Status.REMOVED) {
    1.44              remove_overlay()
    1.45              editor.flush()
    1.46            }
    1.47 @@ -187,7 +188,7 @@
    1.48            current_location match {
    1.49              case Some(command)
    1.50              if current_update_pending ||
    1.51 -              (current_status != Query_Operation.Status.FINISHED &&
    1.52 +              (current_status != Query_Operation.Status.REMOVED &&
    1.53                  changed.commands.contains(command)) =>
    1.54                Swing_Thread.later { content_update() }
    1.55              case _ =>