Add extra lsp features

.gitignore

@@ -8,3 +8,6 @@ ter.bat
 ver.bat
 .bsp/
 logs/
+.bloop
+.metals
+metals.sbt

build.sbt

@@ -18,7 +18,7 @@ lazy val server = (project in file("."))
         // General settings
         name := "ViperServer",
         organization := "viper",
-        version := "2.0.0", // has to be a proper semver
+        version := "3.0.0", // has to be a proper semver
 
         // Fork test to a different JVM than SBT's, avoiding SBT's classpath interfering with
         // classpath used by Scala's reflection.
@@ -30,7 +30,7 @@ lazy val server = (project in file("."))
         libraryDependencies += "com.typesafe.akka" %% "akka-stream" % "2.6.10",
         libraryDependencies += "com.typesafe.akka" %% "akka-stream-testkit" % "2.6.10" % Test,
         libraryDependencies += "com.typesafe.akka" %% "akka-http-testkit" % "10.2.1" % Test,
-        libraryDependencies += "org.eclipse.lsp4j" % "org.eclipse.lsp4j" % "0.15.0", // Java implementation of language server protocol
+        libraryDependencies += "org.eclipse.lsp4j" % "org.eclipse.lsp4j" % "0.20.1", // Java implementation of language server protocol
 
         silicon / excludeFilter := "logback.xml", /* Ignore Silicon's Logback configuration */
         carbon / excludeFilter := "logback.xml", /* Ignore Carbon's Logback configuration */

src/main/scala/viper/server/core/AstWorker.scala

@@ -11,6 +11,7 @@ import viper.server.ViperConfig
 import viper.server.utility.AstGenerator
 import viper.server.vsi.AstConstructionException
 import viper.silver.ast.Program
+import viper.silver.ast.utility.FileLoader
 import viper.silver.reporter.{Entity, ExceptionReport}
 import viper.silver.verifier.VerificationResult
 
@@ -24,20 +25,21 @@ object OutOfResourcesException extends AstConstructionException
 case class ServerCrashException(e: Throwable) extends Exception(e)
 
 
