src/Pure/Thy/present.scala

--- a/src/Pure/Thy/present.scala	Sun Nov 08 16:20:39 2020 +0100
+++ b/src/Pure/Thy/present.scala	Sun Nov 08 21:27:08 2020 +0100
@@ -193,6 +193,17 @@
 
 
 
+  /** make document source **/
+
+  def write_tex_index(dir: Path, names: List[Document.Node.Name])
+  {
+    val path = dir + Path.explode("session.tex")
+    val text = names.map(name => "\\input{" + name.theory_base_name + ".tex}\n\n").mkString
+    File.write(path, text)
+  }
+
+
+
   /** build document **/
 
   val document_format = "pdf"