--- a/src/Doc/System/Server.thy Tue Sep 04 15:01:05 2018 +0200
+++ b/src/Doc/System/Server.thy Tue Sep 04 16:23:54 2018 +0200
@@ -909,6 +909,7 @@
\quad~~\<open>export_pattern?: string,\<close> \\
\quad~~\<open>check_delay?: double,\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>0.5\<close> \\
\quad~~\<open>check_limit?: int,\<close> \\
+ \quad~~\<open>watchdog_timeout?: double,\<close> \\
\quad~~\<open>nodes_status_delay?: double}\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>-1.0\<close> \\
\end{tabular}
@@ -948,9 +949,13 @@
\<^medskip> The status of PIDE processing 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>
+ \<open>check_limit > 0\<close> effectively specifies a global timeout of \<open>check_delay \<times>
check_limit\<close> seconds.
+ \<^medskip> If \<open>watchdog_timeout\<close> is greater than 0, it specifies the timespan (in
+ seconds) after the last command status change of Isabelle/PIDE, before
+ finishing with a potentially non-terminating or deadlocked execution.
+
\<^medskip> A non-negative \<open>nodes_status_delay\<close> enables continuous notifications of
kind \<open>nodes_status\<close>, with a field of name and type \<open>nodes_status\<close>. The time
interval is specified in seconds; by default it is negative and thus