Fixes

Author: rayman2000

src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala

@@ -25,10 +25,9 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif
   private var _client: Option[IdeLanguageClient] = None
   private val _files: ConcurrentMap[String, FileManager] = new ConcurrentHashMap() // each file is managed individually.
   private var _vprFileEndings: Option[Array[String]] = None
-  private var _exited: Boolean = false
 
-  def client: IdeLanguageClient = {
-    _client.getOrElse({assert(false, "getting client failed - client has not been set yet"); ???})
+  def client: Option[IdeLanguageClient] = {
+    _client
   }
 
   def setClient(c: IdeLanguageClient): Unit = {
@@ -38,15 +37,10 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif
 
   /** called when client disconnects; the server should however remain running */
   def exit(): Unit = {
-    _exited = true
     _client = None
     _files.clear()
   }
 
-  def isAlive: Boolean = {
-    !_exited
-  }
-
   def closeFile(uri: String): Unit = {
     val toRemove = Option(_files.get(uri)).map(fm => {
       fm.isOpen = false
@@ -167,17 +161,17 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif
     // update file manager's state:
     task.foreach(vm => vm.state = VerificationState(params.newState))
     try {
-      client.notifyStateChanged(params)
+      client.get.notifyStateChanged(params)
     } catch {
       case e: Throwable => logger.debug(s"Error while changing state: $e")
     }
   }
 
   def refreshEndings(): Future[Array[String]] = {
-    client.requestVprFileEndings().asScala.map(response => {
+    client.map{_.requestVprFileEndings().asScala.map(response => {
       _vprFileEndings = Some(response.fileEndings)
       response.fileEndings
-    })
+    })}.getOrElse(Future(Array()))
   }
 
   def isViperSourceFile(uri: String): Future[Boolean] = {
@@ -191,8 +185,7 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif
   }
 
   def hint(message: String, showSettingsButton: Boolean = false, showViperToolsUpdateButton: Boolean = false): Unit = {
-    if (!isAlive) return
-    client.notifyHint(HintMessage(message, showSettingsButton, showViperToolsUpdateButton ))
+    client.map{_.notifyHint(HintMessage(message, showSettingsButton, showViperToolsUpdateButton ))}
   }
 
   private def getFileManager(uri: String, content: Option[String] = None): FileManager = {

src/main/scala/viper/server/frontends/lsp/ClientLogger.scala

@@ -41,15 +41,16 @@ class ClientAppender(coordinator: ClientCoordinator) extends UnsynchronizedAppen
     def getParams(logLevel: LogLevel): LogParams =
       LogParams(event.getMessage, logLevel.id)
 
-    if (!coordinator.isAlive) return
+    if (coordinator.client.isEmpty) return
+    val client = coordinator.client.get
     event.getLevel match {
       case Level.OFF =>
-      case Level.ERROR => coordinator.client.notifyLog(getParams(LogLevel.Info))
-      case Level.WARN => coordinator.client.notifyLog(getParams(LogLevel.Info))
-      case Level.INFO => coordinator.client.notifyLog(getParams(LogLevel.Info))
-      case Level.DEBUG => coordinator.client.notifyLog(getParams(LogLevel.Debug))
-      case Level.TRACE => coordinator.client.notifyLog(getParams(LogLevel.LowLevelDebug))
-      case Level.ALL => coordinator.client.notifyLog(getParams(LogLevel.LowLevelDebug))
+      case Level.ERROR => client.notifyLog(getParams(LogLevel.Info))
+      case Level.WARN => client.notifyLog(getParams(LogLevel.Info))
+      case Level.INFO => client.notifyLog(getParams(LogLevel.Info))
+      case Level.DEBUG => client.notifyLog(getParams(LogLevel.Debug))
+      case Level.TRACE => client.notifyLog(getParams(LogLevel.LowLevelDebug))
+      case Level.ALL => client.notifyLog(getParams(LogLevel.LowLevelDebug))
     }
   }
 }

src/main/scala/viper/server/frontends/lsp/Receiver.scala

@@ -405,16 +405,16 @@ class CustomReceiver(config: ViperConfig, server: ViperServerService, serverUrl:
           if (verificationStarted) {
             coordinator.logger.info("Verification Started")
           } else {
-            coordinator.client.notifyVerificationNotStarted(VerificationNotStartedParams(data.uri))
+            coordinator.client.map{_.notifyVerificationNotStarted(VerificationNotStartedParams(data.uri))}
           }
         })
       }).recover(e => {
         coordinator.logger.debug(s"Error handling verify request: $e")
-        coordinator.client.notifyVerificationNotStarted(VerificationNotStartedParams(data.uri))
+        coordinator.client.map{_.notifyVerificationNotStarted(VerificationNotStartedParams(data.uri))}
       })
     } else {
       coordinator.logger.info("The verification cannot be started.")
-      coordinator.client.notifyVerificationNotStarted(VerificationNotStartedParams(data.uri))
+      coordinator.client.map{_.notifyVerificationNotStarted(VerificationNotStartedParams(data.uri))}
     }
   }
 

