# HG changeset patch
# User wenzelm
# Date 1690020603 -7200
# Node ID ee5d9ecc6a0a4ae8cf867da25b484a26bb494f40
# Parent  1ab113f4db740d45384a310c8ff5b6abd7b919bb
tuned signature;
more operations;

diff -r 1ab113f4db74 -r ee5d9ecc6a0a src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Sat Jul 22 11:41:43 2023 +0200
+++ b/src/Pure/System/progress.scala	Sat Jul 22 12:10:03 2023 +0200
@@ -173,7 +173,7 @@
   def verbose: Boolean = false
   final def do_output(message: Progress.Message): Boolean = !message.verbose || verbose
 
-  def output(message: Progress.Message) = {}
+  def output(message: Progress.Message): Unit = {}
 
   final def echo(msg: String, verbose: Boolean = false): Unit =
     output(Progress.Message(Progress.Kind.writeln, msg, verbose = verbose))
@@ -187,6 +187,12 @@
   def theory(theory: Progress.Theory): Unit = output(theory.message)
   def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit = {}
 
+  final def capture[A](e: => A, msg: String, err: Throwable => String): Exn.Result[A] = {
+    echo(msg)
+    try { Exn.Res(e) }
+    catch { case exn: Throwable => echo_error_message(err(exn)); Exn.Exn[A](exn) }
+  }
+
   final def timeit[A](
     body: => A,
     message: Exn.Result[A] => String = null,