clarified messages;
authorwenzelm
Sun, 31 Jan 2021 20:44:42 +0100
changeset 73216 60c32e2c5577
parent 73215 a81ec42bac45
child 73217 2ab14dbc6feb
clarified messages;
src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Sun Jan 31 20:39:16 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Sun Jan 31 20:44:42 2021 +0100
@@ -467,6 +467,7 @@
       def read_theory(name: Document.Node.Name): Option[Theory] =
       {
         progress.expose_interrupt()
+        if (verbose) progress.echo("Presenting theory " + name)
 
         for (command <- Build_Job.read_theory(db_context, resources, session, name.theory))
         yield {
@@ -479,6 +480,8 @@
             }
             yield {
               progress.expose_interrupt()
+              if (verbose) progress.echo("Presenting file " + src_path)
+
               (src_path, html_context.source(make_html(elements, entity_link, xml)))
             }
 
@@ -492,13 +495,9 @@
 
       for (thy <- Par_List.map(read_theory, base.session_theories).flatten)
       yield {
-        if (verbose) progress.echo("Presenting theory " + thy.name)
-
         val files =
           for { (src_path, file_html) <- thy.files_html }
           yield {
-            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 {