--- a/etc/options Wed Dec 26 20:57:23 2018 +0100
+++ b/etc/options Thu Dec 27 16:56:53 2018 +0100
@@ -144,7 +144,7 @@
-- "ML process command prefix (process policy)"
-section "Editor Reactivity"
+section "Editor Session"
public option editor_load_delay : real = 0.5
-- "delay for file load operations (new buffers etc.)"
@@ -195,6 +195,24 @@
-- "dynamic presentation while editing"
+section "Headless Session"
+
+option headless_check_delay : real = 0.5
+ -- "delay for theory status check during PIDE processing (seconds)"
+
+option headless_check_limit : int = 0
+ -- "maximum number of theory status checks (0 = unlimited)"
+
+option headless_nodes_status_delay : real = -1
+ -- "delay for overall nodes status check during PIDE processing (seconds, disabled for < 0)"
+
+option headless_watchdog_timeout : real = 600
+ -- "watchdog timeout for PIDE processing of broken theories (seconds, 0 = disabled)"
+
+option headless_commit_cleanup_delay : real = 60
+ -- "delay for cleanup of already imported theories (seconds, 0 = disabled)"
+
+
section "Miscellaneous Tools"
public option find_theorems_limit : int = 40
--- a/src/Pure/PIDE/headless.scala Wed Dec 26 20:57:23 2018 +0100
+++ b/src/Pure/PIDE/headless.scala Thu Dec 27 16:56:53 2018 +0100
@@ -84,18 +84,21 @@
(nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok })
}
- val default_check_delay = Time.seconds(0.5)
- val default_nodes_status_delay = Time.seconds(-1.0)
- val default_commit_cleanup_delay = Time.seconds(60.0)
- val default_watchdog_timeout = Time.seconds(600.0)
+ class Session private[Headless](
+ session_name: String,
+ _session_options: => Options,
+ override val resources: Resources) extends isabelle.Session(_session_options, resources)
+ {
+ session =>
- class Session private[Headless](
- session_name: String,
- session_options: Options,
- override val resources: Resources) extends isabelle.Session(session_options, resources)
- {
- session =>
+ /* options */
+
+ def default_check_delay: Time = session_options.seconds("headless_check_delay")
+ def default_check_limit: Int = session_options.int("headless_check_limit")
+ def default_nodes_status_delay: Time = session_options.seconds("headless_nodes_status_delay")
+ def default_watchdog_timeout: Time = session_options.seconds("headless_watchdog_timeout")
+ def default_commit_cleanup_delay: Time = session_options.seconds("headless_commit_cleanup_delay")
/* temporary directory */
@@ -190,7 +193,7 @@
qualifier: String = Sessions.DRAFT,
master_dir: String = "",
check_delay: Time = default_check_delay,
- check_limit: Int = 0,
+ check_limit: Int = default_check_limit,
watchdog_timeout: Time = default_watchdog_timeout,
nodes_status_delay: Time = default_nodes_status_delay,
id: UUID.T = UUID.random(),
--- a/src/Pure/Tools/dump.scala Wed Dec 26 20:57:23 2018 +0100
+++ b/src/Pure/Tools/dump.scala Thu Dec 27 16:56:53 2018 +0100
@@ -94,8 +94,6 @@
select_dirs: List[Path] = Nil,
output_dir: Path = default_output_dir,
verbose: Boolean = false,
- commit_cleanup_delay: Time = Headless.default_commit_cleanup_delay,
- watchdog_timeout: Time = Headless.default_watchdog_timeout,
system_mode: Boolean = false,
selection: Sessions.Selection = Sessions.Selection.empty): Boolean =
{
@@ -163,11 +161,7 @@
include_sessions = include_sessions, progress = progress, log = log)
val use_theories_result =
- session.use_theories(use_theories,
- progress = progress,
- commit = Some(Consumer.apply _),
- commit_cleanup_delay = commit_cleanup_delay,
- watchdog_timeout = watchdog_timeout)
+ session.use_theories(use_theories, progress = progress, commit = Some(Consumer.apply _))
session.stop()
@@ -189,11 +183,9 @@
{
var aspects: List[Aspect] = known_aspects
var base_sessions: List[String] = Nil
- var commit_cleanup_delay = Headless.default_commit_cleanup_delay
var select_dirs: List[Path] = Nil
var output_dir = default_output_dir
var requirements = false
- var watchdog_timeout = Headless.default_watchdog_timeout
var exclude_session_groups: List[String] = Nil
var all_sessions = false
var dirs: List[Path] = Nil
@@ -210,13 +202,9 @@
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 (0 = disabled, default: """ +
- Value.Seconds(Headless.default_commit_cleanup_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(Headless.default_watchdog_timeout) + """)
-X NAME exclude sessions from group NAME and all descendants
-a select all sessions
-d DIR include session directory
@@ -232,11 +220,9 @@
""" + 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_cleanup_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))),
@@ -259,8 +245,6 @@
dirs = dirs,
select_dirs = select_dirs,
output_dir = output_dir,
- commit_cleanup_delay = commit_cleanup_delay,
- watchdog_timeout = watchdog_timeout,
verbose = verbose,
selection = Sessions.Selection(
requirements = requirements,
--- a/src/Pure/Tools/server_commands.scala Wed Dec 26 20:57:23 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala Thu Dec 27 16:56:53 2018 +0100
@@ -158,10 +158,11 @@
pretty_margin: Double = Pretty.default_margin,
unicode_symbols: Boolean = false,
export_pattern: String = "",
- check_delay: Time = Headless.default_check_delay,
- check_limit: Int = 0,
- watchdog_timeout: Time = Headless.default_watchdog_timeout,
- nodes_status_delay: Time = Headless.default_nodes_status_delay)
+ check_delay: Option[Time] = None,
+ check_limit: Option[Int] = None,
+ watchdog_timeout: Option[Time] = None,
+ nodes_status_delay: Option[Time] = None,
+ commit_cleanup_delay: Option[Time] = None)
def unapply(json: JSON.T): Option[Args] =
for {
@@ -171,18 +172,17 @@
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.seconds_default(json, "check_delay", Headless.default_check_delay)
- check_limit <- JSON.int_default(json, "check_limit")
- watchdog_timeout <-
- JSON.seconds_default(json, "watchdog_timeout", Headless.default_watchdog_timeout)
- nodes_status_delay <-
- JSON.seconds_default(json, "nodes_status_delay", Headless.default_nodes_status_delay)
+ check_delay = JSON.seconds(json, "check_delay")
+ check_limit = JSON.int(json, "check_limit")
+ watchdog_timeout = JSON.seconds(json, "watchdog_timeout")
+ nodes_status_delay = JSON.seconds(json, "nodes_status_delay")
+ commit_cleanup_delay = JSON.seconds(json, "commit_cleanup_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, watchdog_timeout = watchdog_timeout,
- nodes_status_delay = nodes_status_delay)
+ nodes_status_delay = nodes_status_delay, commit_cleanup_delay = commit_cleanup_delay)
}
def command(args: Args,
@@ -192,9 +192,12 @@
{
val result =
session.use_theories(args.theories, master_dir = args.master_dir,
- check_delay = args.check_delay, check_limit = args.check_limit,
- watchdog_timeout = args.watchdog_timeout,
- nodes_status_delay = args.nodes_status_delay,
+ check_delay = args.check_delay.getOrElse(session.default_check_delay),
+ check_limit = args.check_limit.getOrElse(session.default_check_limit),
+ watchdog_timeout = args.watchdog_timeout.getOrElse(session.default_watchdog_timeout),
+ nodes_status_delay = args.nodes_status_delay.getOrElse(session.default_nodes_status_delay),
+ commit_cleanup_delay =
+ args.commit_cleanup_delay.getOrElse(session.default_commit_cleanup_delay),
id = id, progress = progress)
def output_text(s: String): String =