clarified documentation;
authorwenzelm
Fri Jul 27 22:23:37 2018 +0200 (11 months ago)
changeset 686959072bfd24d8f
parent 68694 03e104be99af
child 68696 8a071eeddb2a
clarified documentation;
src/Doc/System/Server.thy
     1.1 --- a/src/Doc/System/Server.thy	Fri Jul 27 22:09:27 2018 +0200
     1.2 +++ b/src/Doc/System/Server.thy	Fri Jul 27 22:23:37 2018 +0200
     1.3 @@ -937,7 +937,9 @@
     1.4    \<^verbatim>\<open>use_theories\<close> will wait forever. The status is checked every \<open>check_delay\<close>
     1.5    seconds, and bounded by \<open>check_limit\<close> attempts (default: 0, i.e.\
     1.6    unbounded). A \<open>check_limit > 0\<close> effectively specifies a timeout of
     1.7 -  \<open>check_delay \<times> check_limit\<close> seconds.
     1.8 +  \<open>check_delay \<times> check_limit\<close> seconds; it needs to be greater than the system
     1.9 +  option @{system_option editor_consolidate_delay} to give PIDE processing a
    1.10 +  chance to consolidate document nodes in the first place.
    1.11  \<close>
    1.12  
    1.13