diff --git a/flake.lock b/flake.lock index af0da5259..84e9bc756 100644 --- a/flake.lock +++ b/flake.lock @@ -8,17 +8,17 @@ ] }, "locked": { - "lastModified": 1731955962, - "narHash": "sha256-CXImBSYiB0D4CNpPx4EFkQcypf+5ylb7BRf3MBjvt30=", - "owner": "coq", + "lastModified": 1732642450, + "narHash": "sha256-XiE7gL8/myxrvHnhyueyyQq6H5v/XGHKZX8cupf8L0A=", + "owner": "rtetley", "repo": "coq", - "rev": "668dc3ca9735a2b008f5ce52c14969af59cc24e1", + "rev": "d6dd8a618cbf628a6580c9a42db0cf5f44606bea", "type": "github" }, "original": { - "owner": "coq", + "owner": "rtetley", "repo": "coq", - "rev": "668dc3ca9735a2b008f5ce52c14969af59cc24e1", + "rev": "d6dd8a618cbf628a6580c9a42db0cf5f44606bea", "type": "github" } }, diff --git a/flake.nix b/flake.nix index 2769b9b06..5ebf9a9c2 100644 --- a/flake.nix +++ b/flake.nix @@ -4,7 +4,7 @@ inputs = { flake-utils.url = "github:numtide/flake-utils"; - coq-master = { url = "github:coq/coq/668dc3ca9735a2b008f5ce52c14969af59cc24e1"; }; # Should be kept in sync with PIN_COQ in CI workflow + coq-master = { url = "github:coq/coq/d6dd8a618cbf628a6580c9a42db0cf5f44606bea"; }; # Should be kept in sync with PIN_COQ in CI workflow coq-master.inputs.nixpkgs.follows = "nixpkgs"; }; diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index 4ef800266..bf777dbce 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -749,6 +749,48 @@ let hover st pos = let lconstr = Procq.Constr.lconstr [%%endif] + +[%%if coq = "8.18" || coq = "8.19" || coq = "8.20"] +let jump_to_definition _ _ = None +[%%else] +let jump_to_definition st pos = + let raw_doc = Document.raw_document st.document in + let loc = RawDocument.loc_of_position raw_doc pos in + let opattern = RawDocument.word_at_position raw_doc pos in + match opattern with + | None -> log "jumpToDef: no word found at cursor"; None + | Some pattern -> + log ("jumpToDef: found word at cursor: \"" ^ pattern ^ "\""); + try + let qid = parse_entry st loc (Procq.Prim.qualid) pattern in + let ref = Nametab.locate_extended qid in + match Nametab.cci_src_loc ref with + | None -> None + | Some loc -> + begin match loc.Loc.fname with + | Loc.ToplevelInput | InFile { dirpath = None } -> None + | InFile { dirpath = Some dp } -> + let f = Loadpath.locate_absolute_library @@ Libnames.dirpath_of_string dp in + begin match f with + | Ok f -> + let f = Filename.remove_extension f ^ ".v" in + (if Sys.file_exists f then + let b_pos = Position.create ~character:(loc.bp - loc.bol_pos) ~line:(loc.line_nb - 1) in + let e_pos = Position.create ~character:(loc.ep - loc.bol_pos) ~line:(loc.line_nb - 1) in + let range = Range.create ~end_:b_pos ~start:e_pos in + Some (range, f) + else + None + ) + | Error _ -> None + end + end + with e -> + let e, info = Exninfo.capture e in + log (Pp.string_of_ppcmds @@ CErrors.iprint (e, info)); None + +[%%endif] + let check st pos ~pattern = let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in match get_context st pos with diff --git a/language-server/dm/documentManager.mli b/language-server/dm/documentManager.mli index c5ae1b77f..c5780b540 100644 --- a/language-server/dm/documentManager.mli +++ b/language-server/dm/documentManager.mli @@ -132,6 +132,8 @@ val hover : state -> Position.t -> MarkupContent.t option if None, the position did not have a word, if Some, an Ok/Error result is returned. *) +val jump_to_definition : state -> Position.t -> (Range.t * string) option + val check : state -> Position.t -> pattern:string -> (pp,error) Result.t val locate : state -> Position.t -> pattern:string -> (pp, error) Result.t diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml index d7b2c262d..a9047774a 100644 --- a/language-server/vscoqtop/lspManager.ml +++ b/language-server/vscoqtop/lspManager.ml @@ -153,10 +153,12 @@ let do_initialize id params = let completionProvider = CompletionOptions.create ~resolveProvider:false () in let documentSymbolProvider = `DocumentSymbolOptions (DocumentSymbolOptions.create ~workDoneProgress:true ()) in let hoverProvider = `Bool true in + let definitionProvider = `Bool true in let capabilities = ServerCapabilities.create ~textDocumentSync ~completionProvider ~hoverProvider + ~definitionProvider ~documentSymbolProvider () in @@ -367,7 +369,7 @@ let textDocumentDidClose params = let Lsp.Types.DidCloseTextDocumentParams.{ textDocument } = params in let path = DocumentUri.to_path textDocument.uri in begin match Hashtbl.find_opt states path with - | None -> assert false + | None -> log @@ "[textDocumentDidClose] closed document with no state" | Some { st } -> replace_state path st false end; consider_purge_invisible_tabs (); @@ -383,6 +385,19 @@ let textDocumentHover id params = | Some contents -> Ok (Some (Hover.create ~contents:(`MarkupContent contents) ())) | _ -> Ok None (* FIXME handle error case properly *) +let textDocumentDefinition params = + let Lsp.Types.DefinitionParams.{ textDocument; position } = params in + match Hashtbl.find_opt states (DocumentUri.to_path textDocument.uri) with + | None -> log @@ "[textDocumentDefinition] ignoring event on non existing document"; Ok None (* FIXME handle error case properly *) + | Some { st } -> + match Dm.DocumentManager.jump_to_definition st position with + | None -> log @@ "[textDocumentDefinition] could not find symbol location"; Ok None (* FIXME handle error case properly *) + | Some (range, uri) -> + let uri = DocumentUri.of_path uri in + let location = Location.create ~range:range ~uri:uri in + Ok (Some (`Location [location])) + + let progress_hook uri () = match Hashtbl.find_opt states (DocumentUri.to_path uri) with | None -> log @@ "ignoring non existent document" @@ -548,6 +563,8 @@ let dispatch_std_request : type a. Jsonrpc.Id.t -> a Lsp.Client_request.t -> (a, do_shutdown id () | TextDocumentCompletion params -> textDocumentCompletion id params + | TextDocumentDefinition params -> + textDocumentDefinition params, [] | TextDocumentHover params -> textDocumentHover id params, [] | DocumentSymbol params ->