merged

--- a/.hgtags	Sun Jan 31 12:10:20 2021 +0100
+++ b/.hgtags	Mon Feb 01 16:03:07 2021 +0100
@@ -41,3 +41,4 @@
 d4b67dc6f4ebd5f0fbd4ed1cccd0cc32c344d122 Isabelle2021-RC1
 802647edfe7be4478ca47a6e54e4d73733347e02 Isabelle2021-RC2
 02422c9add5e1c608290e48f3f0815c93ab00c1d Isabelle2021-RC3
+2ab14dbc6feb5e64c9c0c93ff2dff28f34a23f28 Isabelle2021-RC4

--- a/Admin/Release/CHECKLIST	Sun Jan 31 12:10:20 2021 +0100
+++ b/Admin/Release/CHECKLIST	Mon Feb 01 16:03:07 2021 +0100
@@ -78,7 +78,7 @@
 
 - Docker image:
 
-  isabelle build_docker -o Dockerfile -E -t makarius/isabelle:Isabelle2020 Isabelle2020_linux.tar.gz
+  isabelle build_docker -o Dockerfile -E -t makarius/isabelle:Isabelle2021 Isabelle2021_linux.tar.gz
 
   https://hub.docker.com/r/makarius/isabelle
   https://docs.docker.com/engine/reference/commandline/push

--- a/Admin/components/components.sha1	Sun Jan 31 12:10:20 2021 +0100
+++ b/Admin/components/components.sha1	Mon Feb 01 16:03:07 2021 +0100
@@ -217,6 +217,7 @@
 eda10c62da927a842c0a8881f726eac85e1cb4f7  naproche-20210122.tar.gz
 edcb517b7578db4eec1b6573b624f291776e11f6  naproche-20210124.tar.gz
 d858eb0ede6aea6b8cc40de63bd3a17f8f9f5300  naproche-20210129.tar.gz
+810ee0f35adada9bf970c33fd80b986ab2255bf3  naproche-20210201.tar.gz
 26df569cee9c2fd91b9ac06714afd43f3b37a1dd  nunchaku-0.3.tar.gz
 e573f2cbb57eb7b813ed5908753cfe2cb41033ca  nunchaku-0.5.tar.gz
 fe57793aca175336deea4f5e9c0d949a197850ac  opam-1.2.2.tar.gz

--- a/src/Pure/Thy/presentation.scala	Sun Jan 31 12:10:20 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Mon Feb 01 16:03:07 2021 +0100
@@ -458,32 +458,53 @@
           case _ => None
         }
 
-      for {
-        thy_name <- base.session_theories
-        thy_command <- Build_Job.read_theory(db_context, resources, session, thy_name.theory)
-      }
-      yield {
+      sealed case class Theory(
+        name: Document.Node.Name,
+        command: Command,
+        files_html: List[(Path, XML.Tree)],
+        html: XML.Tree)
+
+      def read_theory(name: Document.Node.Name): Option[Theory] =
+      {
         progress.expose_interrupt()
-        if (verbose) progress.echo("Presenting theory " + thy_name)
+        if (verbose) progress.echo("Presenting theory " + name)
 
-        val snapshot = Document.State.init.snippet(thy_command)
+        for (command <- Build_Job.read_theory(db_context, resources, session, name.theory))
+        yield {
+          val snapshot = Document.State.init.snippet(command)
 
+          val files_html =
+            for {
+              (src_path, xml) <- snapshot.xml_markup_blobs(elements = elements.html)
+              if xml.nonEmpty
+            }
+            yield {
+              progress.expose_interrupt()
+              if (verbose) progress.echo("Presenting file " + src_path)
+
+              (src_path, html_context.source(make_html(elements, entity_link, xml)))
+            }
+
+          val html =
+            html_context.source(
+              make_html(elements, entity_link, snapshot.xml_markup(elements = elements.html)))
+
+          Theory(name, command, files_html, html)
+        }
+      }
+
+      for (thy <- Par_List.map(read_theory, base.session_theories).flatten)
+      yield {
         val files =
-          for {
-            (src_path, xml) <- snapshot.xml_markup_blobs(elements = elements.html)
-            if xml.nonEmpty
-          }
+          for { (src_path, file_html) <- thy.files_html }
           yield {
-            progress.expose_interrupt()
-            if (verbose) progress.echo("Presenting file " + src_path)
-
             val file_name = (files_path + src_path.squash.html).implode
 
             seen_files.find(p => p._1 == src_path || p._2 == file_name) match {
-              case None => seen_files ::= (src_path, file_name, thy_name)
+              case None => seen_files ::= (src_path, file_name, thy.name)
               case Some((_, _, thy_name1)) =>
                 error("Incoherent use of file name " + src_path + " as " + quote(file_name) +
-                  " in theory " + thy_name1 + " vs. " + thy_name)
+                  " in theory " + thy_name1 + " vs. " + thy.name)
             }
 
             val file_path = session_dir + Path.explode(file_name)
@@ -491,21 +512,18 @@
 
             val file_title = "File " + Symbol.cartouche_decoded(src_path.implode_short)
             HTML.write_document(file_path.dir, file_path.file_name,
-              List(HTML.title(file_title)),
-              List(html_context.head(file_title),
-                html_context.source(make_html(elements, entity_link, xml))))
+              List(HTML.title(file_title)), List(html_context.head(file_title), file_html))
 
             List(HTML.link(file_name, HTML.text(file_title)))
           }
 
-        val thy_title = "Theory " + thy_name.theory_base_name
-        val thy_body = make_html(elements, entity_link, snapshot.xml_markup(elements = elements.html))
-        HTML.write_document(session_dir, html_name(thy_name),
-          List(HTML.title(thy_title)),
-          List(html_context.head(thy_title), html_context.source(thy_body)))
+        val thy_title = "Theory " + thy.name.theory_base_name
 
-        List(HTML.link(html_name(thy_name),
-          HTML.text(thy_name.theory_base_name) :::
+        HTML.write_document(session_dir, html_name(thy.name),
+          List(HTML.title(thy_title)), List(html_context.head(thy_title), thy.html))
+
+        List(HTML.link(html_name(thy.name),
+          HTML.text(thy.name.theory_base_name) :::
             (if (files.isEmpty) Nil else List(HTML.itemize(files)))))
       }
     }