# HG changeset patch
# User wenzelm
# Date 1692276384 -7200
# Node ID 62c6164f0fc1e5ecc59309a59e3172111b906371
# Parent  ec761aa6cc64a9657e7d52c7dea161feddcc6bf4
clarified signature;

diff -r ec761aa6cc64 -r 62c6164f0fc1 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Thu Aug 17 14:43:45 2023 +0200
+++ b/src/Pure/System/progress.scala	Thu Aug 17 14:46:24 2023 +0200
@@ -263,12 +263,12 @@
 /* database progress */
 
 class Database_Progress(
-  val db: SQL.Database,
-  val base_progress: Progress,
-  val output_stopped: Boolean = false,
-  val kind: String = "progress",
-  val hostname: String = Isabelle_System.hostname(),
-  val context_uuid: String = UUID.random().toString)
+  db: SQL.Database,
+  base_progress: Progress,
+  output_stopped: Boolean = false,
+  kind: String = "progress",
+  hostname: String = Isabelle_System.hostname(),
+  context_uuid: String = UUID.random().toString)
 extends Progress {
   database_progress =>