[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,39 @@ 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
+    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

@@ -60,21 +60,15 @@ let mk_unicode_completion_item point (label, newText) =
   mk_completion ~label ~labelDetails ~textEdit ~commitCharacters ()
 
 let unicode_list point : Yojson.Safe.t list =
-  let ulist =
-    match !Fleche.Config.v.unicode_completion with
-    | Off -> []
-    | Internal_small -> Unicode_bindings.small
-    | Normal -> Unicode_bindings.normal
-    | Extended -> Unicode_bindings.extended
-  in
+  let ulist = Unicode_bindings.from_config () in
   (* Coq's CList.map is tail-recursive *)
   CList.map (mk_unicode_completion_item point) ulist
 
 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,29 @@ 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
+
+  (* A bit hackish, but OK *)
+  let unimap =
+    Lazy.from_fun (fun () ->
+        mk_map (Unicode_bindings.from_config ()))
+
+  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 (Lazy.force 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 +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 () =
+  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

controller/unicode_bindings.ml

@@ -1697,3 +1697,10 @@ let extended =
   ; ("\\_v", "ᵥ")
   ; ("\\_x", "ₓ")
   ]
+
+let from_config () =
+  match !Fleche.Config.v.unicode_completion with
+  | Off -> []
+  | Internal_small -> small
+  | Normal -> normal
+  | Extended -> extended

controller/unicode_bindings.mli

@@ -9,3 +9,6 @@ val normal : (string * string) list
 
 (** All the supported bindings for unicode characters in a table. *)
 val extended : (string * string) list
+
+(** Return the list selected in config *)
+val from_config : unit -> (string * string) list