# HG changeset patch
# User wenzelm
# Date 1532723017 -7200
# Node ID 9072bfd24d8f71c5803481cb5a94c15e6eb8f4ef
# Parent  03e104be99af3a34d8f042cbcc8d0484c81a4b0d
clarified documentation;

diff -r 03e104be99af -r 9072bfd24d8f src/Doc/System/Server.thy
--- a/src/Doc/System/Server.thy	Fri Jul 27 22:09:27 2018 +0200
+++ b/src/Doc/System/Server.thy	Fri Jul 27 22:23:37 2018 +0200
@@ -937,7 +937,9 @@
   \<^verbatim>\<open>use_theories\<close> will wait forever. The status is checked every \<open>check_delay\<close>
   seconds, and bounded by \<open>check_limit\<close> attempts (default: 0, i.e.\
   unbounded). A \<open>check_limit > 0\<close> effectively specifies a timeout of
-  \<open>check_delay \<times> check_limit\<close> seconds.
+  \<open>check_delay \<times> check_limit\<close> seconds; it needs to be greater than the system
+  option @{system_option editor_consolidate_delay} to give PIDE processing a
+  chance to consolidate document nodes in the first place.
 \<close>