Skip to content

Commit

Permalink
[hover] Add a simple plugin system.
Browse files Browse the repository at this point in the history
This allows users to extend hover in a well-typed way.
  • Loading branch information
ejgallego committed Oct 2, 2023
1 parent ea182d9 commit 3f6d76c
Show file tree
Hide file tree
Showing 3 changed files with 33 additions and 6 deletions.
1 change: 1 addition & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@
- Provide basic notation information on hover. This is intended for
people to build their own more refined notation feedback systems
(@ejgallego, #)
- Hover request can now be extended by plugins (@ejgallego, #)

# coq-lsp 0.1.7: Just-in-time
-----------------------------
Expand Down
21 changes: 15 additions & 6 deletions controller/rq_hover.ml
Original file line number Diff line number Diff line change
Expand Up @@ -204,18 +204,27 @@ module Notation : HoverProvider = struct
let h = Handler.WithNode info_notation
end

let handlers : Handler.t list = [ Loc_info.h; Stats.h; Type.h; Notation.h ]
module Register = struct
let handlers : Handler.t list ref = ref []
let add fn = handlers := fn :: !handlers

let handle_hover ~contents ~point ~node = function
| Handler.MaybeNode h -> h ~contents ~point ~node
| Handler.WithNode h ->
Option.bind node (fun node -> h ~contents ~point ~node)
let handle ~contents ~point ~node = function
| Handler.MaybeNode h -> h ~contents ~point ~node
| Handler.WithNode h ->
Option.bind node (fun node -> h ~contents ~point ~node)

let fire ~contents ~point ~node =
List.filter_map (handle ~contents ~point ~node) !handlers
end

(* Register in-file hover plugins *)
let () = List.iter Register.add [ Loc_info.h; Stats.h; Type.h; Notation.h ]

let hover ~doc ~point =
let contents = doc.Doc.contents in
let node = Info.LC.node ~doc ~point Exact in
let range = Option.map Doc.Node.range node in
let hovers = List.filter_map (handle_hover ~contents ~point ~node) handlers in
let hovers = Register.fire ~contents ~point ~node in
match hovers with
| [] -> `Null
| hovers ->
Expand Down
17 changes: 17 additions & 0 deletions controller/rq_hover.mli
Original file line number Diff line number Diff line change
Expand Up @@ -6,3 +6,20 @@
(************************************************************************)

val hover : Request.position

open Fleche

module Handler : sig
(** Returns [Some markdown] if there is some hover to match *)
type 'node h =
contents:Contents.t -> point:int * int -> node:'node -> string option

type t =
| MaybeNode : Doc.Node.t option h -> t
| WithNode : Doc.Node.t h -> t
end

(** Register a hover plugin *)
module Register : sig
val add : Handler.t -> unit
end

0 comments on commit 3f6d76c

Please sign in to comment.