# HG changeset patch
# User paulson
# Date 1601368574 -3600
# Node ID 4750ea34603e6ee7ff14d48b6522c22965fdd2e0
# Parent  e36f94e2eb6bb32308a436bf31c6c516fe99d41f# Parent  fb6295a224f835aa13d63a0acc6b72f44d3ee4fe
merged

diff -r fb6295a224f8 -r 4750ea34603e src/Doc/Corec/document/root.tex
--- a/src/Doc/Corec/document/root.tex	Mon Sep 28 18:34:27 2020 +0100
+++ b/src/Doc/Corec/document/root.tex	Tue Sep 29 09:36:14 2020 +0100
@@ -1,5 +1,4 @@
 \documentclass[12pt,a4paper]{article} % fleqn
-\usepackage{lmodern}
 \usepackage[T1]{fontenc}
 \usepackage{amsfonts}
 \usepackage{amsmath}
diff -r fb6295a224f8 -r 4750ea34603e src/Doc/Datatypes/document/root.tex
--- a/src/Doc/Datatypes/document/root.tex	Mon Sep 28 18:34:27 2020 +0100
+++ b/src/Doc/Datatypes/document/root.tex	Tue Sep 29 09:36:14 2020 +0100
@@ -1,5 +1,4 @@
 \documentclass[12pt,a4paper]{article} % fleqn
-\usepackage{lmodern}
 \usepackage[T1]{fontenc}
 \usepackage{amsfonts}
 \usepackage{amsmath}
diff -r fb6295a224f8 -r 4750ea34603e src/Doc/Eisbach/document/root.tex
--- a/src/Doc/Eisbach/document/root.tex	Mon Sep 28 18:34:27 2020 +0100
+++ b/src/Doc/Eisbach/document/root.tex	Tue Sep 29 09:36:14 2020 +0100
@@ -1,5 +1,4 @@
 \documentclass[12pt,a4paper,fleqn]{report}
-\usepackage{lmodern}
 \usepackage[T1]{fontenc}
 \usepackage{latexsym,graphicx}
 \usepackage[refpage]{nomencl}
diff -r fb6295a224f8 -r 4750ea34603e src/Doc/How_to_Prove_it/document/prelude.tex
--- a/src/Doc/How_to_Prove_it/document/prelude.tex	Mon Sep 28 18:34:27 2020 +0100
+++ b/src/Doc/How_to_Prove_it/document/prelude.tex	Tue Sep 29 09:36:14 2020 +0100
@@ -4,7 +4,6 @@
 \usepackage{multicol}        % used for the two-column index
 \usepackage[bottom]{footmisc}% places footnotes at page bottom
 
-\usepackage{lmodern}
 \usepackage[T1]{fontenc}
 
 \usepackage{isabelle,isabellesym}
diff -r fb6295a224f8 -r 4750ea34603e src/Doc/Implementation/document/root.tex
--- a/src/Doc/Implementation/document/root.tex	Mon Sep 28 18:34:27 2020 +0100
+++ b/src/Doc/Implementation/document/root.tex	Tue Sep 29 09:36:14 2020 +0100
@@ -1,5 +1,4 @@
 \documentclass[12pt,a4paper,fleqn]{report}
-\usepackage{lmodern}
 \usepackage[T1]{fontenc}
 \usepackage{latexsym,graphicx}
 \usepackage[refpage]{nomencl}
diff -r fb6295a224f8 -r 4750ea34603e src/Doc/Isar_Ref/document/root.tex
--- a/src/Doc/Isar_Ref/document/root.tex	Mon Sep 28 18:34:27 2020 +0100
+++ b/src/Doc/Isar_Ref/document/root.tex	Tue Sep 29 09:36:14 2020 +0100
@@ -1,5 +1,4 @@
 \documentclass[12pt,a4paper,fleqn]{report}
-\usepackage{lmodern}
 \usepackage[T1]{fontenc}
 \usepackage{amsmath}
 \usepackage{amssymb}
diff -r fb6295a224f8 -r 4750ea34603e src/Doc/JEdit/document/root.tex
--- a/src/Doc/JEdit/document/root.tex	Mon Sep 28 18:34:27 2020 +0100
+++ b/src/Doc/JEdit/document/root.tex	Tue Sep 29 09:36:14 2020 +0100
@@ -1,5 +1,4 @@
 \documentclass[12pt,a4paper]{report}
-\usepackage{lmodern}
 \usepackage[T1]{fontenc}
 \usepackage{supertabular}
 \usepackage{rotating}
diff -r fb6295a224f8 -r 4750ea34603e src/Doc/Locales/document/root.tex
--- a/src/Doc/Locales/document/root.tex	Mon Sep 28 18:34:27 2020 +0100
+++ b/src/Doc/Locales/document/root.tex	Tue Sep 29 09:36:14 2020 +0100
@@ -1,5 +1,4 @@
 \documentclass[11pt,a4paper]{article}
-\usepackage{lmodern}
 \usepackage[T1]{fontenc}
 \usepackage{tikz}
 \usepackage{subfigure}
