# HG changeset patch
# User wenzelm
# Date 1346418224 -7200
# Node ID e780d1bf767e4dc831a31da069a5da8b1ecd6bf3
# Parent  2f0530b81c45dc4eecaa6984b9ffc16b08e2b9f1
clarified command status (again);

diff -r 2f0530b81c45 -r e780d1bf767e src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Fri Aug 31 14:52:29 2012 +0200
+++ b/src/Pure/PIDE/protocol.scala	Fri Aug 31 15:03:44 2012 +0200
@@ -61,7 +61,7 @@
 
     def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
     def is_running: Boolean = runs != 0
-    def is_finished: Boolean = !failed && forks == 0 && runs == 0
+    def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
     def is_failed: Boolean = failed
   }