--- 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 {
--- 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 =