# HG changeset patch
# User wenzelm
# Date 1617100344 -7200
# Node ID e52a9b2084813a18973a14d44894178d4a81a8b8
# Parent  2cdbb6a2f2a7ad98aacded28863e705408e499f5
support sequential LaTeX jobs: more robust when TeX installation is self-installing packages etc.;

diff -r 2cdbb6a2f2a7 -r e52a9b208481 src/Pure/Admin/build_doc.scala
--- a/src/Pure/Admin/build_doc.scala	Tue Mar 30 09:42:25 2021 +0200
+++ b/src/Pure/Admin/build_doc.scala	Tue Mar 30 12:32:24 2021 +0200
@@ -16,6 +16,7 @@
     progress: Progress = new Progress,
     all_docs: Boolean = false,
     max_jobs: Int = 1,
+    sequential: Boolean = false,
     docs: List[String] = Nil): Unit =
   {
     val store = Sessions.store(options)
@@ -63,7 +64,7 @@
               val sep = if (msg.contains('\n')) "\n" else " "
               Some("Documentation " + quote(doc) + " failed:" + sep + msg)
           }
-      }, selected).flatten
+      }, selected, sequential = sequential).flatten
 
     if (errs.nonEmpty) error(cat_lines(errs))
   }
@@ -76,6 +77,7 @@
     {
       var all_docs = false
       var max_jobs = 1
+      var sequential = false
       var options = Options.init()
 
       val getopts =
@@ -86,13 +88,15 @@
     -a           select all documentation sessions
     -j INT       maximum number of parallel jobs (default 1)
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
+    -s           sequential LaTeX jobs
 
   Build Isabelle documentation from documentation sessions with
   suitable document_variants entry.
 """,
           "a" -> (_ => all_docs = true),
           "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
-          "o:" -> (arg => options = options + arg))
+          "o:" -> (arg => options = options + arg),
+          "s" -> (_ => sequential = true))
 
       val docs = getopts(args)
 
@@ -101,7 +105,8 @@
       val progress = new Console_Progress()
 
       progress.interrupt_handler {
-        build_doc(options, progress, all_docs, max_jobs, docs)
+        build_doc(options, progress = progress, all_docs = all_docs, max_jobs = max_jobs,
+          sequential = sequential, docs = docs)
       }
     })
 }
diff -r 2cdbb6a2f2a7 -r e52a9b208481 src/Pure/Concurrent/par_list.scala
--- a/src/Pure/Concurrent/par_list.scala	Tue Mar 30 09:42:25 2021 +0200
+++ b/src/Pure/Concurrent/par_list.scala	Tue Mar 30 12:32:24 2021 +0200
@@ -10,8 +10,10 @@
 
 object Par_List
 {
-  def managed_results[A, B](f: A => B, xs: List[A]): List[Exn.Result[B]] =
-    if (xs.isEmpty || xs.tail.isEmpty) xs.map(x => Exn.capture { f(x) })
+  def managed_results[A, B](f: A => B, xs: List[A], sequential: Boolean = false)
+      : List[Exn.Result[B]] =
+  {
+    if (sequential || xs.isEmpty || xs.tail.isEmpty) xs.map(x => Exn.capture { f(x) })
     else {
       val state = Synchronized[(List[Future[B]], Boolean)]((Nil, false))
 
@@ -39,9 +41,10 @@
       }
       finally { cancel_other() }
     }
+  }
 
-  def map[A, B](f: A => B, xs: List[A]): List[B] =
-    Exn.release_first(managed_results(f, xs))
+  def map[A, B](f: A => B, xs: List[A], sequential: Boolean = false): List[B] =
+    Exn.release_first(managed_results(f, xs, sequential = sequential))
 
   def get_some[A, B](f: A => Option[B], xs: List[A]): Option[B] =
   {