From 3f6d76c7c01d64886de3aff7fc78e5e8fa35725b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 2 Oct 2023 03:43:16 +0200
Subject: [PATCH] [hover] Add a simple plugin system.

This allows users to extend hover in a well-typed way.
---
 CHANGES.md              |  1 +
 controller/rq_hover.ml  | 21 +++++++++++++++------
 controller/rq_hover.mli | 17 +++++++++++++++++
 3 files changed, 33 insertions(+), 6 deletions(-)

diff --git a/CHANGES.md b/CHANGES.md
index 12e9817d5..512b78ebf 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -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
 -----------------------------
diff --git a/controller/rq_hover.ml b/controller/rq_hover.ml
index 86f4414cf..c59d37156 100644
--- a/controller/rq_hover.ml
+++ b/controller/rq_hover.ml
@@ -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 ->
diff --git a/controller/rq_hover.mli b/controller/rq_hover.mli
index 6a2cecb5a..7228fac7d 100644
--- a/controller/rq_hover.mli
+++ b/controller/rq_hover.mli
@@ -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