--- 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}
--- 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}
--- 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}
--- 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}
--- 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}
--- 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}
--- 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}
--- 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}
--- 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
--- 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}
--- 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}
--- 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}
--- 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}
--- 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}
--- 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;
--- 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,
--- 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