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.

Sign up for GitHub

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

[definition] Try to also recognize module names. #764

Merged
merged 1 commit into from
Jun 6, 2024
+28 −6
Merged

[definition] Try to also recognize module names. #764

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
9 changes: 6 additions & 3 deletions CHANGES.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,9 +10,10 @@
heuristic is enabled (@ejgallego, #748)
- [memo] More precise hashing for Coq states, this improves cache
performance quite a bit (@ejgallego, #751)
- [fleche] This achieves an almost 50% memory reduction for example
when opening all of HoTT .v files (@ejgallego, @SkySkimmer,
@bhaktishh, #744)
- [fleche] Enable sharing of `.vo` file parsing. This enables better
sharing, achieving an almost 50% memory reduction for example when
opening all of HoTT .v files (@ejgallego, @SkySkimmer, @bhaktishh,
#744)
- [memo] Provide API to query Hashtbl stats (@ejgallego, #753)
- [nix] Add `pet-server` deps to flake.nix (Léo Stefanesco, #754)
- [coq-lsp] Fix crash on `--help` option (Léo Stefanesco, @ejgallego,
Expand All @@ -26,6 +27,8 @@
it is often not perfect. (@ejgallego, #762, fixes #317)
- [lsp] [hover] Show full name and provenance of identifiers
(@ejgallego, #762)
- [lsp] [definition] Try also to resolve and locate module imports
(@ejgallego, #764)

# coq-lsp 0.1.10: Hasta el 40 de Mayo _en effect_...
----------------------------------------------------
Expand Down
25 changes: 22 additions & 3 deletions controller/rq_definition.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,8 +54,27 @@ let get_from_file id_at_point =
Fleche.Io.Log.trace "rq_definition" "No TrueGlobal Found";
Ok None

let get_from_file ~token ~st id_at_point =
let f = get_from_file in
let get_from_import require_at_point =
match Loadpath.locate_qualified_library require_at_point with
| Ok (dp, _file) -> (
match Rq_common.CoqModule.make dp with
| Error _err -> None
| Ok mod_ ->
let uri = Rq_common.CoqModule.uri mod_ in
let start = Lang.Point.{ line = 0; character = 0; offset = 0 } in
let range = Lang.Range.{ start; end_ = start } in
Some Lsp.Core.Location.{ uri; range })
| Error _ -> None

let get_from_file_or_import ~token ~st id_at_point =
let f id =
match get_from_file id with
| Error err -> Error err
| Ok (Some res) -> Ok (Some res)
| Ok None ->
let qualid = Libnames.qualid_of_string id_at_point in
Ok (get_from_import qualid)
in
Coq.State.in_state ~token ~st ~f id_at_point

let request ~token ~(doc : Fleche.Doc.t) ~point =
Expand All @@ -72,7 +91,7 @@ let request ~token ~(doc : Fleche.Doc.t) ~point =
|> Option.cata
(fun node ->
let st = Fleche.Doc.Node.state node in
get_from_file ~token ~st idp)
get_from_file_or_import ~token ~st idp)
(ok None))
(ok None) idp
|> Coq.Protect.E.map
Expand Down
Loading