# 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>\use_theories\ will wait forever. The status is checked every \check_delay\ seconds, and bounded by \check_limit\ attempts (default: 0, i.e.\ unbounded). A \check_limit > 0\ effectively specifies a timeout of - \check_delay \ check_limit\ seconds. + \check_delay \ check_limit\ 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. \