fix mmt lsp

UniFormal · Jul 4, 2023 · 8dc74e5 · 8dc74e5
1 parent f4cc506
commit 8dc74e5
Show file tree

Hide file tree

Showing 4 changed files with 21 additions and 35 deletions.
diff --git a/src/mmt-lsp/src/info/kwarc/mmt/lsp/Server.scala b/src/mmt-lsp/src/info/kwarc/mmt/lsp/Server.scala
@@ -17,6 +17,8 @@ import java.util.logging.Logger
 import info.kwarc.mmt.api.frontend.{Controller, Extension}
 import info.kwarc.mmt.api.parser.SourceRef
 import info.kwarc.mmt.api.presentation.Presenter
+import info.kwarc.mmt.api.utils.{File, FileURI, URI}
+import info.kwarc.mmt.api.utils.File.read
 import info.kwarc.mmt.api.utils.time.Time
 import info.kwarc.mmt.api.web.ServerExtension
 import org.eclipse.jetty.server.{Server, ServerConnector}
@@ -422,12 +424,19 @@ class LSPServer[+ClientType <: LSPClient](clct : Class[ClientType]) {
 
 object LSPServer {
   def URItoVSCode(s : String) : String = URLEncoder.encode(s.replace("+","%2B"),"UTF-8")
-  def VSCodeToURI(s : String) : String = {
+  def VSCodeToURI(s: String): String = {
     val dec = URLDecoder.decode(s,"UTF-8")
-    if (dec.startsWith("file:///") && dec(9) == ':') {
+    if (dec.startsWith("file:///")) {
       dec.take(8) + dec(8).toUpper + dec.drop(9)
-    } else dec
-  }//s.replace("%3A",":")
+    } else {
+      dec
+    }
+  }
+
+  def VSCodeToFile(s: String): Option[File] = URI(VSCodeToURI(s)) match {
+    case FileURI(f) => Some(f)
+    case _ => None
+  }
 }
 
 class AbstractLSPServer[A <: LSPClient, B <: LSPServer[A], C <: LSPWebsocket[A,B]](val server : B,lsp:LSP[A,B,C])

diff --git a/src/mmt-lsp/src/info/kwarc/mmt/lsp/Utils.scala b/src/mmt-lsp/src/info/kwarc/mmt/lsp/Utils.scala
diff --git a/src/mmt-lsp/src/info/kwarc/mmt/lsp/mmt/Server.scala b/src/mmt-lsp/src/info/kwarc/mmt/lsp/mmt/Server.scala
@@ -69,9 +69,12 @@ class MMTLSPServer(style : RunStyle) extends LSPServer(classOf[MMTClient])
     })
 
     params.getWorkspaceFolders.asScala
-      .map(_.getUri)
-      .map(URI(_))
-      .map(Utils.vscodeURIToFile)
+      .flatMap(workspaceFolder => LSPServer.VSCodeToFile(workspaceFolder.getUri) match {
+        case Some(f) => Some(f)
+        case None =>
+          client.log(s"Could not parse `${workspaceFolder.getUri} as a file path on your operating system.")
+          None
+      })
       .foreach(workspacePath => {
         client.log(s"Registering `$workspacePath` as mathpath archive.")
         controller.addArchive(workspacePath)
@@ -92,12 +95,6 @@ class MMTLSPServer(style : RunStyle) extends LSPServer(classOf[MMTClient])
       })
   }
 
-  private object fg extends ReportHandler("lsp-frontend") {
-    override def apply(ind: Int, caller: => String, group: String, msgParts: List[String]): Unit = {
-      // TODO client.client.
-    }
-  }
-
   override val triggerChar: Char = 'j'
 
   val completionls = {

diff --git a/src/mmt-stex/src/info/kwarc/mmt/stex/lsp/Server.scala b/src/mmt-stex/src/info/kwarc/mmt/stex/lsp/Server.scala
@@ -597,9 +597,8 @@ class STeXLSPServer(style:RunStyle) extends LSPServer(classOf[STeXClient]) with
      result.getCapabilities.setWorkspaceSymbolProvider(true)
      if (params.getWorkspaceFolders != null) {
        params.getWorkspaceFolders.asScala
-         .map(_.getUri)
-         .map(URI(_))
-         .map(info.kwarc.mmt.lsp.Utils.vscodeURIToFile).foreach {
+         .flatMap(workspaceFolder => LSPServer.VSCodeToFile(workspaceFolder.getUri))
+         .foreach {
            case f if f.exists() => workspacefolders ::= f
          }
      }