# HG changeset patch
# User wenzelm
# Date 1689618705 -7200
# Node ID 6c211e1c94d5881ee65aac176bbd0fcb6edaebad
# Parent  9c86b609eeb6d8d85879ae01f1ef91ff67cde1a0
clarified errors;

diff -r 9c86b609eeb6 -r 6c211e1c94d5 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Mon Jul 17 16:09:59 2023 +0200
+++ b/src/Pure/System/progress.scala	Mon Jul 17 20:31:45 2023 +0200
@@ -253,7 +253,7 @@
   database_progress =>
 
   private var _agent_uuid: String = ""
-  private var _context: Long = 0
+  private var _context: Long = -1
   private var _seen: Long = 0
 
   def agent_uuid: String = synchronized { _agent_uuid }
@@ -305,7 +305,9 @@
   }
 
   private def sync_database[A](body: => A): A = synchronized {
-    require(_context > 0)
+    if (_context < 0) throw new IllegalStateException("Database_Progress before init")
+    if (_context == 0) throw new IllegalStateException("Database_Progress after exit")
+
     Progress.Data.transaction_lock(db, label = "Database_Progress.sync") {
       val stopped_db = Progress.Data.read_progress_stopped(db, _context)
       val stopped = base_progress.stopped