From 305377c37207d48bb4357fdd46aea32dc809a5a8 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 25 Oct 2023 16:59:50 +0200 Subject: [PATCH] [workspace] [windows] Tolerate better Windows paths with mixed path separators. This needs a more principled approach, but should fix the most immediate Windows problems. Fixes #569 --- CHANGES.md | 2 ++ controller/lsp_core.ml | 12 +++++++++++- 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/CHANGES.md b/CHANGES.md index 895093d4..bf600b79 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -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 ----------------------------- diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml index 6770bd04..0b9f1d30 100644 --- a/controller/lsp_core.ml +++ b/controller/lsp_core.ml @@ -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