# HG changeset patch
# User wenzelm
# Date 1375817698 -7200
# Node ID 9a26ec5739dd633bedbd792235189448a1fd6d7a
# Parent  78989972d5b854f77d3c88c07f76f9b92c21112e
tuned -- more explicit type Status.Value;

diff -r 78989972d5b8 -r 9a26ec5739dd src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Tue Aug 06 21:08:04 2013 +0200
+++ b/src/Pure/PIDE/markup.scala	Tue Aug 06 21:34:58 2013 +0200
@@ -245,8 +245,6 @@
   val FINISHED = "finished"
   val FAILED = "failed"
 
-  val WAITING = "waiting"
-
 
   /* interactive documents */
 
diff -r 78989972d5b8 -r 9a26ec5739dd src/Tools/jEdit/src/query_operation.scala
--- a/src/Tools/jEdit/src/query_operation.scala	Tue Aug 06 21:08:04 2013 +0200
+++ b/src/Tools/jEdit/src/query_operation.scala	Tue Aug 06 21:34:58 2013 +0200
@@ -34,36 +34,20 @@
   private val instance = Document_ID.make().toString
 
 
-  /* animation */
-
-  private val passive_icon =
-    JEdit_Lib.load_image_icon(PIDE.options.string("process_passive_icon")).getImage
-  private val active_icons =
-    space_explode(':', PIDE.options.string("process_active_icons")).map(name =>
-      JEdit_Lib.load_image_icon(name).getImage)
+  /* implicit state -- owned by Swing thread */
 
-  val animation = new Label
-  private val animation_icon =
-    new AnimatedIcon(passive_icon, active_icons.toArray, 5, animation.peer)
-  animation.icon = animation_icon
-
-  private def animation_rate(rate: Int)
+  private object Status extends Enumeration
   {
-    animation_icon.stop
-    if (rate > 0) {
-      animation_icon.setRate(rate)
-      animation_icon.start
-    }
+    val WAITING = Value("waiting")
+    val RUNNING = Value("running")
+    val FINISHED = Value("finished")
   }
 
-
-  /* implicit state -- owned by Swing thread */
-
   private var current_location: Option[Command] = None
   private var current_query: List[String] = Nil
   private var current_update_pending = false
   private var current_output: List[XML.Tree] = Nil
-  private var current_status = Markup.FINISHED
+  private var current_status = Status.FINISHED
 
   private def reset_state()
   {
@@ -71,7 +55,7 @@
     current_query = Nil
     current_update_pending = false
     current_output = Nil
-    current_status = Markup.FINISHED
+    current_status = Status.FINISHED
   }
 
   private def remove_overlay()
@@ -85,7 +69,34 @@
     } model.remove_overlay(command, operation_name, instance :: current_query)
   }
 
-  private def handle_update()
+
+  /* animation */
+
+  val animation = new Label
+
+  private val passive_icon =
+    JEdit_Lib.load_image_icon(PIDE.options.string("process_passive_icon")).getImage
+  private val active_icons =
+    space_explode(':', PIDE.options.string("process_active_icons")).map(name =>
+      JEdit_Lib.load_image_icon(name).getImage)
+
+  private val animation_icon =
+    new AnimatedIcon(passive_icon, active_icons.toArray, 5, animation.peer)
+  animation.icon = animation_icon
+
+  private def animation_update()
+  {
+    animation_icon.stop
+    if (current_status != Status.FINISHED) {
+      animation_icon.setRate(if (current_status == Status.RUNNING) 15 else 5)
+      animation_icon.start
+    }
+  }
+
+
+  /* content update */
+
+  private def content_update()
   {
     Swing_Thread.require()
 
@@ -121,11 +132,13 @@
 
     /* status */
 
-    def status(name: String): Option[String] =
-      results.collectFirst({ case List(XML.Elem(m, _)) if m.name == name => name })
+    def get_status(name: String, status: Status.Value): Option[Status.Value] =
+      results.collectFirst({ case List(XML.Elem(m, _)) if m.name == name => status })
 
     val new_status =
-      status(Markup.FINISHED) orElse status(Markup.RUNNING) getOrElse Markup.WAITING
+      get_status(Markup.FINISHED, Status.FINISHED) orElse
+      get_status(Markup.RUNNING, Status.RUNNING) getOrElse
+      Status.WAITING
 
 
     /* state update */
@@ -134,25 +147,26 @@
       if (snapshot.is_outdated)
         current_update_pending = true
       else {
-        if (current_output != new_output)
+        current_update_pending = false
+        if (current_output != new_output) {
+          current_output = new_output
           consume_result(snapshot, state.results, new_output)
-        if (current_status != new_status)
-          new_status match {
-            case Markup.WAITING => animation_rate(5)
-            case Markup.RUNNING => animation_rate(15)
-            case Markup.FINISHED =>
-              animation_rate(0)
-              remove_overlay()
-              PIDE.flush_buffers()
-            case _ =>
+        }
+        if (current_status != new_status) {
+          current_status = new_status
+          animation_update()
+          if (new_status == Status.FINISHED) {
+            remove_overlay()
+            PIDE.flush_buffers()
           }
-        current_output = new_output
-        current_status = new_status
-        current_update_pending = false
+        }
       }
     }
   }
 
+
+  /* apply query */
+
   def apply_query(query: List[String])
   {
     Swing_Thread.require()
@@ -162,21 +176,23 @@
         val snapshot = doc_view.model.snapshot()
         remove_overlay()
         reset_state()
-        animation_rate(0)
         snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
           case Some(command) =>
             current_location = Some(command)
             current_query = query
-            current_status = Markup.WAITING
-            animation_rate(5)
+            current_status = Status.WAITING
             doc_view.model.insert_overlay(command, operation_name, instance :: query)
           case None =>
         }
+        animation_update()
         PIDE.flush_buffers()
       case None =>
     }
   }
 
+
+  /* locate query */
+
   def locate_query()
   {
     Swing_Thread.require()
@@ -205,8 +221,8 @@
           current_location match {
             case Some(command)
             if current_update_pending ||
-              (current_status != Markup.FINISHED && changed.commands.contains(command)) =>
-              Swing_Thread.later { handle_update() }
+              (current_status != Status.FINISHED && changed.commands.contains(command)) =>
+              Swing_Thread.later { content_update() }
             case _ =>
           }
         case bad =>