# HG changeset patch
# User wenzelm
# Date 1612122282 -3600
# Node ID 60c32e2c5577cfd85e682525cc3bc994fb50e89b
# Parent  a81ec42bac45a164ce372baea6c15fccf1646b27
clarified messages;

diff -r a81ec42bac45 -r 60c32e2c5577 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 {