--- a/etc/options Sat Nov 21 16:22:35 2020 +0100
+++ b/etc/options Sat Nov 21 17:12:17 2020 +0100
@@ -9,8 +9,6 @@
-- "build document in given format: pdf, dvi, false"
option document_output : string = ""
-- "document output directory"
-option document_output_sources : bool = true
- -- "copy generated sources into document output directory"
option document_variants : string = "document"
-- "alternative document variants (separated by colons)"
option document_tags : string = ""
--- a/src/Doc/System/Presentation.thy Sat Nov 21 16:22:35 2020 +0100
+++ b/src/Doc/System/Presentation.thy Sat Nov 21 17:12:17 2020 +0100
@@ -129,7 +129,9 @@
\<open>Usage: isabelle document [OPTIONS] SESSION
Options are:
- -O set option "document_output", relative to current directory
+ -O DIR output directory for LaTeX sources and resulting PDF
+ -P DIR output directory for resulting PDF
+ -S DIR output directory for LaTeX sources
-V verbose latex
-d DIR include session directory
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
@@ -148,9 +150,9 @@
\<^medskip> Option \<^verbatim>\<open>-V\<close> prints full output of {\LaTeX} tools.
- \<^medskip> Option \<^verbatim>\<open>-O\<close>~\<open>dir\<close> specifies the @{system_option document_output} option
- relative to the current directory, while \<^verbatim>\<open>-o document_output=\<close>\<open>dir\<close> is
- relative to the session directory.
+ \<^medskip> Option \<^verbatim>\<open>-O\<close>~\<open>dir\<close> specifies the output directory for generated {\LaTeX}
+ sources and the result PDF file. Options \<^verbatim>\<open>-P\<close> and \<^verbatim>\<open>-S\<close> only refer to the
+ PDF and sources, respectively.
For example, for output directory ``\<^verbatim>\<open>output\<close>'' and the default document
variant ``\<^verbatim>\<open>document\<close>'', the generated document sources are placed into the
--- a/src/Pure/Admin/build_doc.scala Sat Nov 21 16:22:35 2020 +0100
+++ b/src/Pure/Admin/build_doc.scala Sat Nov 21 17:12:17 2020 +0100
@@ -43,21 +43,25 @@
error("Build failed")
progress.echo("Build started for documentation " + commas_quote(documents))
- val doc_options =
- options + "document=pdf" + "document_output=~~/doc" + "document_output_sources=false"
+ val doc_options = options + "document=pdf"
val deps = Sessions.load_structure(doc_options).selection_deps(selection)
val errs =
- Par_List.map((doc_session: (String, String)) =>
- try {
- Presentation.build_documents(doc_session._2, deps, store, progress = progress)
- None
- }
- catch {
- case Exn.Interrupt.ERROR(msg) =>
- val sep = if (msg.contains('\n')) "\n" else " "
- Some("Documentation " + doc_session._1 + " failed:" + sep + msg)
- }, selected).flatten
+ Par_List.map[(String, String), Option[String]](
+ {
+ case (doc, session) =>
+ try {
+ progress.echo("Documentation " + doc + " ...")
+ Presentation.build_documents(session, deps, store,
+ output_pdf = Some(Path.explode("~~/src/doc")))
+ None
+ }
+ catch {
+ case Exn.Interrupt.ERROR(msg) =>
+ val sep = if (msg.contains('\n')) "\n" else " "
+ Some("Documentation " + doc + " failed:" + sep + msg)
+ }
+ }, selected).flatten
if (errs.nonEmpty) error(cat_lines(errs))
}
--- a/src/Pure/Thy/presentation.scala Sat Nov 21 16:22:35 2020 +0100
+++ b/src/Pure/Thy/presentation.scala Sat Nov 21 17:12:17 2020 +0100
@@ -439,6 +439,8 @@
deps: Sessions.Deps,
store: Sessions.Store,
progress: Progress = new Progress,
+ output_sources: Option[Path] = None,
+ output_pdf: Option[Path] = None,
verbose: Boolean = false,
verbose_latex: Boolean = false): List[(Document_Variant, Bytes)] =
{
@@ -493,8 +495,6 @@
/* produce documents */
- val doc_output = info.document_output
-
val documents =
for (doc <- info.documents)
yield {
@@ -511,8 +511,10 @@
val sources = SHA1.digest_set(digests).toString
prepare_dir2(tmp_dir, doc)
- doc_output.foreach(prepare_dir1(_, doc))
- doc_output.foreach(prepare_dir2(_, doc))
+ for (dir <- output_sources) {
+ prepare_dir1(dir, doc)
+ prepare_dir2(dir, doc)
+ }
// old document from database
@@ -583,7 +585,8 @@
})
}
- for (dir <- doc_output; (doc, pdf) <- documents) {
+ for (dir <- output_pdf; (doc, pdf) <- documents) {
+ Isabelle_System.make_directory(dir)
val path = dir + doc.path.pdf
Bytes.write(path, pdf)
progress.echo_document("Document at " + path.absolute)
@@ -598,6 +601,8 @@
val isabelle_tool =
Isabelle_Tool("document", "prepare session theory document", args =>
{
+ var output_sources: Option[Path] = None
+ var output_pdf: Option[Path] = None
var verbose_latex = false
var dirs: List[Path] = Nil
var options = Options.init()
@@ -608,7 +613,9 @@
Usage: isabelle document [OPTIONS] SESSION
Options are:
- -O set option "document_output", relative to current directory
+ -O DIR output directory for LaTeX sources and resulting PDF
+ -P DIR output directory for resulting PDF
+ -S DIR output directory for LaTeX sources
-V verbose latex
-d DIR include session directory
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
@@ -616,7 +623,14 @@
Prepare the theory document of a session.
""",
- "O:" -> (arg => options += ("document_output=" + Path.explode(arg).absolute.implode)),
+ "O:" -> (arg =>
+ {
+ val dir = Path.explode(arg)
+ output_sources = Some(dir)
+ output_pdf = Some(dir)
+ }),
+ "P:" -> (arg => { output_pdf = Some(Path.explode(arg)) }),
+ "S:" -> (arg => { output_sources = Some(Path.explode(arg)) }),
"V" -> (_ => verbose_latex = true),
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
"o:" -> (arg => options = options + arg),
@@ -642,11 +656,12 @@
Sessions.load_structure(options + "document=pdf", dirs = dirs).
selection_deps(Sessions.Selection.session(session))
- if (deps.sessions_structure(session).document_output.isEmpty) {
- progress.echo_warning("No document_output")
+ if (output_sources.isEmpty && output_pdf.isEmpty) {
+ progress.echo_warning("No output directory")
}
build_documents(session, deps, store, progress = progress,
+ output_sources = output_sources, output_pdf = output_pdf,
verbose = true, verbose_latex = verbose_latex)
}
})
--- a/src/Pure/Tools/build_job.scala Sat Nov 21 16:22:35 2020 +0100
+++ b/src/Pure/Tools/build_job.scala Sat Nov 21 17:12:17 2020 +0100
@@ -217,7 +217,8 @@
val document_errors =
try {
- if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty) {
+ if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty)
+ {
val document_progress =
new Progress {
override def echo(msg: String): Unit =
@@ -226,8 +227,12 @@
progress.echo_document(msg)
}
val documents =
- Presentation.build_documents(session_name, deps, store, verbose = verbose,
- verbose_latex = true, progress = document_progress)
+ Presentation.build_documents(session_name, deps, store,
+ output_sources = info.document_output,
+ output_pdf = info.document_output,
+ progress = document_progress,
+ verbose = verbose,
+ verbose_latex = true)
using(store.open_database(session_name, output = true))(db =>
for ((doc, pdf) <- documents) {
db.transaction {