diff --git a/CHANGES.md b/CHANGES.md index 18a68010..002ba362 100644 --- a/CHANGES.md +++ b/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_... ---------------------------------------------------- diff --git a/controller/rq_common.ml b/controller/rq_common.ml index 2a1627af..958a5a1f 100644 --- a/controller/rq_common.ml +++ b/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 diff --git a/controller/rq_common.mli b/controller/rq_common.mli index a7f7bf68..75ac2447 100644 --- a/controller/rq_common.mli +++ b/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 diff --git a/controller/rq_completion.ml b/controller/rq_completion.ml index 62a8519e..81b2a601 100644 --- a/controller/rq_completion.ml +++ b/controller/rq_completion.ml @@ -60,13 +60,7 @@ 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 @@ -74,7 +68,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 diff --git a/controller/rq_hover.ml b/controller/rq_hover.ml index c69849ad..3f41b1e5 100644 --- a/controller/rq_hover.ml +++ b/controller/rq_hover.ml @@ -223,6 +223,28 @@ 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 +262,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 diff --git a/controller/unicode_bindings.ml b/controller/unicode_bindings.ml index 77ac63d8..569cb9ee 100644 --- a/controller/unicode_bindings.ml +++ b/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 diff --git a/controller/unicode_bindings.mli b/controller/unicode_bindings.mli index b14b2f49..67d604fc 100644 --- a/controller/unicode_bindings.mli +++ b/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