diff --git a/CHANGES.md b/CHANGES.md index 37fe7786c..99b647c73 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -26,6 +26,8 @@ resumption, still cached sentences will display the cached timing tho (@ejgallego, #257) - Set Coq library name correctly (@ejgallego, #260) + - `_CoqProject` file is now detected using LSP client `rootPath` + (@ejgallego, #261) # coq-lsp 0.1.3: Event ---------------------- diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index 020895d1f..4aa10dd33 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -282,7 +282,8 @@ let rec lsp_init_loop ic ofmt ~cmdline ~debug : Coq.Workspace.t = LIO.logMessage ~lvl:3 ~message:"Server initialized"; (* Workspace initialization *) let debug = debug || !Fleche.Config.v.debug in - let workspace = Coq.Workspace.guess ~cmdline ~debug in + let dir = string_field "rootPath" params in + let workspace = Coq.Workspace.guess ~cmdline ~debug ~dir in log_workspace workspace; workspace | LSP.Message.Request { id; _ } -> diff --git a/coq/workspace.ml b/coq/workspace.ml index 5b8777930..18ed989b5 100644 --- a/coq/workspace.ml +++ b/coq/workspace.ml @@ -157,7 +157,7 @@ let apply ~uri Declaremods.start_library (dirpath_of_uri ~uri); load_objs require_libs -let workspace_from_coqproject ~coqlib ~debug : t = +let workspace_from_coqproject ~coqlib ~debug cp_file : t = (* Io.Log.error "init" "Parsing _CoqProject"; *) let open CoqProject_file in let to_vo_loadpath f implicit = @@ -173,7 +173,7 @@ let workspace_from_coqproject ~coqlib ~debug : t = } in let { r_includes; q_includes; ml_includes; extra_args; _ } = - read_project_file ~warning_fn:(fun _ -> ()) "_CoqProject" + read_project_file ~warning_fn:(fun _ -> ()) cp_file in let ml_include_path = List.map (fun f -> f.thing.path) ml_includes in let vo_path = List.map (fun f -> to_vo_loadpath f.thing false) q_includes in @@ -206,7 +206,8 @@ let workspace_from_cmdline ~debug let w = default ~implicit ~coqlib ~kind ~debug in add_loadpaths w ~vo_load_path ~ml_include_path -let guess ~debug ~cmdline = - if Sys.file_exists "_CoqProject" then - workspace_from_coqproject ~coqlib:cmdline.CmdLine.coqlib ~debug +let guess ~debug ~cmdline ~dir = + let cp_file = Filename.concat dir "_CoqProject" in + if Sys.file_exists cp_file then + workspace_from_coqproject ~coqlib:cmdline.CmdLine.coqlib ~debug cp_file else workspace_from_cmdline ~debug cmdline diff --git a/coq/workspace.mli b/coq/workspace.mli index d8e9b12d3..f27ce4b54 100644 --- a/coq/workspace.mli +++ b/coq/workspace.mli @@ -38,7 +38,7 @@ module CmdLine : sig } end -val guess : debug:bool -> cmdline:CmdLine.t -> t +val guess : debug:bool -> cmdline:CmdLine.t -> dir:string -> t (** [apply libname w] will prepare Coq for a new file [libname] on workspace [w] *) val apply : uri:string -> t -> unit