src/Pure/Tools/server_commands.scala

       theories: List[String],
       master_dir: String = "",
       pretty_margin: Double = Pretty.default_margin,
       unicode_symbols: Boolean = false,
       export_pattern: String = "",
-      check_delay: Double = Thy_Resources.default_use_theories_check_delay,
-      check_limit: Int = 0)
+      check_delay: Double = Thy_Resources.default_check_delay,
+      check_limit: Int = 0,
+      nodes_status_delay: Double = Thy_Resources.default_nodes_status_delay)
 
     def unapply(json: JSON.T): Option[Args] =
       for {
         session_id <- JSON.uuid(json, "session_id")
         theories <- JSON.strings(json, "theories")
         master_dir <- JSON.string_default(json, "master_dir")
         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_delay <- JSON.double_default(json, "check_delay", Thy_Resources.default_check_delay)
         check_limit <- JSON.int_default(json, "check_limit")
+        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,
+          nodes_status_delay = nodes_status_delay)
       }
 
     def command(args: Args,
       session: Thy_Resources.Session,
       id: UUID = UUID(),
       progress: Progress = No_Progress): (JSON.Object.T, Thy_Resources.Theories_Result) =
     {
       val result =
         session.use_theories(args.theories, master_dir = args.master_dir,
           check_delay = Time.seconds(args.check_delay), check_limit = args.check_limit,
+          nodes_status_delay = Time.seconds(args.nodes_status_delay),
           id = id, progress = progress)
 
       def output_text(s: String): String =
         if (args.unicode_symbols) Symbol.decode(s) else Symbol.encode(s)