[hover] Show documentation on identifier hover.

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

CHANGES.md

@@ -19,6 +19,11 @@
    #754)
  - [vscode] Fix focus race when a Coq file is in column 2 (@ejgallego,
    #755, cc: #722, #725)
+ - [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.1.10: Hasta el 40 de Mayo _en effect_...
 ----------------------------------------------------

controller/rq_hover.ml

@@ -223,6 +223,44 @@ 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) 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
@@ -240,7 +278,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 ~token ~(doc : Fleche.Doc.t) ~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.