--- a/src/Doc/System/Server.thy Sat Sep 08 08:09:07 2018 +0000
+++ b/src/Doc/System/Server.thy Sat Sep 08 16:55:38 2018 +0200
@@ -909,7 +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>watchdog_timeout?: double,\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>600.0\<close> \\
\quad~~\<open>nodes_status_delay?: double}\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>-1.0\<close> \\
\end{tabular}
--- a/src/Pure/General/json.scala Sat Sep 08 08:09:07 2018 +0000
+++ b/src/Pure/General/json.scala Sat Sep 08 16:55:38 2018 +0200
@@ -309,6 +309,11 @@
case _ => None
}
}
+
+ object Seconds {
+ def unapply(json: T): Option[Time] =
+ Double.unapply(json).map(Time.seconds(_))
+ }
}
@@ -381,4 +386,9 @@
list(obj, name, JSON.Value.String.unapply _)
def strings_default(obj: T, name: String, default: => List[String] = Nil): Option[List[String]] =
list_default(obj, name, JSON.Value.String.unapply _, default)
+
+ def seconds(obj: T, name: String): Option[Time] =
+ value(obj, name, Value.Seconds.unapply)
+ def seconds_default(obj: T, name: String, default: => Time = Time.zero): Option[Time] =
+ value_default(obj, name, Value.Seconds.unapply, default)
}
--- a/src/Pure/General/value.scala Sat Sep 08 08:09:07 2018 +0000
+++ b/src/Pure/General/value.scala Sat Sep 08 16:55:38 2018 +0200
@@ -51,4 +51,16 @@
def parse(s: java.lang.String): scala.Double =
unapply(s) getOrElse error("Bad real: " + quote(s))
}
+
+ object Seconds
+ {
+ def apply(t: Time): java.lang.String =
+ {
+ val s = t.seconds
+ if (s.toInt.toDouble == s) s.toInt.toString else t.toString
+ }
+ def unapply(s: java.lang.String): Option[Time] = Double.unapply(s).map(Time.seconds(_))
+ def parse(s: java.lang.String): Time =
+ unapply(s) getOrElse error("Bad real (for seconds): " + quote(s))
+ }
}
--- a/src/Pure/Thy/thy_resources.scala Sat Sep 08 08:09:07 2018 +0000
+++ b/src/Pure/Thy/thy_resources.scala Sat Sep 08 16:55:38 2018 +0200
@@ -78,9 +78,10 @@
(nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok })
}
- val default_check_delay: Double = 0.5
- val default_nodes_status_delay: Double = -1.0
- val default_commit_clean_delay: Double = 60.0
+ val default_check_delay = Time.seconds(0.5)
+ val default_nodes_status_delay = Time.seconds(-1.0)
+ val default_commit_clean_delay = Time.seconds(60.0)
+ val default_watchdog_timeout = Time.seconds(600.0)
class Session private[Thy_Resources](
@@ -152,18 +153,23 @@
{
val st1 =
if (commit.isDefined) {
- val committed =
- for {
- name <- dep_theories
- if !already_committed.isDefinedAt(name) && state.node_consolidated(version, name)
- }
- yield {
- val snapshot = stable_snapshot(state, version, name)
- val status = Document_Status.Node_Status.make(state, version, name)
- commit.get.apply(snapshot, status)
- (name -> status)
- }
- copy(already_committed = already_committed ++ committed)
+ val already_committed1 =
+ (already_committed /: dep_theories)({ case (committed, name) =>
+ def parents_committed: Boolean =
+ version.nodes(name).header.imports.forall({ case (parent, _) =>
+ Sessions.is_pure(parent.theory) || committed.isDefinedAt(parent)
+ })
+ if (!committed.isDefinedAt(name) && parents_committed &&
+ state.node_consolidated(version, name))
+ {
+ val snapshot = stable_snapshot(state, version, name)
+ val status = Document_Status.Node_Status.make(state, version, name)
+ commit.get.apply(snapshot, status)
+ committed + (name -> status)
+ }
+ else committed
+ })
+ copy(already_committed = already_committed1)
}
else this
@@ -194,14 +200,14 @@
theories: List[String],
qualifier: String = Sessions.DRAFT,
master_dir: String = "",
- check_delay: Time = Time.seconds(default_check_delay),
+ check_delay: Time = default_check_delay,
check_limit: Int = 0,
- watchdog_timeout: Time = Time.zero,
- nodes_status_delay: Time = Time.seconds(default_nodes_status_delay),
+ watchdog_timeout: Time = default_watchdog_timeout,
+ nodes_status_delay: Time = default_nodes_status_delay,
id: UUID = UUID(),
// commit: must not block, must not fail
commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None,
- commit_clean_delay: Time = Time.seconds(default_commit_clean_delay),
+ commit_clean_delay: Time = default_commit_clean_delay,
progress: Progress = No_Progress): Theories_Result =
{
val dep_theories =
@@ -303,7 +309,7 @@
check_result()
- if (commit.isDefined && commit_clean_delay >= Time.zero) {
+ if (commit.isDefined && commit_clean_delay > Time.zero) {
if (use_theories_state.value.finished_result)
delay_commit_clean.revoke
else delay_commit_clean.invoke
--- a/src/Pure/Tools/dump.scala Sat Sep 08 08:09:07 2018 +0000
+++ b/src/Pure/Tools/dump.scala Sat Sep 08 16:55:38 2018 +0200
@@ -75,8 +75,7 @@
/* dump */
- val default_output_dir = Path.explode("dump")
- val default_commit_clean_delay = Time.seconds(-1.0)
+ val default_output_dir: Path = Path.explode("dump")
def make_options(options: Options, aspects: List[Aspect]): Options =
{
@@ -92,7 +91,8 @@
select_dirs: List[Path] = Nil,
output_dir: Path = default_output_dir,
verbose: Boolean = false,
- commit_clean_delay: Time = default_commit_clean_delay,
+ commit_clean_delay: Time = Thy_Resources.default_commit_clean_delay,
+ watchdog_timeout: Time = Thy_Resources.default_watchdog_timeout,
system_mode: Boolean = false,
selection: Sessions.Selection = Sessions.Selection.empty): Process_Result =
{
@@ -163,7 +163,8 @@
session.use_theories(use_theories,
progress = progress,
commit = Some(Consumer.apply _),
- commit_clean_delay = commit_clean_delay)
+ commit_clean_delay = commit_clean_delay,
+ watchdog_timeout = watchdog_timeout)
val session_result = session.stop()
@@ -181,10 +182,11 @@
{
var aspects: List[Aspect] = known_aspects
var base_sessions: List[String] = Nil
- var commit_clean_delay = default_commit_clean_delay
+ var commit_clean_delay = Thy_Resources.default_commit_clean_delay
var select_dirs: List[Path] = Nil
var output_dir = default_output_dir
var requirements = false
+ var watchdog_timeout = Thy_Resources.default_watchdog_timeout
var exclude_session_groups: List[String] = Nil
var all_sessions = false
var dirs: List[Path] = Nil
@@ -201,11 +203,13 @@
Options are:
-A NAMES dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
-B NAME include session NAME and all descendants
- -C SECONDS delay for cleaning of already dumped theories (disabled for < 0, default: """ +
- default_commit_clean_delay.seconds.toInt + """)
+ -C SECONDS delay for cleaning of already dumped theories (0 = disabled, default: """ +
+ Value.Seconds(Thy_Resources.default_commit_clean_delay) + """)
-D DIR include session directory and select its sessions
-O DIR output directory for dumped files (default: """ + default_output_dir + """)
-R operate on requirements of selected sessions
+ -W SECONDS watchdog timeout for PIDE processing (0 = disabled, default: """ +
+ Value.Seconds(Thy_Resources.default_watchdog_timeout) + """)
-X NAME exclude sessions from group NAME and all descendants
-a select all sessions
-d DIR include session directory
@@ -221,10 +225,11 @@
""" + Library.prefix_lines(" ", show_aspects) + "\n",
"A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),
"B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
- "C:" -> (arg => commit_clean_delay = Time.seconds(Value.Double.parse(arg))),
+ "C:" -> (arg => commit_clean_delay = Value.Seconds.parse(arg)),
"D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
"O:" -> (arg => output_dir = Path.explode(arg)),
"R" -> (_ => requirements = true),
+ "W:" -> (arg => watchdog_timeout = Value.Seconds.parse(arg)),
"X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
"a" -> (_ => all_sessions = true),
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
@@ -237,7 +242,7 @@
val sessions = getopts(args)
- val progress = new Console_Progress(verbose = verbose)
+ val progress = new Console_Progress()
{
override def theory_percentage(session: String, theory: String, percentage: Int)
{
@@ -250,11 +255,11 @@
dump(options, logic,
aspects = aspects,
progress = progress,
- log = new File_Logger(Path.explode("$ISABELLE_HOME_USER/dump.log")),
dirs = dirs,
select_dirs = select_dirs,
output_dir = output_dir,
commit_clean_delay = commit_clean_delay,
+ watchdog_timeout = watchdog_timeout,
verbose = verbose,
selection = Sessions.Selection(
requirements = requirements,
--- a/src/Pure/Tools/server_commands.scala Sat Sep 08 08:09:07 2018 +0000
+++ b/src/Pure/Tools/server_commands.scala Sat Sep 08 16:55:38 2018 +0200
@@ -158,10 +158,10 @@
pretty_margin: Double = Pretty.default_margin,
unicode_symbols: Boolean = false,
export_pattern: String = "",
- check_delay: Double = Thy_Resources.default_check_delay,
+ check_delay: Time = Thy_Resources.default_check_delay,
check_limit: Int = 0,
- watchdog_timeout: Double = 0.0,
- nodes_status_delay: Double = Thy_Resources.default_nodes_status_delay)
+ watchdog_timeout: Time = Thy_Resources.default_watchdog_timeout,
+ nodes_status_delay: Time = Thy_Resources.default_nodes_status_delay)
def unapply(json: JSON.T): Option[Args] =
for {
@@ -171,11 +171,12 @@
pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin)
unicode_symbols <- JSON.bool_default(json, "unicode_symbols")
export_pattern <- JSON.string_default(json, "export_pattern")
- check_delay <- JSON.double_default(json, "check_delay", Thy_Resources.default_check_delay)
+ check_delay <- JSON.seconds_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")
+ watchdog_timeout <-
+ JSON.seconds_default(json, "watchdog_timeout", Thy_Resources.default_watchdog_timeout)
nodes_status_delay <-
- JSON.double_default(json, "nodes_status_delay", Thy_Resources.default_nodes_status_delay)
+ JSON.seconds_default(json, "nodes_status_delay", Thy_Resources.default_nodes_status_delay)
}
yield {
Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin,
@@ -191,9 +192,9 @@
{
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),
+ check_delay = args.check_delay, check_limit = args.check_limit,
+ watchdog_timeout = args.watchdog_timeout,
+ nodes_status_delay = args.nodes_status_delay,
id = id, progress = progress)
def output_text(s: String): String =