# HG changeset patch
# User wenzelm
# Date 1535914267 -7200
# Node ID 344a4a8847befc0fa353ca735a08850222fb4dad
# Parent  d975449b266eb70453cd106b27e0a769667cf532
tuned documentation;

diff -r d975449b266e -r 344a4a8847be src/Doc/System/Server.thy
--- a/src/Doc/System/Server.thy	Sun Sep 02 20:47:38 2018 +0200
+++ b/src/Doc/System/Server.thy	Sun Sep 02 20:51:07 2018 +0200
@@ -518,15 +518,25 @@
   \<^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. 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 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>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.
+  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
+      abstraction for \<open>failed = 0\<close>.
+
+    \<^item> 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).
+
+    \<^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.
 \<close>