src/main/scala/viper/server/frontends/lsp/ViperServerService.scala

@@ -115,13 +115,19 @@ class ViperServerService(config: ViperConfig)(override implicit val executor: Ve
   }
 
   private def stopOnlyVerification(handle: VerHandle, combinedLogger: Logger): Future[Boolean] = {
-    implicit val askTimeout: Timeout = Timeout(config.actorCommunicationTimeout() milliseconds)
-    val interrupt: Future[String] = (handle.job_actor ? StopVerification).mapTo[String]
-    handle.job_actor ! PoisonPill // the actor played its part.
-    interrupt.map(msg => {
-      combinedLogger.info(msg)
-      true
-    })
+    handle match {
+      // If AST construction failed, a verification handle will be returned where the actor field is null.
+      case VerHandle(null, _, _, _) => Future.successful(false)
+      case _ => {
+        implicit val askTimeout: Timeout = Timeout(config.actorCommunicationTimeout() milliseconds)
+        val interrupt: Future[String] = (handle.job_actor ? StopVerification).mapTo[String]
+        handle.job_actor ! PoisonPill // the actor played its part.
+        interrupt.map(msg => {
+          combinedLogger.info(msg)
+          true
+        })
+      }
+    }
   }
 
   def stopAstConstruction(jid: AstJobId, localLogger: Option[Logger] = None): Future[Boolean] = {

src/main/scala/viper/server/frontends/lsp/file/Manager.scala

@@ -90,9 +90,10 @@ trait StandardManager extends Manager {
     c.onUpdate()
   }
 
+
   // CodeLens
   type CodeLensContainer = utility.StageArrayContainer.ArrayContainer[lsp.CodeLens, lsp4j.CodeLens]
-  val codeLensContainer: CodeLensContainer = utility.LspContainer(utility.CodeLensTranslator, coordinator.client.refreshCodeLenses)
+  val codeLensContainer: CodeLensContainer = utility.LspContainer(utility.CodeLensTranslator, if (coordinator.client.isDefined) coordinator.client.get.refreshCodeLenses else () => {})
   containers.addOne(codeLensContainer)
   def getCodeLens() = codeLensContainer.get(())
   def addCodeLens(first: Boolean)(vs: Seq[lsp.CodeLens]): Unit = add(codeLensContainer, first, vs)
@@ -102,7 +103,7 @@ trait StandardManager extends Manager {
   val diagnosticContainer: DiagnosticContainer = utility.LspContainer(utility.DiagnosticTranslator, publishDiags)
   private def publishDiags(): Unit = {
     val diagnosticParams = new PublishDiagnosticsParams(file.file_uri, getDiagnostic().asJava)
-    coordinator.client.publishDiagnostics(diagnosticParams)
+    coordinator.client.map{_.publishDiagnostics(diagnosticParams)}
   }
   // containers.addOne(diagnosticContainer)
   def getDiagnostic() = diagnosticContainer.get(())
@@ -145,14 +146,14 @@ trait StandardManager extends Manager {
 
   // InlayHint
   type InlayHintContainer = utility.StageArrayContainer.ArrayContainer[lsp.InlayHint, lsp4j.InlayHint]
-  val inlayHintContainer: InlayHintContainer = utility.LspContainer(utility.InlayHintTranslator, coordinator.client.refreshInlayHints)
+  val inlayHintContainer: InlayHintContainer = utility.LspContainer(utility.InlayHintTranslator, if(coordinator.client.isDefined) coordinator.client.get.refreshInlayHints else () => {})
   containers.addOne(inlayHintContainer)
   def getInlayHint() = inlayHintContainer.get(())
   def addInlayHint(first: Boolean)(vs: Seq[lsp.InlayHint]): Unit = add(inlayHintContainer, first, vs)
 
   // SemanticHighlight
   type SemanticHighlightContainer = utility.StageArrayContainer.ArrayContainer[lsp.SemanticHighlight, Lsp4jSemanticHighlight]
-  val semanticHighlightContainer: SemanticHighlightContainer = utility.LspContainer(utility.SemanticHighlightTranslator, coordinator.client.refreshSemanticTokens)
+  val semanticHighlightContainer: SemanticHighlightContainer = utility.LspContainer(utility.SemanticHighlightTranslator, if(coordinator.client.isDefined) coordinator.client.get.refreshSemanticTokens else () => {})
   containers.addOne(semanticHighlightContainer)
   def getSemanticHighlight() = semanticHighlightContainer.get(())
   def addSemanticHighlight(first: Boolean)(vs: Seq[lsp.SemanticHighlight]): Unit = add(semanticHighlightContainer, first, vs)

src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala

@@ -172,7 +172,7 @@ trait ProjectManager extends FullManager with ProjectAware {
     this.project = Left(newProject.map(uri => uri -> getLeafManager(uri)).toMap)
 
     val setupProject = SetupProjectParams(file.file_uri, newProject.toArray)
-    coordinator.client.requestSetupProject(setupProject)
+    coordinator.client.map{_.requestSetupProject(setupProject)}
   }
 
   def handleChangeInLeaf(leaf: String, range: Range, text: String): Unit = {

src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala

@@ -79,7 +79,7 @@ trait MessageHandler extends ProjectManager with VerificationManager with Quanti
       timeMs = 0
     } catch {
       case e: Throwable =>
-        coordinator.client.notifyVerificationNotStarted(lsp.VerificationNotStartedParams(file_uri))
+        coordinator.client.map{_.notifyVerificationNotStarted(lsp.VerificationNotStartedParams(file_uri))}
         coordinator.logger.debug(s"Error handling verification completion: $e")
     }
   }
@@ -207,7 +207,7 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends
       task.handleQuantifierInstantiations(quantifier, instantiations, magGen, maxCost)
     case m: Message =>
       coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] Message")
-      coordinator.client.notifyUnhandledViperServerMessage(lsp.UnhandledViperServerMessageTypeParams(m.name, m.toString, lsp.LogLevel.Info.id))
+      coordinator.client.map{_.notifyUnhandledViperServerMessage(lsp.UnhandledViperServerMessageTypeParams(m.name, m.toString, lsp.LogLevel.Info.id))}
     case Status.Success =>
       coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] Status.Success")
       // Success is sent when the stream is completed

src/main/scala/viper/server/vsi/VerificationServer.scala

@@ -168,7 +168,8 @@ trait VerificationServer extends Post {
   protected def discardAstOnCompletion(jid: AstJobId, jobActor: ActorRef) = {
     ast_jobs.lookupJob(jid).map(_.map(_.queue.watchCompletion().onComplete(_ => {
       ast_jobs.discardJob(jid)
-      jobActor ! PoisonPill
+      // Killing the jobActor here is too early, messages still arrive.
+      //jobActor ! PoisonPill
     })))
   }