diff -r fb6295a224f8 -r 4750ea34603e src/Doc/Main/document/root.tex
--- a/src/Doc/Main/document/root.tex	Mon Sep 28 18:34:27 2020 +0100
+++ b/src/Doc/Main/document/root.tex	Tue Sep 29 09:36:14 2020 +0100
@@ -1,5 +1,4 @@
 \documentclass[12pt,a4paper]{article}
-\usepackage{lmodern}
 \usepackage[T1]{fontenc}
 
 %shortens document but can cause odd page breaks
diff -r fb6295a224f8 -r 4750ea34603e src/Doc/Nitpick/document/root.tex
--- a/src/Doc/Nitpick/document/root.tex	Mon Sep 28 18:34:27 2020 +0100
+++ b/src/Doc/Nitpick/document/root.tex	Tue Sep 29 09:36:14 2020 +0100
@@ -1,5 +1,4 @@
 \documentclass[a4paper,12pt]{article}
-\usepackage{lmodern}
 \usepackage[T1]{fontenc}
 \usepackage{amsmath}
 \usepackage{amssymb}
diff -r fb6295a224f8 -r 4750ea34603e src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Mon Sep 28 18:34:27 2020 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Tue Sep 29 09:36:14 2020 +0100
@@ -1,5 +1,4 @@
 \documentclass[a4paper,12pt]{article}
-\usepackage{lmodern}
 \usepackage[T1]{fontenc}
 \usepackage{amsmath}
 \usepackage{amssymb}
diff -r fb6295a224f8 -r 4750ea34603e src/Doc/System/document/root.tex
--- a/src/Doc/System/document/root.tex	Mon Sep 28 18:34:27 2020 +0100
+++ b/src/Doc/System/document/root.tex	Tue Sep 29 09:36:14 2020 +0100
@@ -1,5 +1,4 @@
 \documentclass[12pt,a4paper]{report}
-\usepackage{lmodern}
 \usepackage[T1]{fontenc}
 \usepackage{supertabular}
 \usepackage{graphicx}
diff -r fb6295a224f8 -r 4750ea34603e src/HOL/Examples/document/root.tex
--- a/src/HOL/Examples/document/root.tex	Mon Sep 28 18:34:27 2020 +0100
+++ b/src/HOL/Examples/document/root.tex	Tue Sep 29 09:36:14 2020 +0100
@@ -1,6 +1,6 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage[utf8]{inputenc}
-\usepackage[T1]{fontenc}
 \usepackage[only,bigsqcap]{stmaryrd}
 \usepackage{ifthen,proof,amssymb,isabelle,isabellesym}
 
diff -r fb6295a224f8 -r 4750ea34603e src/Pure/Examples/document/root.tex
--- a/src/Pure/Examples/document/root.tex	Mon Sep 28 18:34:27 2020 +0100
+++ b/src/Pure/Examples/document/root.tex	Tue Sep 29 09:36:14 2020 +0100
@@ -1,6 +1,6 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage[utf8]{inputenc}
-\usepackage[T1]{fontenc}
 \usepackage{ifthen,proof,amssymb,isabelle,isabellesym}
 
 \isabellestyle{literal}
diff -r fb6295a224f8 -r 4750ea34603e src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Mon Sep 28 18:34:27 2020 +0100
+++ b/src/Pure/Thy/present.ML	Tue Sep 29 09:36:14 2020 +0100
@@ -225,8 +225,8 @@
   write_tex (index_buffer tex_index) doc_indexN path;
 
 fun finish () =
-  with_session_info () (fn {name, chapter, info, info_path, document,
-    doc_output, doc_files, graph_file, documents, verbose, readme, ...} =>
+  with_session_info () (fn {name, chapter, info, info_path, doc_output, doc_files, graph_file,
+    documents, verbose, readme, ...} =>
   let
     val {theories, tex_index, html_index} = Synchronized.value browser_info;
     val thys = Symtab.dest theories;
diff -r fb6295a224f8 -r 4750ea34603e src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Sep 28 18:34:27 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Sep 29 09:36:14 2020 +0100
@@ -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 fb6295a224f8 -r 4750ea34603e src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Sep 28 18:34:27 2020 +0100
+++ b/src/Pure/Tools/build.scala	Tue Sep 29 09:36:14 2020 +0100
@@ -169,7 +169,6 @@
     private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf")
     graphview.Graph_File.write(options, graph_file, deps(session_name).session_graph_display)
 
-    private val export_tmp_dir = Isabelle_System.tmp_dir("export")
     private val export_consumer =
       Export.consumer(store.open_database(session_name, output = true), cache = store.xz_cache)
 
@@ -201,7 +200,6 @@
 
         val env =
           Isabelle_System.settings() +
-            ("ISABELLE_EXPORT_TMP" -> File.standard_path(export_tmp_dir)) +
             ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)
 
         val is_pure = Sessions.is_pure(session_name)
@@ -413,10 +411,17 @@
           case errs => result0.errors(errs).error_rc
         }
 
-      Isabelle_System.rm_tree(export_tmp_dir)
+      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)
 
-      if (result1.ok)
+          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