181 Markup.LOADING_THEORY -> loading_theory) |
181 Markup.LOADING_THEORY -> loading_theory) |
182 } |
182 } |
183 |
183 |
184 |
184 |
185 /* job: running prover process */ |
185 /* job: running prover process */ |
|
186 |
|
187 private val Loading_Theory_Marker = Protocol_Message.Marker("loading_theory") |
186 |
188 |
187 private class Job(progress: Progress, |
189 private class Job(progress: Progress, |
188 name: String, |
190 name: String, |
189 val info: Sessions.Info, |
191 val info: Sessions.Info, |
190 deps: Sessions.Deps, |
192 deps: Sessions.Deps, |
289 cwd = info.dir.file, env = env, cleanup = () => args_file.delete) |
291 cwd = info.dir.file, env = env, cleanup = () => args_file.delete) |
290 } |
292 } |
291 |
293 |
292 process.result( |
294 process.result( |
293 progress_stdout = (line: String) => |
295 progress_stdout = (line: String) => |
294 Library.try_unprefix("\floading_theory = ", line) match { |
296 line match { |
295 case Some(theory) => |
297 case Loading_Theory_Marker(theory) => |
296 progress.theory(Progress.Theory(theory, session = name)) |
298 progress.theory(Progress.Theory(theory, session = name)) |
297 case None => |
299 case Markup.Export.Marker((args, path)) => |
298 for { |
300 val body = |
299 text <- Library.try_unprefix("\fexport = ", line) |
301 try { Bytes.read(path) } |
300 (args, path) <- |
302 catch { |
301 Markup.Export.dest_inline(XML.Decode.properties(YXML.parse_body(text))) |
303 case ERROR(msg) => |
302 } { |
304 error("Failed to read export " + quote(args.compound_name) + "\n" + msg) |
303 val body = |
305 } |
304 try { Bytes.read(path) } |
306 path.file.delete |
305 catch { |
307 export_consumer(name, args, body) |
306 case ERROR(msg) => |
308 case _ => |
307 error("Failed to read export " + quote(args.compound_name) + "\n" + msg) |
|
308 } |
|
309 path.file.delete |
|
310 export_consumer(name, args, body) |
|
311 } |
|
312 }, |
309 }, |
313 progress_limit = |
310 progress_limit = |
314 options.int("process_output_limit") match { |
311 options.int("process_output_limit") match { |
315 case 0 => None |
312 case 0 => None |
316 case m => Some(m * 1000000L) |
313 case m => Some(m * 1000000L) |
538 case Some((name, (input_heaps, job))) => |
535 case Some((name, (input_heaps, job))) => |
539 //{{{ finish job |
536 //{{{ finish job |
540 |
537 |
541 val (process_result, heap_digest) = job.join |
538 val (process_result, heap_digest) = job.join |
542 |
539 |
543 val log_lines = process_result.out_lines.filterNot(_.startsWith("\f")) |
540 val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test) |
544 val process_result_tail = |
541 val process_result_tail = |
545 { |
542 { |
546 val tail = job.info.options.int("process_output_tail") |
543 val tail = job.info.options.int("process_output_tail") |
547 process_result.copy( |
544 process_result.copy( |
548 out_lines = |
545 out_lines = |