Revert "Merge pull request #201 from viperproject/sem-highlight"

This reverts commit 7c5305b, reversing
changes made to 5cd18bd.

.gitignore

@@ -8,6 +8,3 @@ 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 := "3.0.0", // has to be a proper semver
+        version := "2.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.20.1", // Java implementation of language server protocol
+        libraryDependencies += "org.eclipse.lsp4j" % "org.eclipse.lsp4j" % "0.15.0", // 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,7 +11,6 @@ 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
 
@@ -27,8 +26,7 @@ case class ServerCrashException(e: Throwable) extends Exception(e)
 
 class AstWorker(val arg_list: List[String],
                 override val logger: Logger,
-                private val config: ViperConfig,
-                private val loader: Option[FileLoader]
+                private val config: ViperConfig
                )(override val executor: VerificationExecutionContext)
   extends MessageReportingTask[Option[Program]] {
 
@@ -39,7 +37,7 @@ class AstWorker(val arg_list: List[String],
     val astGen = new AstGenerator(logger, reporter, arg_list, disablePlugins = config.disablePlugins())
 
     val ast_option: Option[Program] = try {
-      astGen.generateViperAst(file, loader)
+      astGen.generateViperAst(file)
     } catch {
       case _: java.nio.file.NoSuchFileException =>
         logger.error(s"The file ($file) for which verification has been requested was not found.")

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

@@ -13,7 +13,6 @@ 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._
@@ -59,10 +58,10 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V
     }
   }
 
-  def requestAst(arg_list: List[String], localLogger: Option[Logger] = None, loader: Option[FileLoader] = None): AstJobId = {
+  def requestAst(arg_list: List[String], localLogger: Option[Logger] = None): AstJobId = {
     require(config != null)
     val logger = combineLoggers(localLogger)
-    val task_backend = new AstWorker(arg_list, logger, config, loader)(executor)
+    val task_backend = new AstWorker(arg_list, logger, config)(executor)
     val ast_id = initializeAstConstruction(task_backend)
 
     if (ast_id.id >= 0) {
@@ -73,7 +72,6 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V
     }
     ast_id
   }
-  def discardAstJobOnCompletion(jid: AstJobId, jobActor: ActorRef): Unit = discardAstOnCompletion(jid, jobActor)
 
   def verifyWithAstJob(programId: String, ast_id: AstJobId, backend_config: ViperBackendConfig, localLogger: Option[Logger] = None): VerJobId = {
     val logger = combineLoggers(localLogger)
@@ -125,11 +123,7 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V
     ver_id
   }
 
-  override def streamMessages(jid: VerJobId, clientActor: ActorRef, full: Boolean): Option[Future[Done]] = {
-    globalLogger.info(s"Streaming results for job #${jid.id}.")
-    super.streamMessages(jid, clientActor, full)
-  }
-  override def streamMessages(jid: AstJobId, clientActor: ActorRef): Option[Future[Done]] = {
+  override def streamMessages(jid: VerJobId, 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, true).getOrElse(Future.failed(JobNotFoundException))
+    val complete_future = core.streamMessages(jid, actor).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/jsonWriters/ViperIDEProtocol.scala

@@ -493,8 +493,6 @@ 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
       }))
   })
 

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

@@ -7,16 +7,15 @@
 package viper.server.frontends.lsp
 
 import ch.qos.logback.classic.Logger
-import org.eclipse.lsp4j.Range
+import org.eclipse.lsp4j.DocumentSymbol
 import viper.server.core.VerificationExecutionContext
 import viper.server.frontends.lsp.VerificationState.Ready
 
 import java.util.concurrent.{ConcurrentHashMap, ConcurrentMap}
+import scala.collection.mutable.ArrayBuffer
 import scala.concurrent.Future
 import scala.jdk.CollectionConverters._
 import scala.jdk.FutureConverters._
-import viper.server.frontends.lsp.file.FileManager
-import viper.server.frontends.lsp.file.VerificationManager
 
 /** manages per-client state and interacts with the server instance (which is shared among all clients) */
 class ClientCoordinator(val server: ViperServerService)(implicit executor: VerificationExecutionContext) {
@@ -47,41 +46,59 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif
     !_exited
   }
 
