--- a/src/Pure/Tools/build.scala Mon Sep 28 21:14:47 2020 +0200
+++ b/src/Pure/Tools/build.scala Mon Sep 28 22:22:56 2020 +0200
@@ -411,8 +411,17 @@
case errs => result0.errors(errs).error_rc
}
- if (result1.ok)
+ if (result1.ok) {
+ for (document_output <- proper_string(options.string("document_output"))) {
+ val document_output_dir = info.dir + Path.explode(document_output)
+ Isabelle_System.mkdirs(document_output_dir)
+
+ val base = deps(session_name)
+ File.write(document_output_dir + Path.explode("session.tex"),
+ base.session_theories.map(name => "\\input{" + name.theory_base_name + ".tex}\n\n").mkString)
+ }
Present.finish(progress, store.browser_info, graph_file, info, session_name)
+ }
graph_file.delete