# HG changeset patch
# User wenzelm
# Date 1608761337 -3600
# Node ID bcba32fd89dedfbc058c3984383b3c0c26df22d0
# Parent  d0a0b74f0ad70d77e3a58ac4bd4833e79fd774cb
more interrupts;

diff -r d0a0b74f0ad7 -r bcba32fd89de src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Wed Dec 23 23:03:03 2020 +0100
+++ b/src/Pure/Thy/presentation.scala	Wed Dec 23 23:08:57 2020 +0100
@@ -374,6 +374,7 @@
     session: String,
     deps: Sessions.Deps,
     db_context: Sessions.Database_Context,
+    progress: Progress = new Progress,
     html_context: HTML_Context,
     presentation: Context)
   {
@@ -431,6 +432,8 @@
 
       for (thy_name <- base.session_theories)
       yield {
+        progress.expose_interrupt()
+
         val syntax = base.theory_syntax(thy_name)
         val keywords = syntax.keywords
         val spans = syntax.parse_spans(Symbol.decode(File.read(thy_name.path)))
@@ -467,6 +470,8 @@
             (src_path, xml) <- snapshot.xml_markup_blobs(elements = html_elements).iterator
             if xml.nonEmpty
           } yield {
+            progress.expose_interrupt()
+
             val file_name = (files_path + src_path.squash.html).implode
 
             seen_files.find(p => p._1 == src_path || p._2 == file_name) match {
diff -r d0a0b74f0ad7 -r bcba32fd89de src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Dec 23 23:03:03 2020 +0100
+++ b/src/Pure/Tools/build.scala	Wed Dec 23 23:08:57 2020 +0100
@@ -510,7 +510,7 @@
             progress.expose_interrupt()
             progress.echo("Presenting " + session_name + " ...")
             Presentation.session_html(
-              resources, session_name, deps, db_context, html_context, presentation)
+              resources, session_name, deps, db_context, progress, html_context, presentation)
           })
 
         val browser_chapters =