diff --git a/CHANGES.md b/CHANGES.md index dbac0004c..de2a47428 100644 --- a/CHANGES.md +++ b/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 ----------------------------- diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml index 3980c0ef9..f09f166ef 100644 --- a/controller/lsp_core.ml +++ b/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