[hover] Show documentation on identifier hover.

This is a first, simple prototype, mainly to showcase.

CHANGES.md

@@ -1,11 +1,11 @@
 # unreleased
 -----------
 
- - new option `show_loc_info_on_hover` that will display parsing debug
+ - New option `show_loc_info_on_hover` that will display parsing debug
    information on hover; previous flag was fixed in code, which is way
    less flexible. This also fixes the option being on in 0.1.8 by
    mistake (@ejgallego, #588)
- - hover plugins can now access the full document, this is convenient
+ - Hover plugins can now access the full document, this is convenient
    for many use cases (@ejgallego, #591)
  - fix hover position computation on the presence of Utf characters
    (@ejgallego, #597, thanks to Pierre Courtieu for the report and
@@ -41,6 +41,9 @@
  - don't trigger the goals window in general markdown buffer
    (@ejgallego, #625, reported by Théo Zimmerman)
  - allow not to postpone full document requests (#626, @ejgallego)
+ - Hover will now show coqdoc documentation of identifiers, using some
+   heuristics to infer it from the comments. Documentation is treated
+   as Markdown, this may change in the future. (@ejgallego, #590)
 
 # coq-lsp 0.1.8: Trick-or-treat
 -------------------------------

controller/rq_hover.ml

@@ -210,6 +210,42 @@ module Notation : HoverProvider = struct
   let h = Handler.WithNode info_notation
 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) { Lang.Range.start; _ } =
+    let { Lang.Point.line; _ } = start in
+    let lines = contents.lines in
+    Option.map (extract lines line) (guess_start_line lines line)
+
+  let h ~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* range = CString.Map.find_opt id_at_point toc in
+    process ~contents range
+
+  let h = Handler.WithDoc h
+end
+
 module Register = struct
   let handlers : Handler.t list ref = ref []
   let add fn = handlers := fn :: !handlers
@@ -227,7 +263,9 @@ module Register = struct
 end
 
 (* Register in-file hover plugins *)
-let () = List.iter Register.add [ Loc_info.h; Stats.h; Type.h; Notation.h ]
+let () =
+  [ Loc_info.h; Documentation.h; Type.h; Notation.h; Stats.h ]
+  |> List.iter Register.add
 
 let hover ~doc ~point =
   let node = Info.LC.node ~doc ~point Exact in

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.