--- a/src/Pure/Tools/server_commands.scala Fri Jul 27 17:32:16 2018 +0200
+++ b/src/Pure/Tools/server_commands.scala Fri Jul 27 22:09:27 2018 +0200
@@ -157,7 +157,9 @@
master_dir: String = "",
pretty_margin: Double = Pretty.default_margin,
unicode_symbols: Boolean = false,
- export_pattern: String = "")
+ export_pattern: String = "",
+ check_delay: Double = Thy_Resources.default_use_theories_check_delay,
+ check_limit: Int = 0)
def unapply(json: JSON.T): Option[Args] =
for {
@@ -167,10 +169,14 @@
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_use_theories_check_delay)
+ check_limit <- JSON.int_default(json, "check_limit")
}
yield {
Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin,
- unicode_symbols = unicode_symbols, export_pattern = export_pattern)
+ unicode_symbols = unicode_symbols, export_pattern = export_pattern,
+ check_delay = check_delay, check_limit = check_limit)
}
def command(args: Args,
@@ -180,6 +186,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,
id = id, progress = progress)
def output_text(s: String): String =