From 603435df2c69423b6b2e125dcb26963a329a9706 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Thu, 26 Oct 2023 01:57:29 +0200
Subject: [PATCH] [hover] Show documentation on identifier hover.

This is a first, simple prototype, mainly to showcase.
---
 CHANGES.md             |  5 +++++
 controller/rq_hover.ml | 49 ++++++++++++++++++++++++++++++++++++++++--
 examples/doc_hover.v   | 29 +++++++++++++++++++++++++
 3 files changed, 81 insertions(+), 2 deletions(-)
 create mode 100644 examples/doc_hover.v

diff --git a/CHANGES.md b/CHANGES.md
index a225207f..32840083 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -23,6 +23,11 @@
    provides a full working Coq enviroment in `vscode.dev`. The web
    worker version is build as an artifact on CI (@ejgallego
    @corwin-of-amber, #433)
+ - [hover] When the `show_doc_on_hover` option is enabled, hover will
+   show coqdoc documentation when hovering on identifiers, using some
+   heuristics to infer it from the comment just before
+   it. Documentation is treated as Markdown. This feature is
+   experimental and may change in the future. (@ejgallego, #590)
 
 # coq-lsp 0.2.0: From Green to Blue
 -----------------------------------
diff --git a/controller/rq_hover.ml b/controller/rq_hover.ml
index 903bfc56..31ef5f08 100644
--- a/controller/rq_hover.ml
+++ b/controller/rq_hover.ml
@@ -288,6 +288,44 @@ module UniDiff = struct
   let h = Handler.WithNode h
 end
 
+module Documentation : HoverProvider = struct
+  let extract s =
+    let r = Str.regexp ({|(\*\*?[ ]*\(\(.\||} ^ "\n" ^ {|\)*\)[ ]*\*)|}) in
+    (* "**[Docstring]**: \n" ^ *)
+    Str.replace_first r {|\1|} s
+
+  let extract lines line num =
+    let ll = List.init num (fun idx -> lines.(line - (num - idx))) in
+    String.concat "\n" ll |> extract
+
+  (* TODO: Stop when in node *)
+  let guess_start_line lines line =
+    let limit = 20 in
+    let rec back cur =
+      if cur > limit then None
+      else if CString.is_prefix "(*" lines.(line - cur) then Some cur
+      else back (cur + 1)
+    in
+    back 1
+
+  let process ~(contents : Contents.t) prev { Lang.Range.start; _ } =
+    (* XXX: Fix to use prev instead of the current hack *)
+    let _end_ = prev in
+    let { Lang.Point.line; _ } = start in
+    let lines = contents.lines in
+    Option.map (extract lines line) (guess_start_line lines line)
+
+  let h ~token:_ ~doc ~point ~node:_ =
+    let ( let* ) = Option.bind in
+
+    let { Fleche.Doc.toc; contents; _ } = doc in
+    let* id_at_point = Rq_common.get_id_at_point ~contents ~point in
+    let* node = CString.Map.find_opt id_at_point toc in
+    process ~contents node.prev node.range
+
+  let h = Handler.WithDoc h
+end
+
 module Register = struct
   let handlers : Handler.t list ref = ref []
   let add fn = handlers := fn :: !handlers
@@ -306,8 +344,15 @@ end
 
 (* Register in-file hover plugins *)
 let () =
-  List.iter Register.add
-    [ Loc_info.h; Stats.h; Type.h; Notation.h; InputHelp.h; UniDiff.h ]
+  [ Loc_info.h
+  ; Documentation.h
+  ; Stats.h
+  ; Type.h
+  ; Notation.h
+  ; InputHelp.h
+  ; UniDiff.h
+  ]
+  |> List.iter Register.add
 
 let hover ~token ~(doc : Fleche.Doc.t) ~point =
   let node = Info.LC.node ~doc ~point Exact in
diff --git a/examples/doc_hover.v b/examples/doc_hover.v
new file mode 100644
index 00000000..659eb916
--- /dev/null
+++ b/examples/doc_hover.v
@@ -0,0 +1,29 @@
+From Coq Require Import List.
+Import ListNotations.
+
+(* asdf *)
+Definition hello := 3.
+
+(** `my_map` a reimplementation of `map`
+
+ - this is cool
+ - really
+ 
+ a source code example. 
+ 
+ ```coq
+ Definition my_map bar := 3.
+ ```
+ Pretty _nice_ :D
+*)
+Fixpoint my_map {A B} (f : A -> B) (l : list A) : list B :=
+  match l with
+    | [] => []
+    | (x :: xs) => (f x :: my_map f xs)
+  end.
+
+(** I'm going to use `my_map` *)
+Definition my_map_alias := @my_map.
+
+About my_map_alias.
+About hello.