# HG changeset patch # User wenzelm # Date 1692296029 -7200 # Node ID 0a4e3e3a55d03beb01ea5dea436fd69c0d92fbc3 # Parent 555bdac7c279a8f36505df0d625a4edda84b632b more robust; diff -r 555bdac7c279 -r 0a4e3e3a55d0 src/Pure/System/progress.scala --- a/src/Pure/System/progress.scala Thu Aug 17 20:06:24 2023 +0200 +++ b/src/Pure/System/progress.scala Thu Aug 17 20:13:49 2023 +0200 @@ -274,6 +274,10 @@ extends Progress { database_progress => + if (UUID.unapply(context_uuid).isEmpty) { + error("Bad Database_Progress.context_uuid: " + quote(context_uuid)) + } + private var _agent_uuid: String = "" private var _context: Long = -1 private var _serial: Long = 0