--- 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 =>