diff -r 9bb16dcb9ed8 -r e36f94e2eb6b src/Pure/Tools/build.scala --- 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