# HG changeset patch
# User wenzelm
# Date 1326551454 -3600
# Node ID aad604f74be0a74768757b3185613d17cf4d610a
# Parent  4cab63a6dc160f2d7e8e3a0b49eb8c5f046a987a
tuned comments;

diff -r 4cab63a6dc16 -r aad604f74be0 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Sat Jan 14 15:20:29 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala	Sat Jan 14 15:30:54 2012 +0100
@@ -41,7 +41,7 @@
   }
 
 
-  /* toplevel transactions */
+  /* command status */
 
   sealed case class Status(
     private val finished: Boolean = false,
@@ -70,6 +70,9 @@
   def command_status(markups: List[Markup]): Status =
     (Status() /: markups)(command_status(_, _))
 
+
+  /* node status */
+
   sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int)
   {
     def total: Int = unprocessed + running + finished + failed