# HG changeset patch
# User wenzelm
# Date 1609764016 -3600
# Node ID 759b6869377d05941e9506569fedbb23eee50d00
# Parent  22f5a628347721d22b913ccf4735bc6ca261c131
misc tuning and clarification;

diff -r 22f5a6283477 -r 759b6869377d src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Mon Jan 04 13:23:51 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Mon Jan 04 13:40:16 2021 +0100
@@ -437,18 +437,22 @@
     val theories: List[XML.Body] =
     {
       var seen_files = List.empty[(Path, String, Document.Node.Name)]
-
-      for (thy_name <- base.session_theories)
+      for {
+        thy_name <- base.session_theories
+        thy_command <- Build_Job.read_theory(db_context, resources, session, thy_name.theory)
+      }
       yield {
         progress.expose_interrupt()
         if (verbose) progress.echo("Presenting theory " + thy_name)
 
-        val syntax = base.theory_syntax(thy_name)
-        val keywords = syntax.keywords
-        val spans = syntax.parse_spans(Symbol.decode(File.read(thy_name.path)))
+        val snapshot = Document.State.init.snippet(thy_command)
 
         val thy_body =
         {
+          val syntax = base.theory_syntax(thy_name)
+          val keywords = syntax.keywords
+          val spans = syntax.parse_spans(Symbol.decode(File.read(thy_name.path)))
+
           val imports_offset = base.known_theories(thy_name.theory).header.imports_offset
           var token_offset = 1
           spans.flatMap(span =>
@@ -472,14 +476,13 @@
         }
 
         val files =
-          (for {
-            thy_command <-
-              Build_Job.read_theory(db_context, resources, session, thy_name.theory).iterator
-            snapshot = Document.State.init.snippet(thy_command)
-            (src_path, xml) <- snapshot.xml_markup_blobs(elements = html_elements).iterator
+          for {
+            (src_path, xml) <- snapshot.xml_markup_blobs(elements = html_elements)
             if xml.nonEmpty
-          } yield {
+          }
+          yield {
             progress.expose_interrupt()
+            if (verbose) progress.echo("Presenting file " + src_path)
 
             val file_name = (files_path + src_path.squash.html).implode
 
@@ -490,8 +493,6 @@
                   " in theory " + thy_name1 + " vs. " + thy_name)
             }
 
-            if (verbose) progress.echo("Presenting file " + src_path)
-
             val file_path = session_dir + Path.explode(file_name)
             html_context.init_fonts(file_path.dir)
 
@@ -501,7 +502,7 @@
               List(html_context.head(file_title), html_context.source(html_body(xml))))
 
             List(HTML.link(file_name, HTML.text(file_title)))
-          }).toList
+          }
 
         val thy_title = "Theory " + thy_name.theory_base_name
         HTML.write_document(session_dir, html_name(thy_name),