# HG changeset patch
# User wenzelm
# Date 1536071034 -7200
# Node ID abc338d25640478fa221994a4f572343ff19f2dd
# Parent  3afa4f03864bda9a0961430bfe94de0f0b824ef5
support for watchdog_timeout;

diff -r 3afa4f03864b -r abc338d25640 src/Doc/System/Server.thy
--- 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
diff -r 3afa4f03864b -r abc338d25640 src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Tue Sep 04 15:01:05 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala	Tue Sep 04 16:23:54 2018 +0200
@@ -102,6 +102,7 @@
       master_dir: String = "",
       check_delay: Time = Time.seconds(default_check_delay),
       check_limit: Int = 0,
+      watchdog_timeout: Time = Time.zero,
       nodes_status_delay: Time = Time.seconds(default_nodes_status_delay),
       id: UUID = UUID(),
       progress: Progress = No_Progress): Theories_Result =
@@ -119,12 +120,16 @@
 
       val result = Future.promise[Theories_Result]
 
+      var watchdog_time = Synchronized(Time.now())
+      def watchdog: Boolean =
+        watchdog_timeout > Time.zero && Time.now() - watchdog_time.value > watchdog_timeout
+
       def check_state(beyond_limit: Boolean = false)
       {
         val state = session.current_state()
         state.stable_tip_version match {
           case Some(version) =>
-            if (beyond_limit ||
+            if (beyond_limit || watchdog ||
                 dep_theories.forall(name =>
                   state.node_consolidated(version, name) ||
                   current_nodes_status.value.quasi_consolidated(name)))
@@ -168,6 +173,8 @@
               val state = snapshot.state
               val version = snapshot.version
 
+              watchdog_time.change(_ => Time.now())
+
               val theory_percentages =
                 current_nodes_status.change_result(nodes_status =>
                   {
diff -r 3afa4f03864b -r abc338d25640 src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Tue Sep 04 15:01:05 2018 +0200
+++ b/src/Pure/Tools/server_commands.scala	Tue Sep 04 16:23:54 2018 +0200
@@ -160,6 +160,7 @@
       export_pattern: String = "",
       check_delay: Double = Thy_Resources.default_check_delay,
       check_limit: Int = 0,
+      watchdog_timeout: Double = 0.0,
       nodes_status_delay: Double = Thy_Resources.default_nodes_status_delay)
 
     def unapply(json: JSON.T): Option[Args] =
@@ -172,13 +173,14 @@
         export_pattern <- JSON.string_default(json, "export_pattern")
         check_delay <- JSON.double_default(json, "check_delay", Thy_Resources.default_check_delay)
         check_limit <- JSON.int_default(json, "check_limit")
+        watchdog_timeout <- JSON.double_default(json, "watchdog_timeout")
         nodes_status_delay <-
           JSON.double_default(json, "nodes_status_delay", Thy_Resources.default_nodes_status_delay)
       }
       yield {
         Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin,
           unicode_symbols = unicode_symbols, export_pattern = export_pattern,
-          check_delay = check_delay, check_limit = check_limit,
+          check_delay = check_delay, check_limit = check_limit, watchdog_timeout = watchdog_timeout,
           nodes_status_delay = nodes_status_delay)
       }
 
@@ -190,6 +192,7 @@
       val result =
         session.use_theories(args.theories, master_dir = args.master_dir,
           check_delay = Time.seconds(args.check_delay), check_limit = args.check_limit,
+          watchdog_timeout = Time.seconds(args.watchdog_timeout),
           nodes_status_delay = Time.seconds(args.nodes_status_delay),
           id = id, progress = progress)