# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1719838011 -7200
# Node ID 8ae5312032ccf6fd5f7e3c64e3fe126e65b2cb59
# Parent  010d45681b8788f2786ea6006051e7c0a9a00e39
clarified: more operations;

diff -r 010d45681b87 -r 8ae5312032cc src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Mon Jul 01 14:31:30 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Mon Jul 01 14:46:51 2024 +0200
@@ -234,6 +234,11 @@
 
     def add_running(job: Job): State = copy(running = running + (job.name -> job))
     def remove_running(name: String): State = copy(running = running - name)
+    def cancel_running(name: String): State =
+      running.get(name) match {
+        case Some(job) => copy(running = (running - name) + (name -> job.copy(cancelled = true)))
+        case None => this
+      }
 
     def add_finished(result: Result): State = copy(finished = finished + (result.name -> result))
 
@@ -1178,10 +1183,7 @@
                   _state = _state.remove_pending(task.name)
                   Model.Cancelled
                 case job: Job =>
-                  val job1 = job.copy(cancelled = true)
-                  _state = _state
-                    .remove_running(job.name)
-                    .add_running(job1)
+                  _state = _state.cancel_running(job.name)
                   Model.Cancelled
                 case result: Result => Model.Details(result, _state, public = false)
               }