fix: go-to-def paths on Windows

src/Init/System/FilePath.lean

@@ -19,16 +19,12 @@ def pathSeparator : Char :=
 def pathSeparators : List Char :=
   if isWindows then ['\\', '/'] else ['/']
 
-/-- The character that is used to separate the entries in the $PATH environment variable. -/
+/-- The character that is used to separate the entries in the $PATH (or %PATH%) environment variable. -/
 def searchPathSeparator : Char :=
   if isWindows then ';' else ':'
 
-/-- The list of all possible separators. -/
-def searchPathSeparators : List Char :=
-  if isWindows then [';', ':'] else [':']
-
 def splitSearchPath (s : String) : List String :=
-  s.split (fun c => searchPathSeparators.elem c)
+  s.split (fun c => searchPathSeparator == c)
 
 /-- File extension character -/
 def extSeparator : Char := '.'

src/Lean/Server/FileWorker.lean

@@ -195,7 +195,11 @@ section Initialization
                                    srcPath.mapM realPathNormalized
       | _                       => throw <| IO.userError s!"unexpected output from `leanpkg print-paths`:\n{stdout}\nstderr:\n{stderr}"
     else
-      throw <| IO.userError s!"`leanpkg print-paths` failed:\n{stdout}\nstderr:\n{stderr}"
+      -- HACK(WN): `leanpkg` currently runs in the current directory, most likely the directory where the editor
+      -- was ran, which can lead to unexpected failures. We need to support workspace folders and execute it there.
+      -- For now though, just log the failure and press onwards.
+      IO.eprintln s!"`leanpkg print-paths` failed:\n{stdout}\nstderr:\n{stderr}"
+      return []
 
   def compileHeader (m : DocumentMeta) (hOut : FS.Stream) : IO (Snapshot × SearchPath) := do
     let opts := {}  -- TODO
@@ -411,7 +415,7 @@ section RequestHandling
               let modUri? ← match mod? with
                 | some modName =>
                   let modFname? ← st.srcSearchPath.findWithExt ".lean" modName
-                  pure <| modFname?.map ("file://" ++ ·)
+                  pure <| modFname?.map toFileUri
                 | none         => pure <| some doc.meta.uri
 
               let ranges? ← ci.runMetaM i.lctx <| findDeclarationRanges? n

src/Lean/Server/Utils.lean

@@ -6,6 +6,7 @@ Authors: Wojciech Nawrocki, Marc Huisinga
 -/
 import Lean.Data.Position
 import Lean.Data.Lsp
+import Init.System.FilePath
 
 namespace IO
 
@@ -89,6 +90,17 @@ def maybeTee (fName : String) (isOut : Bool) (h : FS.Stream) : IO FS.Stream := d
     else
       h.chainRight hTee true
 
+/-- Transform the given path to a file:// URI. -/
+def toFileUri (fname : String) : Lsp.DocumentUri :=
+  let fname := System.FilePath.normalizePath fname
+  let fname := if System.Platform.isWindows then
+    fname.map fun c => if c == '\\' then '/' else c
+  else
+    fname
+  -- TODO(WN): URL-encode special characters
+  -- Three slashes denote localhost.
+  "file:///" ++ fname.dropWhile (· == '/')
+
 open Lsp
 
 /-- Returns the document contents with all changes applied, together with the position of the change