Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[workspace] [windows] Tolerate better Windows paths with mixed path separators #583

Merged
merged 1 commit into from
Oct 25, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,8 @@
implementation is partial: we only take into account the first
position, and we only return a single range (Coq sentence) without
parents. (@ejgallego, #582)
- Be more robust to mixed-separator windows paths in workspace
detection (@ejgallego, #583, fixes #569)

# coq-lsp 0.1.7: Just-in-time
-----------------------------
Expand Down
12 changes: 11 additions & 1 deletion controller/lsp_core.ml
Original file line number Diff line number Diff line change
Expand Up @@ -115,7 +115,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
Expand Down
Loading