clarified signature;
authorwenzelm
Thu, 17 Aug 2023 14:46:24 +0200
changeset 78532 62c6164f0fc1
parent 78531 ec761aa6cc64
child 78533 dd0501accda8
clarified signature;
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 =>