equal
deleted
inserted
replaced
409 export_consumer.shutdown(close = true).map(Output.error_message_text) match { |
409 export_consumer.shutdown(close = true).map(Output.error_message_text) match { |
410 case Nil => result0 |
410 case Nil => result0 |
411 case errs => result0.errors(errs).error_rc |
411 case errs => result0.errors(errs).error_rc |
412 } |
412 } |
413 |
413 |
414 if (result1.ok) |
414 if (result1.ok) { |
|
415 for (document_output <- proper_string(options.string("document_output"))) { |
|
416 val document_output_dir = info.dir + Path.explode(document_output) |
|
417 Isabelle_System.mkdirs(document_output_dir) |
|
418 |
|
419 val base = deps(session_name) |
|
420 File.write(document_output_dir + Path.explode("session.tex"), |
|
421 base.session_theories.map(name => "\\input{" + name.theory_base_name + ".tex}\n\n").mkString) |
|
422 } |
415 Present.finish(progress, store.browser_info, graph_file, info, session_name) |
423 Present.finish(progress, store.browser_info, graph_file, info, session_name) |
|
424 } |
416 |
425 |
417 graph_file.delete |
426 graph_file.delete |
418 |
427 |
419 val was_timeout = |
428 val was_timeout = |
420 timeout_request match { |
429 timeout_request match { |