# 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~~\export_pattern?: string,\ \\ \quad~~\check_delay?: double,\ & \<^bold>\default:\ \<^verbatim>\0.5\ \\ \quad~~\check_limit?: int,\ \\ + \quad~~\watchdog_timeout?: double,\ \\ \quad~~\nodes_status_delay?: double}\ & \<^bold>\default:\ \<^verbatim>\-1.0\ \\ \end{tabular} @@ -948,9 +949,13 @@ \<^medskip> The status of PIDE processing is checked every \check_delay\ seconds, and bounded by \check_limit\ attempts (default: 0, i.e.\ unbounded). A - \check_limit > 0\ effectively specifies a timeout of \check_delay \ + \check_limit > 0\ effectively specifies a global timeout of \check_delay \ check_limit\ seconds. + \<^medskip> If \watchdog_timeout\ 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 \nodes_status_delay\ enables continuous notifications of kind \nodes_status\, with a field of name and type \nodes_status\. 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)