-class AstWorker(val arg_list: List[String],
+class AstWorker(val file: String,
+                val args: List[String],
                 override val logger: Logger,
-                private val config: ViperConfig
+                private val config: ViperConfig,
+                private val loader: Option[FileLoader]
                )(override val executor: VerificationExecutionContext)
   extends MessageReportingTask[Option[Program]] {
 
-  private def constructAst(arg_list: Seq[String]): Option[Program] = {
-    val file: String = arg_list.last
+  private def constructAst(args: Seq[String]): Option[Program] = {
 
     val reporter = new ActorReporter("AstGenerationReporter")
-    val astGen = new AstGenerator(logger, reporter, arg_list, disablePlugins = config.disablePlugins())
+    val astGen = new AstGenerator(logger, reporter, args, disablePlugins = config.disablePlugins())
 
     val ast_option: Option[Program] = try {
-      astGen.generateViperAst(file)
+      astGen.generateViperAst(file, loader)
     } catch {
       case _: java.nio.file.NoSuchFileException =>
         logger.error(s"The file ($file) for which verification has been requested was not found.")
@@ -68,5 +70,5 @@ class AstWorker(val arg_list: List[String],
     ???
   }
 
-  override def call(): Option[Program] = constructAst(arg_list)
+  override def call(): Option[Program] = constructAst(args)
 }

src/main/scala/viper/server/core/ViperCoreServer.scala

@@ -13,6 +13,7 @@ import ch.qos.logback.classic.Logger
 import viper.server.ViperConfig
 import viper.server.vsi.{AstHandle, AstJobId, VerJobId, VerificationServer}
 import viper.silver.ast.Program
+import viper.silver.ast.utility.FileLoader
 import viper.silver.logger.ViperLogger
 
 import scala.concurrent.duration._
@@ -58,10 +59,11 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V
     }
   }
 
-  def requestAst(arg_list: List[String], localLogger: Option[Logger] = None): AstJobId = {
+  def requestAst(file: String, backend_config: ViperBackendConfig, localLogger: Option[Logger] = None, loader: Option[FileLoader] = None): AstJobId = {
     require(config != null)
     val logger = combineLoggers(localLogger)
-    val task_backend = new AstWorker(arg_list, logger, config)(executor)
+    val args: List[String] = backend_config.toList
+    val task_backend = new AstWorker(file, args, logger, config, loader)(executor)
     val ast_id = initializeAstConstruction(task_backend)
 
     if (ast_id.id >= 0) {
@@ -72,6 +74,7 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V
     }
     ast_id
   }
+  def discardAstJobOnCompletion(jid: AstJobId): Unit = discardAstOnCompletion(jid)
 
   def verifyWithAstJob(programId: String, ast_id: AstJobId, backend_config: ViperBackendConfig, localLogger: Option[Logger] = None): VerJobId = {
     val logger = combineLoggers(localLogger)
@@ -123,7 +126,11 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V
     ver_id
   }
 
-  override def streamMessages(jid: VerJobId, clientActor: ActorRef): Option[Future[Done]] = {
+  override def streamMessages(jid: VerJobId, clientActor: ActorRef, include_ast: Boolean): Option[Future[Done]] = {
+    globalLogger.info(s"Streaming results for job #${jid.id}.")
+    super.streamMessages(jid, clientActor, include_ast)
+  }
+  override def streamMessages(jid: AstJobId, clientActor: ActorRef): Option[Future[Done]] = {
     globalLogger.info(s"Streaming results for job #${jid.id}.")
     super.streamMessages(jid, clientActor)
   }

src/main/scala/viper/server/core/ViperCoreServerUtils.scala

@@ -56,7 +56,7 @@ object ViperCoreServerUtils {
     import scala.language.postfixOps
 
     val actor = executor.actorSystem.actorOf(SeqActor.props(jid, core.globalLogger))
-    val complete_future = core.streamMessages(jid, actor).getOrElse(Future.failed(JobNotFoundException))
+    val complete_future = core.streamMessages(jid, actor, include_ast = true).getOrElse(Future.failed(JobNotFoundException))
     complete_future.flatMap(_ => {
       implicit val askTimeout: Timeout = Timeout(core.config.actorCommunicationTimeout() milliseconds)
       (actor ? SeqActor.Result).mapTo[Future[List[Message]]].flatten

src/main/scala/viper/server/frontends/http/ViperHttpServer.scala

@@ -65,8 +65,6 @@ class ViperHttpServer(config: ViperConfig)(executor: VerificationExecutionContex
       return VerificationRequestReject("File not found")
     }
 
-    val ast_id = requestAst(arg_list)
-
     val backend = try {
       ViperBackendConfig(arg_list_partial)
     } catch {
@@ -76,6 +74,7 @@ class ViperHttpServer(config: ViperConfig)(executor: VerificationExecutionContex
         return VerificationRequestReject("Invalid arguments for backend.")
     }
 
+    val ast_id = requestAst(file, backend)
     val ver_id = verifyWithAstJob(file, ast_id, backend)
 
     VerificationRequestAccept(ast_id, ver_id)

src/main/scala/viper/server/frontends/http/jsonWriters/ViperIDEProtocol.scala

@@ -493,6 +493,7 @@ object ViperIDEProtocol extends akka.http.scaladsl.marshallers.sprayjson.SprayJs
         case q: QuantifierInstantiationsMessage => q.toJson
         case q: QuantifierChosenTriggersMessage => q.toJson
         case v: VerificationTerminationMessage => v.toJson
+        case p: PProgramReport => p.semanticAnalysisSuccess.toJson
         case w: WarningsDuringVerification => w.toJson
       }))
   })