clarified messages;
authorwenzelm
Tue, 04 Nov 2025 22:36:39 +0100
changeset 83510 0675f4daf3c0
parent 83509 d17e990ebd40
child 83511 4729ac19c03c
clarified messages;
src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Tue Nov 04 22:32:57 2025 +0100
+++ b/src/Pure/System/progress.scala	Tue Nov 04 22:36:39 2025 +0100
@@ -124,7 +124,7 @@
             if_proper(session, session + ": ") +
               "command " + quote(run.name) + " running for " + run.time(now).message +
               " (line " + run.line + " of theory " + quote(name.theory) + ")"
-          Progress.Message(Progress.Kind.writeln, text, verbose = true, status = true)
+          Progress.Message(Progress.Kind.writeln, text, verbose = true)
         })
   }
 
@@ -170,15 +170,12 @@
         for (old <- old_status if old._1 < session) buf += old
         if (status_detailed) {
           for (thy <- nodes_status.status_theories) buf += (session -> thy)
-          for (msg <- nodes_status.status_commands(status_threshold)) {
-            buf += (session -> msg)
-          }
         }
         for (old <- old_status if old._1 > session) buf += old
         buf.toList
       }
 
-      output(nodes_status.completed_theories)
+      output(nodes_status.completed_theories ::: nodes_status.status_commands(status_threshold))
       output_status(new_status)
     }
   }