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: Double = Thy_Resources.default_check_delay, |
161 check_delay: Double = Thy_Resources.default_check_delay, |
162 check_limit: Int = 0, |
162 check_limit: Int = 0, |
|
163 watchdog_timeout: Double = 0.0, |
163 nodes_status_delay: Double = Thy_Resources.default_nodes_status_delay) |
164 nodes_status_delay: Double = Thy_Resources.default_nodes_status_delay) |
164 |
165 |
165 def unapply(json: JSON.T): Option[Args] = |
166 def unapply(json: JSON.T): Option[Args] = |
166 for { |
167 for { |
167 session_id <- JSON.uuid(json, "session_id") |
168 session_id <- JSON.uuid(json, "session_id") |
170 pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin) |
171 pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin) |
171 unicode_symbols <- JSON.bool_default(json, "unicode_symbols") |
172 unicode_symbols <- JSON.bool_default(json, "unicode_symbols") |
172 export_pattern <- JSON.string_default(json, "export_pattern") |
173 export_pattern <- JSON.string_default(json, "export_pattern") |
173 check_delay <- JSON.double_default(json, "check_delay", Thy_Resources.default_check_delay) |
174 check_delay <- JSON.double_default(json, "check_delay", Thy_Resources.default_check_delay) |
174 check_limit <- JSON.int_default(json, "check_limit") |
175 check_limit <- JSON.int_default(json, "check_limit") |
|
176 watchdog_timeout <- JSON.double_default(json, "watchdog_timeout") |
175 nodes_status_delay <- |
177 nodes_status_delay <- |
176 JSON.double_default(json, "nodes_status_delay", Thy_Resources.default_nodes_status_delay) |
178 JSON.double_default(json, "nodes_status_delay", Thy_Resources.default_nodes_status_delay) |
177 } |
179 } |
178 yield { |
180 yield { |
179 Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin, |
181 Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin, |
180 unicode_symbols = unicode_symbols, export_pattern = export_pattern, |
182 unicode_symbols = unicode_symbols, export_pattern = export_pattern, |
181 check_delay = check_delay, check_limit = check_limit, |
183 check_delay = check_delay, check_limit = check_limit, watchdog_timeout = watchdog_timeout, |
182 nodes_status_delay = nodes_status_delay) |
184 nodes_status_delay = nodes_status_delay) |
183 } |
185 } |
184 |
186 |
185 def command(args: Args, |
187 def command(args: Args, |
186 session: Thy_Resources.Session, |
188 session: Thy_Resources.Session, |
188 progress: Progress = No_Progress): (JSON.Object.T, Thy_Resources.Theories_Result) = |
190 progress: Progress = No_Progress): (JSON.Object.T, Thy_Resources.Theories_Result) = |
189 { |
191 { |
190 val result = |
192 val result = |
191 session.use_theories(args.theories, master_dir = args.master_dir, |
193 session.use_theories(args.theories, master_dir = args.master_dir, |
192 check_delay = Time.seconds(args.check_delay), check_limit = args.check_limit, |
194 check_delay = Time.seconds(args.check_delay), check_limit = args.check_limit, |
|
195 watchdog_timeout = Time.seconds(args.watchdog_timeout), |
193 nodes_status_delay = Time.seconds(args.nodes_status_delay), |
196 nodes_status_delay = Time.seconds(args.nodes_status_delay), |
194 id = id, progress = progress) |
197 id = id, progress = progress) |
195 |
198 |
196 def output_text(s: String): String = |
199 def output_text(s: String): String = |
197 if (args.unicode_symbols) Symbol.decode(s) else Symbol.encode(s) |
200 if (args.unicode_symbols) Symbol.decode(s) else Symbol.encode(s) |