156 theories: List[String], |
156 theories: List[String], |
157 master_dir: String = "", |
157 master_dir: String = "", |
158 pretty_margin: Double = Pretty.default_margin, |
158 pretty_margin: Double = Pretty.default_margin, |
159 unicode_symbols: Boolean = false, |
159 unicode_symbols: Boolean = false, |
160 export_pattern: String = "", |
160 export_pattern: String = "", |
161 check_delay: Time = Headless.default_check_delay, |
161 check_delay: Option[Time] = None, |
162 check_limit: Int = 0, |
162 check_limit: Option[Int] = None, |
163 watchdog_timeout: Time = Headless.default_watchdog_timeout, |
163 watchdog_timeout: Option[Time] = None, |
164 nodes_status_delay: Time = Headless.default_nodes_status_delay) |
164 nodes_status_delay: Option[Time] = None, |
|
165 commit_cleanup_delay: Option[Time] = None) |
165 |
166 |
166 def unapply(json: JSON.T): Option[Args] = |
167 def unapply(json: JSON.T): Option[Args] = |
167 for { |
168 for { |
168 session_id <- JSON.uuid(json, "session_id") |
169 session_id <- JSON.uuid(json, "session_id") |
169 theories <- JSON.strings(json, "theories") |
170 theories <- JSON.strings(json, "theories") |
170 master_dir <- JSON.string_default(json, "master_dir") |
171 master_dir <- JSON.string_default(json, "master_dir") |
171 pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin) |
172 pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin) |
172 unicode_symbols <- JSON.bool_default(json, "unicode_symbols") |
173 unicode_symbols <- JSON.bool_default(json, "unicode_symbols") |
173 export_pattern <- JSON.string_default(json, "export_pattern") |
174 export_pattern <- JSON.string_default(json, "export_pattern") |
174 check_delay <- JSON.seconds_default(json, "check_delay", Headless.default_check_delay) |
175 check_delay = JSON.seconds(json, "check_delay") |
175 check_limit <- JSON.int_default(json, "check_limit") |
176 check_limit = JSON.int(json, "check_limit") |
176 watchdog_timeout <- |
177 watchdog_timeout = JSON.seconds(json, "watchdog_timeout") |
177 JSON.seconds_default(json, "watchdog_timeout", Headless.default_watchdog_timeout) |
178 nodes_status_delay = JSON.seconds(json, "nodes_status_delay") |
178 nodes_status_delay <- |
179 commit_cleanup_delay = JSON.seconds(json, "commit_cleanup_delay") |
179 JSON.seconds_default(json, "nodes_status_delay", Headless.default_nodes_status_delay) |
|
180 } |
180 } |
181 yield { |
181 yield { |
182 Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin, |
182 Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin, |
183 unicode_symbols = unicode_symbols, export_pattern = export_pattern, |
183 unicode_symbols = unicode_symbols, export_pattern = export_pattern, |
184 check_delay = check_delay, check_limit = check_limit, watchdog_timeout = watchdog_timeout, |
184 check_delay = check_delay, check_limit = check_limit, watchdog_timeout = watchdog_timeout, |
185 nodes_status_delay = nodes_status_delay) |
185 nodes_status_delay = nodes_status_delay, commit_cleanup_delay = commit_cleanup_delay) |
186 } |
186 } |
187 |
187 |
188 def command(args: Args, |
188 def command(args: Args, |
189 session: Headless.Session, |
189 session: Headless.Session, |
190 id: UUID.T = UUID.random(), |
190 id: UUID.T = UUID.random(), |
191 progress: Progress = No_Progress): (JSON.Object.T, Headless.Use_Theories_Result) = |
191 progress: Progress = No_Progress): (JSON.Object.T, Headless.Use_Theories_Result) = |
192 { |
192 { |
193 val result = |
193 val result = |
194 session.use_theories(args.theories, master_dir = args.master_dir, |
194 session.use_theories(args.theories, master_dir = args.master_dir, |
195 check_delay = args.check_delay, check_limit = args.check_limit, |
195 check_delay = args.check_delay.getOrElse(session.default_check_delay), |
196 watchdog_timeout = args.watchdog_timeout, |
196 check_limit = args.check_limit.getOrElse(session.default_check_limit), |
197 nodes_status_delay = args.nodes_status_delay, |
197 watchdog_timeout = args.watchdog_timeout.getOrElse(session.default_watchdog_timeout), |
|
198 nodes_status_delay = args.nodes_status_delay.getOrElse(session.default_nodes_status_delay), |
|
199 commit_cleanup_delay = |
|
200 args.commit_cleanup_delay.getOrElse(session.default_commit_cleanup_delay), |
198 id = id, progress = progress) |
201 id = id, progress = progress) |
199 |
202 |
200 def output_text(s: String): String = |
203 def output_text(s: String): String = |
201 if (args.unicode_symbols) Symbol.decode(s) else Symbol.encode(s) |
204 if (args.unicode_symbols) Symbol.decode(s) else Symbol.encode(s) |
202 |
205 |