-  def closeFile(uri: String): Unit = {
-    val toRemove = Option(_files.get(uri)).map(fm => {
-      fm.isOpen = false
-      fm.removeDiagnostics()
-      fm.isRoot
-    }).getOrElse(false)
-    if (toRemove) {
-      logger.trace(s"Removing FileManager for $uri")
-      _files.remove(uri)
+  def addFileIfNecessary(uri: String): Unit = {
+    logger.trace(s"Adding FileManager for $uri if it does not exist yet")
+    val coordinator = this
+    val createFMFunc = new java.util.function.Function[String, FileManager]() {
+      override def apply(t: String): FileManager = {
+        logger.trace(s"FileManager created for $uri")
+        new FileManager(coordinator, uri)
+      }
     }
+    // we use `computeIfAbsent` instead of `putIfAbsent` such that a new FileManager is only created if it's absent
+    _files.computeIfAbsent(uri, createFMFunc)
+  }
+
+  def removeFileIfExists(uri: String): Unit = {
+    logger.trace(s"Removing FileManager for $uri")
+    _files.remove(uri)
+  }
+
+  /** clears definitions and symbols associated with a file */
+  def resetFile(uri: String): Unit = {
+    Option(_files.get(uri))
+      .foreach(fm => {
+        fm.symbolInformation = ArrayBuffer.empty
+        fm.definitions = ArrayBuffer.empty
+      })
   }
 
   def resetDiagnostics(uri: String): Unit = {
-    getFileManager(uri).removeDiagnostics()
+    Option(_files.get(uri))
+      .foreach(fm => fm.resetDiagnostics())
   }
 
-  def handleChange(uri: String, range: Range, text: String): Unit = {
-    val fm = getFileManager(uri)
-    fm.synchronized {
-      fm.handleContentChange(range, text)
-    }
+  def getSymbolsForFile(uri: String): Array[DocumentSymbol]= {
+    Option(_files.get(uri))
+      .map(fm => fm.symbolInformation.toArray)
+      .getOrElse(Array.empty)
+  }
+
+  def getDefinitionsForFile(uri: String): ArrayBuffer[Definition] = {
+    Option(_files.get(uri))
+      .map(fm => fm.definitions)
+      .getOrElse(ArrayBuffer.empty)
   }
 
   /** Checks if verification can be started for a given file.
     *
     * Informs client differently depending on whether or not verification attempt was triggered manually
     * */
-  def canVerificationBeStarted(uri: String, content: String, manuallyTriggered: Boolean): Boolean = {
+  def canVerificationBeStarted(uri: String, manuallyTriggered: Boolean): Boolean = {
     logger.trace("canVerificationBeStarted")
     if (server.isRunning) {
       logger.trace("server is running")
-      // This should only be necessary if one wants to verify a closed file for some reason
-      val fm = getFileManager(uri, Some(content))
-      // This will be the new project root
-      makeEmptyRoot(fm)
+      addFileIfNecessary(uri)
       true
     } else {
       logger.trace("server is not running")
@@ -94,15 +111,16 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif
   }
 
   def stopRunningVerification(uri: String): Future[Boolean] = {
-    val fm = getFileManager(uri)
-    fm.stop()
-      .map(_ => {
-        logger.trace(s"stopVerification has completed for ${fm.file.uri}")
-        val params = StateChangeParams(Ready.id, verificationCompleted = 0, verificationNeeded = 0, uri = uri)
-        sendStateChangeNotification(params, Some(fm))
-        true
-      })
-      .recover(_ => false)
+    Option(_files.get(uri))
+      .map(fm => fm.stopVerification()
+        .map(_ => {
+          logger.trace(s"stopVerification has completed for ${fm.uri}")
+          val params = StateChangeParams(Ready.id, verificationCompleted = 0, verificationNeeded = 0, uri = uri)
+          sendStateChangeNotification(params, Some(fm))
+          true
+        })
+        .recover(_ => false))
+      .getOrElse(Future.successful(false))
   }
 
   /** Stops all running verifications.
@@ -112,26 +130,18 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif
     * */
   def stopAllRunningVerifications(): Future[Unit] = {
     val tasks = _files.values().asScala.map(fm =>
-      fm.stop().map(_ => {
-        logger.trace(s"stopVerification has completed for ${fm.file.uri}")
+      fm.stopVerification().map(_ => {
+        logger.trace(s"stopVerification has completed for ${fm.uri}")
       }))
     Future.sequence(tasks).map(_ => {
       logger.debug("all running verifications have been stopped")
     })
   }
 
   /** returns true if verification was started */
-  def startVerification(backendClassName: String, customArgs: String, uri: String, manuallyTriggered: Boolean): Future[Boolean] = {
-    val fm = getFileManager(uri)
-    fm.startVerification(backendClassName, customArgs, fm.content, manuallyTriggered)
-  }
-
-  /** returns true if parse/typecheck was started */
-  def startParseTypecheck(uri: String): Boolean = {
-    val fm = getFileManager(uri)
-    val project = Option(_files.get(uri)).flatMap(_.projectRoot).getOrElse(uri)
-    val root = getFileManager(project)
-    root.runParseTypecheck(fm.content)
+  def startVerification(backendClassName: String, customArgs: String, uri: String, manuallyTriggered: Boolean): Boolean = {
+    Option(_files.get(uri))
+      .exists(fm => fm.startVerification(backendClassName, customArgs, manuallyTriggered))
   }
 
   /** flushes verification cache, optionally only for a particular file */
@@ -163,9 +173,9 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif
     *
     * If state change is related to a particular file, its manager's state is also updated.
     * */
-  def sendStateChangeNotification(params: StateChangeParams, task: Option[VerificationManager]): Unit = {
+  def sendStateChangeNotification(params: StateChangeParams, task: Option[FileManager]): Unit = {
     // update file manager's state:
-    task.foreach(vm => vm.state = VerificationState(params.newState))
+    task.foreach(fm => fm.state = VerificationState(params.newState))
     try {
       client.notifyStateChanged(params)
     } catch {
@@ -194,48 +204,4 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif
     if (!isAlive) return
     client.notifyHint(HintMessage(message, showSettingsButton, showViperToolsUpdateButton ))
   }
-
-  private def getFileManager(uri: String, content: Option[String] = None): FileManager = {
-    var createdNew = false
-    val coordinator = this
-    val createFMFunc = new java.util.function.Function[String, FileManager]() {
-      override def apply(t: String): FileManager = {
-        logger.trace(s"FileManager created for $uri")
-        createdNew = true
-        FileManager(uri, coordinator, content)
-      }
-    }
-    // we use `computeIfAbsent` instead of `putIfAbsent` such that a new FileManager is only created if it's absent
-    val fm = _files.computeIfAbsent(uri, createFMFunc)
-    // Override the content if we are given one and the file manager was not just created
-    if (!createdNew && content.isDefined) fm.content.set(content.get)
-    fm
-  }
-  def ensureFmExists(uri: String, content: String): FileManager = {
-    getFileManager(uri, Some(content))
-  }
-  def getRoot(uri: String): FileManager = {
-    val fm = getFileManager(uri)
-    fm.projectRoot.map(getFileManager(_)).getOrElse(fm)
-  }
-
-  ///////////////////////
-  // Project management
-  ///////////////////////
-
-  def addToProject(uri: String, root: String, getContents: Boolean): (Option[String], Option[Set[String]]) = {
-    getFileManager(uri).addToProject(root, getContents)
-  }
-  def removeFromProject(uri: String, root: String) = {
-    Option(_files.get(uri)).map(_.removeFromProject(root))
-  }
-  def makeEmptyRoot(fm: FileManager) = {
-    for (leaves <- fm.projectLeaves; leaf <- leaves) {
-      removeFromProject(leaf, fm.file_uri)
-    }
-    fm.project = Left(Map())
-  }
-  def handleChangeInLeaf(root: String, leaf: String, range: Range, text: String): Unit = {
-    Option(_files.get(root)).map(_.handleChangeInLeaf(leaf, range, text))
-  }
 }

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

@@ -21,10 +21,8 @@ object C2S_Commands {
   // final val GetExecutionTrace = "GetExecutionTrace"
   final val RemoveDiagnostics = "RemoveDiagnostics"
   final val GetViperFileEndings = "GetViperFileEndings"
-  final val SetupProject = "SetupProject"
   final val FlushCache = "FlushCache"
   final val GetIdentifier = "GetIdentifier"
-  final val GetRange = "GetRange"
 }
 
 object S2C_Commands {