# HG changeset patch
# User wenzelm
# Date 1535914058 -7200
# Node ID d975449b266eb70453cd106b27e0a769667cf532
# Parent  8b98db8fd183121d4807ab78b9c13e35cfa4bd9f
more detailed node_status;

diff -r 8b98db8fd183 -r d975449b266e src/Doc/System/Server.thy
--- a/src/Doc/System/Server.thy	Sun Sep 02 20:37:38 2018 +0200
+++ b/src/Doc/System/Server.thy	Sun Sep 02 20:47:38 2018 +0200
@@ -522,7 +522,8 @@
   \<open>failed\<close>, \<open>finished\<close> account for individual commands within a theory node;
   \<open>ok\<close> is an abstraction for \<open>failed = 0\<close>. The \<open>canceled\<close> flag tells if some
   command in the theory has been spontaneously canceled (by an Interrupt
-  exception that could also indicate resource problems). The \<open>initialized\<close>
+  exception that could also indicate resource problems). The \<open>terminated\<close> flag
+  indicates that all evaluations in the node has finished. The \<open>initialized\<close>
   flag indicates that the initial \<^theory_text>\<open>theory\<close> command has been processed. The
   \<open>consolidated\<close> flag indicates whether the outermost theory command structure
   has finished (or failed) and the final \<^theory_text>\<open>end\<close> command has been checked.
diff -r 8b98db8fd183 -r d975449b266e src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Sun Sep 02 20:37:38 2018 +0200
+++ b/src/Pure/PIDE/document_status.scala	Sun Sep 02 20:47:38 2018 +0200
@@ -80,6 +80,7 @@
     def is_failed: Boolean = failed
     def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
     def is_canceled: Boolean = canceled
+    def is_terminated: Boolean = canceled || touched && forks == 0 && runs == 0
   }
 
 
@@ -100,6 +101,7 @@
       var failed = 0
       var finished = 0
       var canceled = false
+      var terminated = false
       for (command <- node.commands.iterator) {
         val states = state.command_states(version, command)
         val status = Command_Status.merge(states.iterator.map(_.document_status))
@@ -111,18 +113,19 @@
         else unprocessed += 1
 
         if (status.is_canceled) canceled = true
+        if (status.is_terminated) terminated = true
       }
       val initialized = state.node_initialized(version, name)
       val consolidated = state.node_consolidated(version, name)
 
-      Node_Status(
-        unprocessed, running, warned, failed, finished, canceled, initialized, consolidated)
+      Node_Status(unprocessed, running, warned, failed, finished, canceled, terminated,
+        initialized, consolidated)
     }
   }
 
   sealed case class Node_Status(
     unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int,
-    canceled: Boolean, initialized: Boolean, consolidated: Boolean)
+    canceled: Boolean, terminated: Boolean, initialized: Boolean, consolidated: Boolean)
   {
     def ok: Boolean = failed == 0
     def total: Int = unprocessed + running + warned + failed + finished
@@ -130,7 +133,8 @@
     def json: JSON.Object.T =
       JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
         "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
-        "canceled" -> canceled, "initialized" -> initialized, "consolidated" -> consolidated)
+        "canceled" -> canceled, "terminated" -> terminated, "initialized" -> initialized,
+        "consolidated" -> consolidated)
   }