diff --git a/CHANGES.md b/CHANGES.md index 18a68010b..002ba362c 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 2a1627afe..65babf2a5 100644 --- a/controller/rq_common.ml +++ b/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 diff --git a/controller/rq_common.mli b/controller/rq_common.mli index a7f7bf68a..75ac2447e 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 62a8519e4..fc3a6306f 100644 --- a/controller/rq_completion.ml +++ b/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 diff --git a/controller/rq_hover.ml b/controller/rq_hover.ml index c69849ad7..ea758c519 100644 --- a/controller/rq_hover.ml +++ b/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