support for watchdog_timeout;
authorwenzelm
Tue Sep 04 16:23:54 2018 +0200 (9 months ago)
changeset 68908abc338d25640
parent 68907 3afa4f03864b
child 68909 34e777447ed5
support for watchdog_timeout;
src/Doc/System/Server.thy
src/Pure/Thy/thy_resources.scala
src/Pure/Tools/server_commands.scala
     1.1 --- a/src/Doc/System/Server.thy	Tue Sep 04 15:01:05 2018 +0200
     1.2 +++ b/src/Doc/System/Server.thy	Tue Sep 04 16:23:54 2018 +0200
     1.3 @@ -909,6 +909,7 @@
     1.4    \quad~~\<open>export_pattern?: string,\<close> \\
     1.5    \quad~~\<open>check_delay?: double,\<close>  & \<^bold>\<open>default:\<close> \<^verbatim>\<open>0.5\<close> \\
     1.6    \quad~~\<open>check_limit?: int,\<close> \\
     1.7 +  \quad~~\<open>watchdog_timeout?: double,\<close> \\
     1.8    \quad~~\<open>nodes_status_delay?: double}\<close>  & \<^bold>\<open>default:\<close> \<^verbatim>\<open>-1.0\<close> \\
     1.9    \end{tabular}
    1.10  
    1.11 @@ -948,9 +949,13 @@
    1.12  
    1.13    \<^medskip> The status of PIDE processing is checked every \<open>check_delay\<close> seconds, and
    1.14    bounded by \<open>check_limit\<close> attempts (default: 0, i.e.\ unbounded). A
    1.15 -  \<open>check_limit > 0\<close> effectively specifies a timeout of \<open>check_delay \<times>
    1.16 +  \<open>check_limit > 0\<close> effectively specifies a global timeout of \<open>check_delay \<times>
    1.17    check_limit\<close> seconds.
    1.18  
    1.19 +  \<^medskip> If \<open>watchdog_timeout\<close> is greater than 0, it specifies the timespan (in
    1.20 +  seconds) after the last command status change of Isabelle/PIDE, before
    1.21 +  finishing with a potentially non-terminating or deadlocked execution.
    1.22 +
    1.23    \<^medskip> A non-negative \<open>nodes_status_delay\<close> enables continuous notifications of
    1.24    kind \<open>nodes_status\<close>, with a field of name and type \<open>nodes_status\<close>. The time
    1.25    interval is specified in seconds; by default it is negative and thus
     2.1 --- a/src/Pure/Thy/thy_resources.scala	Tue Sep 04 15:01:05 2018 +0200
     2.2 +++ b/src/Pure/Thy/thy_resources.scala	Tue Sep 04 16:23:54 2018 +0200
     2.3 @@ -102,6 +102,7 @@
     2.4        master_dir: String = "",
     2.5        check_delay: Time = Time.seconds(default_check_delay),
     2.6        check_limit: Int = 0,
     2.7 +      watchdog_timeout: Time = Time.zero,
     2.8        nodes_status_delay: Time = Time.seconds(default_nodes_status_delay),
     2.9        id: UUID = UUID(),
    2.10        progress: Progress = No_Progress): Theories_Result =
    2.11 @@ -119,12 +120,16 @@
    2.12  
    2.13        val result = Future.promise[Theories_Result]
    2.14  
    2.15 +      var watchdog_time = Synchronized(Time.now())
    2.16 +      def watchdog: Boolean =
    2.17 +        watchdog_timeout > Time.zero && Time.now() - watchdog_time.value > watchdog_timeout
    2.18 +
    2.19        def check_state(beyond_limit: Boolean = false)
    2.20        {
    2.21          val state = session.current_state()
    2.22          state.stable_tip_version match {
    2.23            case Some(version) =>
    2.24 -            if (beyond_limit ||
    2.25 +            if (beyond_limit || watchdog ||
    2.26                  dep_theories.forall(name =>
    2.27                    state.node_consolidated(version, name) ||
    2.28                    current_nodes_status.value.quasi_consolidated(name)))
    2.29 @@ -168,6 +173,8 @@
    2.30                val state = snapshot.state
    2.31                val version = snapshot.version
    2.32  
    2.33 +              watchdog_time.change(_ => Time.now())
    2.34 +
    2.35                val theory_percentages =
    2.36                  current_nodes_status.change_result(nodes_status =>
    2.37                    {
     3.1 --- a/src/Pure/Tools/server_commands.scala	Tue Sep 04 15:01:05 2018 +0200
     3.2 +++ b/src/Pure/Tools/server_commands.scala	Tue Sep 04 16:23:54 2018 +0200
     3.3 @@ -160,6 +160,7 @@
     3.4        export_pattern: String = "",
     3.5        check_delay: Double = Thy_Resources.default_check_delay,
     3.6        check_limit: Int = 0,
     3.7 +      watchdog_timeout: Double = 0.0,
     3.8        nodes_status_delay: Double = Thy_Resources.default_nodes_status_delay)
     3.9  
    3.10      def unapply(json: JSON.T): Option[Args] =
    3.11 @@ -172,13 +173,14 @@
    3.12          export_pattern <- JSON.string_default(json, "export_pattern")
    3.13          check_delay <- JSON.double_default(json, "check_delay", Thy_Resources.default_check_delay)
    3.14          check_limit <- JSON.int_default(json, "check_limit")
    3.15 +        watchdog_timeout <- JSON.double_default(json, "watchdog_timeout")
    3.16          nodes_status_delay <-
    3.17            JSON.double_default(json, "nodes_status_delay", Thy_Resources.default_nodes_status_delay)
    3.18        }
    3.19        yield {
    3.20          Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin,
    3.21            unicode_symbols = unicode_symbols, export_pattern = export_pattern,
    3.22 -          check_delay = check_delay, check_limit = check_limit,
    3.23 +          check_delay = check_delay, check_limit = check_limit, watchdog_timeout = watchdog_timeout,
    3.24            nodes_status_delay = nodes_status_delay)
    3.25        }
    3.26  
    3.27 @@ -190,6 +192,7 @@
    3.28        val result =
    3.29          session.use_theories(args.theories, master_dir = args.master_dir,
    3.30            check_delay = Time.seconds(args.check_delay), check_limit = args.check_limit,
    3.31 +          watchdog_timeout = Time.seconds(args.watchdog_timeout),
    3.32            nodes_status_delay = Time.seconds(args.nodes_status_delay),
    3.33            id = id, progress = progress)
    3.34