clarified build_doc, based on Present.build_documents;

--- a/etc/options	Wed Nov 11 21:09:56 2020 +0100
+++ b/etc/options	Wed Nov 11 22:20:57 2020 +0100
@@ -8,7 +8,9 @@
 option document : string = ""
   -- "build document in given format: pdf, dvi, false"
 option document_output : string = ""
-  -- "document output directory (default within $ISABELLE_BROWSER_INFO tree)"
+  -- "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/Pure/Admin/build_doc.scala	Wed Nov 11 21:09:56 2020 +0100
+++ b/src/Pure/Admin/build_doc.scala	Wed Nov 11 22:20:57 2020 +0100
@@ -19,53 +19,39 @@
     progress: Progress = new Progress,
     all_docs: Boolean = false,
     max_jobs: Int = 1,
-    docs: List[String] = Nil): Int =
+    docs: List[String] = Nil)
   {
+    val store = Sessions.store(options)
+
     val sessions_structure = Sessions.load_structure(options)
-    val selection =
+    val selected =
       for {
-        name <- sessions_structure.build_topological_order
-        info = sessions_structure(name)
+        session <- sessions_structure.build_topological_order
+        info = sessions_structure(session)
         if info.groups.contains("doc")
         doc = info.options.string("document_variants")
         if all_docs || docs.contains(doc)
-      } yield (doc, name)
+      } yield (doc, session)
 
-    val selected_docs = selection.map(_._1)
-    val sessions = selection.map(_._2)
+    val documents = selected.map(_._1)
+    val selection = Sessions.Selection(sessions = selected.map(_._2))
 
-    docs.filter(doc => !selected_docs.contains(doc)) match {
+    docs.filter(doc => !documents.contains(doc)) match {
       case Nil =>
       case bad => error("No documentation session for " + commas_quote(bad))
     }
 
-    progress.echo("Build started for documentation " + commas_quote(selected_docs))
+    progress.echo("Build started for sessions " + commas_quote(selection.sessions))
+    Build.build(options, selection = selection, progress = progress, max_jobs = max_jobs).ok ||
+      error("Build failed")
 
-    val res1 =
-      Build.build(options,
-        selection = Sessions.Selection(requirements = true, sessions = sessions),
-        progress = progress, build_heap = true, max_jobs = max_jobs)
-    if (res1.ok) {
-      Isabelle_System.with_tmp_dir("document_output")(output =>
-        {
-          val res2 =
-            Build.build(
-              options.bool.update("browser_info", false).
-                string.update("document", "pdf").
-                string.update("document_output", output.implode),
-              selection = Sessions.Selection(sessions = sessions),
-              progress = progress, clean_build = true, max_jobs = max_jobs)
-          if (res2.ok) {
-            val doc_dir = Path.explode("~~/doc")
-            for (doc <- selected_docs) {
-              val name = Path.explode(doc + ".pdf")
-              File.copy(output + name, doc_dir + name)
-            }
-          }
-          res2.rc
-        })
+    progress.echo("Build started for documentation " + commas_quote(documents))
+    val doc_options =
+      options + "document=pdf" + "document_output=~~/doc" + "document_output_sources=false"
+    val deps = Sessions.load_structure(doc_options).selection_deps(selection)
+    for (session <- selection.sessions) {
+      Present.build_documents(session, deps, store, progress = progress)
     }
-    else res1.rc
   }
 
 
@@ -99,10 +85,9 @@
       if (!all_docs && docs.isEmpty) getopts.usage()
 
       val progress = new Console_Progress()
-      val rc =
-        progress.interrupt_handler {
-          build_doc(options, progress, all_docs, max_jobs, docs)
-        }
-      sys.exit(rc)
+
+      progress.interrupt_handler {
+        build_doc(options, progress, all_docs, max_jobs, docs)
+      }
     })
 }