diff --git a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala index 5e9c3fbf..d1e0ec6d 100644 --- a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala +++ b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala @@ -144,6 +144,10 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif .exists(fm => fm.startVerification(backendClassName, customArgs, manuallyTriggered)) } + def getDocumentation(uri: String): Option[String] = { + _files.get(uri).getDocumentation() + } + /** flushes verification cache, optionally only for a particular file */ def flushCache(uriOpt: Option[String], backendOpt: Option[String]): Future[Unit] = { (uriOpt, backendOpt) match { diff --git a/src/main/scala/viper/server/frontends/lsp/CommandProtocol.scala b/src/main/scala/viper/server/frontends/lsp/CommandProtocol.scala index e0a2e674..57845c70 100644 --- a/src/main/scala/viper/server/frontends/lsp/CommandProtocol.scala +++ b/src/main/scala/viper/server/frontends/lsp/CommandProtocol.scala @@ -23,6 +23,7 @@ object C2S_Commands { final val GetViperFileEndings = "GetViperFileEndings" final val FlushCache = "FlushCache" final val GetIdentifier = "GetIdentifier" + final val GetDocumentation = "GetDocumentation" } object S2C_Commands { diff --git a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala index be00e4f9..0d2889dd 100644 --- a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala +++ b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala @@ -188,6 +188,10 @@ case class GetIdentifierResponse(identifier: String) case class VerificationNotStartedParams(uri: String) +case class GetDocumentationRequest(uri: String) + +case class GetDocumentationResponse(documentation: String) + //////////////////////////////////////////////////////////////////////////////////////////////////// ////// SETTINGS /////// //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/src/main/scala/viper/server/frontends/lsp/FileManager.scala b/src/main/scala/viper/server/frontends/lsp/FileManager.scala index 598e2338..8ebfa5b3 100644 --- a/src/main/scala/viper/server/frontends/lsp/FileManager.scala +++ b/src/main/scala/viper/server/frontends/lsp/FileManager.scala @@ -19,6 +19,7 @@ import viper.silver.ast import viper.silver.ast.{AbstractSourcePosition, Domain, Field, Function, HasLineColumn, Method, Predicate, SourcePosition} import viper.silver.reporter._ import viper.silver.verifier.{AbortedExceptionally, AbstractError, ErrorMessage} +import viper.server.utility.DocProvider import scala.jdk.CollectionConverters._ import scala.collection.mutable.ArrayBuffer @@ -125,6 +126,11 @@ class FileManager(coordinator: ClientCoordinator, file_uri: String)(implicit exe } } + def getDocumentation(): Option[String] = { + val docProvider = new DocProvider(coordinator.logger) + docProvider.generateViperdocData(uri.getPath()) + } + object RelayActor { def props(task: FileManager, backendClassName: String): Props = Props(new RelayActor(task, backendClassName)) diff --git a/src/main/scala/viper/server/frontends/lsp/Receiver.scala b/src/main/scala/viper/server/frontends/lsp/Receiver.scala index 4501cd12..5d72ef4f 100644 --- a/src/main/scala/viper/server/frontends/lsp/Receiver.scala +++ b/src/main/scala/viper/server/frontends/lsp/Receiver.scala @@ -215,6 +215,14 @@ class CustomReceiver(config: ViperConfig, server: ViperServerService, serverUrl: } } + @JsonRequest(C2S_Commands.GetDocumentation) + def onGetDocumentation(request: GetDocumentationRequest): CompletionStage[GetDocumentationResponse] = { + coordinator.logger.debug("On getting documentation") + val uri = request.uri + val data = coordinator.getDocumentation(uri).getOrElse("") + CompletableFuture.completedFuture(GetDocumentationResponse(data)) + } + override def connect(client: LanguageClient): Unit = { val c = client.asInstanceOf[IdeLanguageClient] coordinator.setClient(c)