[hover] Show input help for Unicode characters

CHANGES.md

@@ -19,6 +19,8 @@
    #754)
  - [vscode] Fix focus race when a Coq file is in column 2 (@ejgallego,
    #755, cc: #722, #725)
+ - [hover] Show input howto for unicode characters on hover
+   (@ejgallego, Léo Stefanesco, #756)
 
 # coq-lsp 0.1.10: Hasta el 40 de Mayo _en effect_...
 ----------------------------------------------------

controller/rq_common.ml

@@ -55,22 +55,41 @@ let validate_line ~(contents : Fleche.Contents.t) ~line =
     Some (Array.get contents.lines line)
   else None
 
-let validate_column char line =
+let validate_column ~get char line =
   let length = Lang.Utf.length_utf16 line in
   if char < length then
     let char = Lang.Utf.utf8_offset_of_utf16_offset ~line ~offset:char in
-    Some (String.get line char)
+    get line char
   else None
 
 (* This returns a byte-based char offset for the line *)
-let validate_position ~contents ~point =
+let validate_position ~get ~contents ~point =
   let line, char = point in
-  validate_line ~contents ~line |> fun l -> Option.bind l (validate_column char)
+  validate_line ~contents ~line |> fun l ->
+  Option.bind l (validate_column ~get char)
 
-let get_char_at_point ~contents ~point =
-  let line, char = point in
-  if char >= 1 then
-    let point = (line, char - 1) in
-    validate_position ~contents ~point
-  else (* Can't get previous char *)
-    None
+let get_char_at_point_gen ~prev ~get ~contents ~point =
+  if prev then
+    let line, char = point in
+    if char >= 1 then
+      let point = (line, char - 1) in
+      validate_position ~get ~contents ~point
+    else (* Can't get previous char *)
+      None
+  else validate_position ~get ~contents ~point
+
+let get_char_at_point ~prev ~contents ~point =
+  let get line utf8_offset = Some (String.get line utf8_offset) in
+  get_char_at_point_gen ~prev ~get ~contents ~point
+
+let get_uchar_at_point ~prev ~contents ~point =
+  let get line utf8_offset =
+    let decode = String.get_utf_8_uchar line utf8_offset in
+    Fleche.Io.Log.trace "get_uchar_at_point"
+      ("utf8_offset is: " ^ string_of_int utf8_offset);
+    if Uchar.utf_decode_is_valid decode then
+      let str = String.sub line utf8_offset (Uchar.utf_decode_length decode) in
+      Some (Uchar.utf_decode_uchar decode, str)
+    else None
+  in
+  get_char_at_point_gen ~prev ~get ~contents ~point

controller/rq_common.mli

@@ -12,4 +12,11 @@ val get_id_at_point :
   contents:Fleche.Contents.t -> point:int * int -> string option
 
 val get_char_at_point :
-  contents:Fleche.Contents.t -> point:int * int -> char option
+  prev:bool -> contents:Fleche.Contents.t -> point:int * int -> char option
+
+(* Get both the uchar and its utf-8 string representation *)
+val get_uchar_at_point :
+     prev:bool
+  -> contents:Fleche.Contents.t
+  -> point:int * int
+  -> (Uchar.t * string) option

controller/rq_completion.ml

@@ -74,7 +74,7 @@ let completion ~token:_ ~(doc : Fleche.Doc.t) ~point =
   (* Instead of get_char_at_point we should have a CompletionContext.t, to be
      addressed in further completion PRs *)
   let contents = doc.contents in
-  (match Rq_common.get_char_at_point ~contents ~point with
+  (match Rq_common.get_char_at_point ~prev:true ~contents ~point with
   | None ->
     let incomplete = true in
     let items = [] in

controller/rq_hover.ml

@@ -223,6 +223,27 @@ module Notation : HoverProvider = struct
   let h = Handler.WithNode info_notation
 end
 
+module InputHelp : HoverProvider = struct
+  let mk_map map =
+    List.fold_left
+      (fun m (tex, uni) -> CString.Map.add uni tex m)
+      CString.Map.empty map
+
+  (* XXX: Fix to use extended map? *)
+  let unimap = mk_map Unicode_bindings.normal
+
+  let input_help ~token:_ ~contents ~point ~node:_ =
+    (* check if contents at point match *)
+    match Rq_common.get_uchar_at_point ~prev:false ~contents ~point with
+    | Some (uchar, uchar_str) when Uchar.utf_8_byte_length uchar > 1 ->
+      Option.map
+        (fun tex -> Format.asprintf "Input %s with %s" uchar_str tex)
+        (CString.Map.find_opt uchar_str unimap)
+    | Some _ | None -> None
+
+  let h = Handler.MaybeNode input_help
+end
+
 module Register = struct
   let handlers : Handler.t list ref = ref []
   let add fn = handlers := fn :: !handlers
@@ -240,7 +261,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 () =
+  List.iter Register.add
+    [ Loc_info.h; Stats.h; Type.h; Notation.h; InputHelp.h ]
 
 let hover ~token ~(doc : Fleche.Doc.t) ~point =
   let node = Info.LC.node ~doc ~point Exact in