# HG changeset patch
# User wenzelm
# Date 1535920490 -7200
# Node ID 17486b8218e22e3a9c8fb48785300f6e7a894820
# Parent  9b97d0b20d95d42a6211196b0eef63c014f5b829
do not expose obscure flags;

diff -r 9b97d0b20d95 -r 17486b8218e2 src/Doc/System/Server.thy
--- a/src/Doc/System/Server.thy	Sun Sep 02 22:30:08 2018 +0200
+++ b/src/Doc/System/Server.thy	Sun Sep 02 22:34:50 2018 +0200
@@ -516,9 +516,9 @@
   session-qualified theory name (e.g.\ \<^verbatim>\<open>HOL-ex.Seq\<close>).
 
   \<^item> \<^bold>\<open>type\<close> \<open>node_status = {ok: bool, total: int, unprocessed: int, running:
-  int, warned: int, failed: int, finished: int, canceled: bool, initialized:
-  bool, consolidated: bool}\<close> represents a formal theory node status of the
-  PIDE document model as follows.
+  int, warned: int, failed: int, finished: int, canceled: bool, consolidated:
+  bool}\<close> represents a formal theory node status of the PIDE document model as
+  follows.
 
     \<^item> Fields \<open>total\<close>, \<open>unprocessed\<close>, \<open>running\<close>, \<open>warned\<close>, \<open>failed\<close>, \<open>finished\<close>
       account for individual commands within a theory node; \<open>ok\<close> is an
@@ -528,12 +528,6 @@
       spontaneously canceled (by an Interrupt exception that could also
       indicate resource problems).
 
-    \<^item> The \<open>terminated\<close> flag indicates that all evaluations in the node has
-      finished.
-
-    \<^item> The \<open>initialized\<close> flag indicates that the initial \<^theory_text>\<open>theory\<close> command has
-      been processed.
-
     \<^item> 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 9b97d0b20d95 -r 17486b8218e2 src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Sun Sep 02 22:30:08 2018 +0200
+++ b/src/Pure/PIDE/document_status.scala	Sun Sep 02 22:34:50 2018 +0200
@@ -141,8 +141,7 @@
     def json: JSON.Object.T =
       JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
         "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
-        "canceled" -> canceled, "terminated" -> terminated, "finalized" -> finalized,
-        "initialized" -> initialized, "consolidated" -> consolidated)
+        "canceled" -> canceled, "consolidated" -> consolidated)
   }