diff --git a/src/Pure/Admin/build_doc.scala b/src/Pure/Admin/build_doc.scala
--- a/src/Pure/Admin/build_doc.scala
+++ b/src/Pure/Admin/build_doc.scala
@@ -1,107 +1,112 @@
 /*  Title:      Pure/Admin/build_doc.scala
     Author:     Makarius
 
 Build Isabelle documentation.
 */
 
 package isabelle
 
 
 object Build_Doc
 {
   /* build_doc */
 
   def build_doc(
     options: Options,
     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)
 
     val sessions_structure = Sessions.load_structure(options)
     val selected =
       for {
         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, session)
 
     val documents = selected.map(_._1)
     val selection = Sessions.Selection(sessions = selected.map(_._2))
 
     docs.filter(doc => !documents.contains(doc)) match {
       case Nil =>
       case bad => error("No documentation session for " + commas_quote(bad))
     }
 
     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")
 
     progress.echo("Build started for documentation " + commas_quote(documents))
     val doc_options = options + "document=pdf"
     val deps = Sessions.load_structure(doc_options).selection_deps(selection)
 
     val errs =
       Par_List.map[(String, String), Option[String]](
       {
         case (doc, session) =>
           try {
             progress.echo("Documentation " + quote(doc) + " ...")
 
             using(store.open_database_context())(db_context =>
               Presentation.build_documents(session, deps, db_context,
                 output_pdf = Some(Path.explode("~~/doc"))))
             None
           }
           catch {
             case Exn.Interrupt.ERROR(msg) =>
               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))
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
     Isabelle_Tool("build_doc", "build Isabelle documentation", Scala_Project.here, args =>
     {
       var all_docs = false
       var max_jobs = 1
+      var sequential = false
       var options = Options.init()
 
       val getopts =
         Getopts("""
 Usage: isabelle build_doc [OPTIONS] [DOCS ...]
 
   Options are:
     -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)
 
       if (!all_docs && docs.isEmpty) getopts.usage()
 
       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 --git a/src/Pure/Concurrent/par_list.scala b/src/Pure/Concurrent/par_list.scala
--- a/src/Pure/Concurrent/par_list.scala
+++ b/src/Pure/Concurrent/par_list.scala
@@ -1,63 +1,66 @@
 /*  Title:      Pure/Concurrent/par_list.scala
     Author:     Makarius
 
 Parallel list combinators.
 */
 
 
 package isabelle
 
 
 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))
 
       def cancel_other(self: Int = -1): Unit =
         state.change { case (futures, canceled) =>
           if (!canceled) {
             for ((future, i) <- futures.iterator.zipWithIndex if i != self)
               future.cancel()
           }
           (futures, true)
         }
 
       try {
         state.change(_ =>
           (xs.iterator.zipWithIndex.map({ case (x, self) =>
             Future.fork {
               Exn.capture { f(x) } match {
                 case Exn.Exn(exn) => cancel_other(self); throw exn
                 case Exn.Res(res) => res
               }
             }
           }).toList, false))
 
         state.value._1.map(_.join_result)
       }
       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] =
   {
     class Found(val res: B) extends Exception
     val results =
       managed_results(
         (x: A) => f(x) match { case None => () case Some(y) => throw new Found(y) }, xs)
     results.collectFirst({ case Exn.Exn(found: Found) => found.res }) match {
       case None => Exn.release_first(results); None
       case some => some
     }
   }
 
   def find_some[A](P: A => Boolean, xs: List[A]): Option[A] =
     get_some((x: A) => if (P(x)) Some(x) else None, xs)
 
   def exists[A](P: A => Boolean, xs: List[A]): Boolean = find_some(P, xs).isDefined
   def forall[A](P: A => Boolean, xs: List[A]): Boolean = !exists((x: A) => !P(x), xs)
 }