src/Doc/System/Server.thy
changeset 68883 3653b3ad729e
parent 68882 344a4a8847be
child 68885 17486b8218e2
     1.1 --- a/src/Doc/System/Server.thy	Sun Sep 02 20:51:07 2018 +0200
     1.2 +++ b/src/Doc/System/Server.thy	Sun Sep 02 21:22:52 2018 +0200
     1.3 @@ -929,10 +929,9 @@
     1.4    \<^medskip>
     1.5    The \<^verbatim>\<open>use_theories\<close> command updates the identified session by adding the
     1.6    current version of theory files to it, while dependencies are resolved
     1.7 -  implicitly. The command succeeds eventually, when all theories have been
     1.8 -  \<^emph>\<open>consolidated\<close> in the sense the formal \<open>node_status\<close>
     1.9 -  (\secref{sec:json-types}): the outermost command structure has finished (or
    1.10 -  failed) and the final \<^theory_text>\<open>end\<close> command of each theory has been checked.
    1.11 +  implicitly. The command succeeds eventually, when all theories have status
    1.12 +  \<^emph>\<open>terminated\<close> or \<^emph>\<open>consolidated\<close> in the sense of \<open>node_status\<close>
    1.13 +  (\secref{sec:json-types}).
    1.14  
    1.15    Already used theories persist in the session until purged explicitly
    1.16    (\secref{sec:command-purge-theories}). This also means that repeated
    1.17 @@ -948,14 +947,10 @@
    1.18    represented as plain text in UTF-8 encoding, which means the string needs to
    1.19    be decoded as in \<^verbatim>\<open>java.util.Base64.getDecoder.decode(String)\<close>.
    1.20  
    1.21 -  \<^medskip> Due to asynchronous nature of PIDE document processing, structurally
    1.22 -  broken theories never reach the \<open>consolidated\<close> state: consequently
    1.23 -  \<^verbatim>\<open>use_theories\<close> will wait forever. The status is checked every \<open>check_delay\<close>
    1.24 -  seconds, and bounded by \<open>check_limit\<close> attempts (default: 0, i.e.\
    1.25 -  unbounded). A \<open>check_limit > 0\<close> effectively specifies a timeout of
    1.26 -  \<open>check_delay \<times> check_limit\<close> seconds; it needs to be greater than the system
    1.27 -  option @{system_option editor_consolidate_delay} to give PIDE processing a
    1.28 -  chance to consolidate document nodes in the first place.
    1.29 +  \<^medskip> The status of PIDE processing is checked every \<open>check_delay\<close> seconds, and
    1.30 +  bounded by \<open>check_limit\<close> attempts (default: 0, i.e.\ unbounded). A
    1.31 +  \<open>check_limit > 0\<close> effectively specifies a timeout of \<open>check_delay \<times>
    1.32 +  check_limit\<close> seconds.
    1.33  
    1.34    \<^medskip> A non-negative \<open>nodes_status_delay\<close> enables continuous notifications of
    1.35    kind \<open>nodes_status\<close>, with a field of name and type \<open>nodes_status\<close>. The time