Integrate the documentation generator

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 {

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 {

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                                                                 ///////
 ////////////////////////////////////////////////////////////////////////////////////////////////////

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))
 

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)