more robust;
authorwenzelm
Thu, 10 Aug 2023 16:57:01 +0200
changeset 78505 8cd399b25dac
parent 78504 98e690566628
child 78506 14da1177d1c3
more robust;
src/Pure/System/progress.scala
src/Pure/Tools/build_cluster.scala
--- a/src/Pure/System/progress.scala	Thu Aug 10 16:49:17 2023 +0200
+++ b/src/Pure/System/progress.scala	Thu Aug 10 16:57:01 2023 +0200
@@ -348,9 +348,9 @@
 
   private def output_database(out: Progress.Output): Unit =
     sync_database {
-      val serial = Progress.private_data.next_messages_serial(db, _context)
+      _serial = _serial max Progress.private_data.next_messages_serial(db, _context)
 
-      Progress.private_data.write_messages(db, _context, serial, out.message)
+      Progress.private_data.write_messages(db, _context, _serial, out.message)
 
       out match {
         case message: Progress.Message =>
@@ -358,7 +358,6 @@
         case theory: Progress.Theory => base_progress.theory(theory)
       }
 
-      _serial = _serial max serial
       Progress.private_data.update_agent(db, _agent_uuid, _serial)
     }
 
--- a/src/Pure/Tools/build_cluster.scala	Thu Aug 10 16:49:17 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala	Thu Aug 10 16:57:01 2023 +0200
@@ -161,7 +161,8 @@
           build_id = build_context.build_uuid,
           isabelle_home = remote_isabelle_home,
           afp_root = remote_afp_root)
-      remote_isabelle.bash(script).check
+      Console.println(script)
+      remote_isabelle.bash(script).print.check
     }
 
     override def close(): Unit = ssh.close()