# HG changeset patch
# User wenzelm
# Date 1605975137 -3600
# Node ID cc1347c8c80496599bb7ec8e7aed5c475e3236f5
# Parent  a9fea3f11cc033507a65ccafba5f37afdc2c26e2
clarified document output;

diff -r a9fea3f11cc0 -r cc1347c8c804 etc/options
--- 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 = ""
diff -r a9fea3f11cc0 -r cc1347c8c804 src/Doc/System/Presentation.thy
--- 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
diff -r a9fea3f11cc0 -r cc1347c8c804 src/Pure/Admin/build_doc.scala
--- 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))
   }
diff -r a9fea3f11cc0 -r cc1347c8c804 src/Pure/Thy/presentation.scala
--- 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)
       }
     })
diff -r a9fea3f11cc0 -r cc1347c8c804 src/Pure/Tools/build_job.scala
--- 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 {