# HG changeset patch
# User wenzelm
# Date 1678092648 -3600
# Node ID 69af424b1f9d5863df7e603c91d7c62e87683a9b
# Parent  3481e54bd8f12cad684d7cb1dd8253dc15bc60df
less verbosity, amending 3bc49507bae5;

diff -r 3481e54bd8f1 -r 69af424b1f9d src/Tools/jEdit/src/session_build.scala
--- a/src/Tools/jEdit/src/session_build.scala	Mon Mar 06 09:46:41 2023 +0100
+++ b/src/Tools/jEdit/src/session_build.scala	Mon Mar 06 09:50:48 2023 +0100
@@ -53,7 +53,6 @@
     /* progress */
 
     private val progress = new Progress {
-      override def verbose: Boolean = true
       override def output(message: Progress.Message): Unit =
         if (do_output(message)) {
           GUI_Thread.later {
@@ -62,6 +61,9 @@
             vertical.setValue(vertical.getMaximum)
           }
         }
+
+      override def theory(theory: Progress.Theory): Unit =
+        output(theory.message.copy(verbose = false))
     }