# HG changeset patch
# User wenzelm
# Date 1601324576 -7200
# Node ID e36f94e2eb6bb32308a436bf31c6c516fe99d41f
# Parent  9bb16dcb9ed8bbfae6eac4c911b3346d6ddc96f6
some support for document preparation in Isabelle/Scala;

diff -r 9bb16dcb9ed8 -r e36f94e2eb6b src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Sep 28 21:14:47 2020 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Sep 28 22:22:56 2020 +0200
@@ -52,6 +52,7 @@
     doc_names: List[String] = Nil,
     session_directories: Map[JFile, String] = Map.empty,
     global_theories: Map[String, String] = Map.empty,
+    session_theories: List[Document.Node.Name] = Nil,
     loaded_theories: Graph[String, Outer_Syntax] = Graph.string,
     used_theories: List[(Document.Node.Name, Options)] = Nil,
     known_theories: Map[String, Document.Node.Entry] = Map.empty,
@@ -165,6 +166,12 @@
 
             val overall_syntax = dependencies.overall_syntax
 
+            val session_theories =
+              for {
+                name <- dependencies.theories
+                if deps_base.theory_qualifier(name) == info.name
+              } yield name
+
             val theory_files = dependencies.theories.map(_.path)
 
             val (loaded_files, loaded_files_errors) =
@@ -295,6 +302,7 @@
                 doc_names = doc_names,
                 session_directories = sessions_structure.session_directories,
                 global_theories = sessions_structure.global_theories,
+                session_theories = session_theories,
                 loaded_theories = dependencies.loaded_theories,
                 used_theories = dependencies.theories_adjunct,
                 known_theories = known_theories,
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