diff --git a/src/main/scala/viper/server/vsi/VerificationServer.scala b/src/main/scala/viper/server/vsi/VerificationServer.scala index ec777d9..10f4491 100644 --- a/src/main/scala/viper/server/vsi/VerificationServer.scala +++ b/src/main/scala/viper/server/vsi/VerificationServer.scala @@ -241,7 +241,12 @@ trait VerificationServer extends Post { // FIXME This assumes that someone will actually complete the verification job queue. // FIXME Could we guarantee that the client won't forget to do this? - ver_handle.queue.watchCompletion() + ver_handle match { + case VerHandle(null, null, null, _) => + Future.successful(Done) + case _ => + ver_handle.queue.watchCompletion() + } }) } } @@ -299,8 +304,13 @@ trait VerificationServer extends Post { handle_future.flatMap { case AstHandle(actor, _, _, _) => (actor ? VerificationProtocol.StopAstConstruction).mapTo[String] + case VerHandle(null, _, _, _) => + Future.successful("Job had no actor.") case VerHandle(actor, _, _, _) => (actor ? VerificationProtocol.StopVerification).mapTo[String] + }.recover { + case _: akka.pattern.AskTimeoutException => + "Job actor already terminated." } } toList val overall_interrupt_future: Future[List[String]] = Future.sequence(interrupt_future_list)