[workspace] [windows] Tolerate better Windows paths with mixed path s…

…eparators.

This needs a more principled approach, but should fix the most
immediate Windows problems.

Fixes #569

CHANGES.md

@@ -48,6 +48,8 @@
  - New `pretac` field for preprocessing of goals with a tactic using
    speculative execution, this is experimental for now (@amblafont,
    @ejgallego, #573, helps with #558)
+ - Be more robust to mixed-separator windows paths in workspace
+   detection (@ejgallego, #583, fixes #569)
 
 # coq-lsp 0.1.7: Just-in-time
 -----------------------------

controller/lsp_core.ml

@@ -108,7 +108,17 @@ module State = struct
     let dir = Lang.LUri.File.to_string_file uri in
     { state with workspaces = List.remove_assoc dir state.workspaces }
 
-  let is_in_dir ~dir ~file = CString.is_prefix dir file
+  let split_in_components path =
+    let phase1 = String.split_on_char '/' path in
+    let phase2 = List.map (String.split_on_char '\\') phase1 in
+    List.concat phase2
+
+  (* This is a bit more tricky in Windows, due to \ vs / paths appearing, so we
+     need to first split the dir *)
+  let is_in_dir ~dir ~file =
+    let dir_c = split_in_components dir in
+    let file_c = split_in_components file in
+    CList.prefix_of String.equal dir_c file_c
 
   let workspace_of_uri ~uri ~state =
     let { root_state; workspaces; _ } = state in