From f9689acda53fbf4700364506ac1746c42b957877 Mon Sep 17 00:00:00 2001 From: Alidra <40537601+Alidra@users.noreply.github.com> Date: Fri, 5 Apr 2024 10:47:19 +0200 Subject: [PATCH] Fix/logs when missing pkg (#1075) * fix #1069 * fix/logs : catch exception in new_doc when lambdapi.pkg is missing. Change lp_doc.t * modify lp_lsp to handle Fatal error * update CHANGES.md --- src/lsp/CHANGES.md | 2 + src/lsp/lp_doc.ml | 42 ++++++++--- src/lsp/lp_lsp.ml | 184 ++++++++++++++++++++++++++------------------- 3 files changed, 138 insertions(+), 90 deletions(-) diff --git a/src/lsp/CHANGES.md b/src/lsp/CHANGES.md index 28fa523bd..5e8f6510b 100644 --- a/src/lsp/CHANGES.md +++ b/src/lsp/CHANGES.md @@ -3,6 +3,8 @@ - First standalone release; code is the same, but we don't build a lambdapi package anymore. +- Logs : show an error message in Debug terminal if + the lambdapi.pkg is missing 0.0.8.7 ------- diff --git a/src/lsp/lp_doc.ml b/src/lsp/lp_doc.ml index 9418bda57..48d437f6e 100644 --- a/src/lsp/lp_doc.ml +++ b/src/lsp/lp_doc.ml @@ -35,8 +35,8 @@ type t = { uri : string; version: int; text : string; - mutable root : Pure.state; (* Only mutated after parsing. *) - mutable final : Pure.state; (* Only mutated after parsing. *) + mutable root : Pure.state option; (* Only mutated after parsing. *) + mutable final : Pure.state option; (* Only mutated after parsing. *) nodes : doc_node list; (* severity is same as LSP specifications : https://git.io/JiGAB *) logs : ((int * string) * Pos.popt) list; (*((severity, message), location)*) @@ -123,11 +123,22 @@ let process_cmd _file (nodes,st,dg,logs) ast = nodes, st, (loc, 1, msg, None) :: dg, ((1, msg), loc) :: logs let new_doc ~uri ~version ~text = - let root = - (* We remove the ["file://"] prefix. *) - assert(String.is_prefix "file://" uri); - let path = String.sub uri 7 (String.length uri - 7) in - Pure.initial_state path + let root, logs = + try + (* We remove the ["file://"] prefix. *) + assert(String.is_prefix "file://" uri); + let path = String.sub uri 7 (String.length uri - 7) in + Some(Pure.initial_state path), [] + with Error.Fatal(_pos, msg) -> + let loc : Pos.pos = + { + fname = Some(uri); + start_line = 0; + start_col = 0; + end_line = 0; + end_col = 0 + } in + (None, [(1, msg), Some(loc)]) in { uri; text; @@ -135,7 +146,7 @@ let new_doc ~uri ~version ~text = root; final = root; nodes = []; - logs = []; + logs = logs; map = RangeMap.empty; } @@ -153,20 +164,27 @@ let dummy_loc = let check_text ~doc = let uri, version = doc.uri, doc.version in + let root = + match doc.root with + | Some(ss) -> ss + | None -> + raise(Error.fatal_no_pos "Root state is missing + probably because new_doc has raised exception") + in try let cmds = - let (cmds, root) = Pure.parse_text doc.root ~fname:uri doc.text in + let (cmds, root) = Pure.parse_text root ~fname:uri doc.text in (* One shot state update after parsing. *) - doc.root <- root; doc.final <- root; cmds + doc.root <- Some(root); doc.final <- Some(root); cmds in (* compute rangemap *) let map = Pure.rangemap cmds in let nodes, final, diag, logs = - List.fold_left (process_cmd uri) ([],doc.root,[],[]) cmds in + List.fold_left (process_cmd uri) ([],root,[],[]) cmds in let logs = List.rev logs in - let doc = { doc with nodes; final; map; logs } in + let doc = { doc with nodes; final=Some(final); map; logs } in doc, LSP.mk_diagnostics ~uri ~version @@ List.fold_left (fun acc (pos,lvl,msg,goal) -> diff --git a/src/lsp/lp_lsp.ml b/src/lsp/lp_lsp.ml index 2a474de5b..7023d40f2 100644 --- a/src/lsp/lp_lsp.ml +++ b/src/lsp/lp_lsp.ml @@ -55,7 +55,20 @@ let completed_table : (string, Lp_doc.t) Hashtbl.t = Hashtbl.create 39 (* Notification handling; reply is optional / asynchronous *) let do_check_text ofmt ~doc = - let doc, diags = Lp_doc.check_text ~doc in + let doc, diags = + try + Lp_doc.check_text ~doc + with Common.Error.Fatal(_pos, msg) -> + let loc : Pos.pos = + { + fname = Some(doc.uri); + start_line = 0; + start_col = 0; + end_line = 0; + end_col = 0 + } in + (doc, Lp_doc.mk_error ~doc loc msg) + in Hashtbl.replace doc_table doc.uri doc; Hashtbl.replace completed_table doc.uri doc; LIO.send_json ofmt @@ diags @@ -137,20 +150,26 @@ let kind_of_type tm = let do_symbols ofmt ~id params = let file, _, doc = grab_doc params in - let sym = Pure.get_symbols doc.final in - let sym = - Extra.StrMap.fold - (fun _ s l -> - let open Term in - (* LIO.log_error "sym" - ( s.sym_name ^ " | " - ^ Format.asprintf "%a" term !(s.sym_type)); *) - Option.map_default - (fun p -> mk_syminfo file - (s.sym_name, s.sym_path, kind_of_type s, p) :: l) l s.sym_pos) - sym [] in - let msg = LSP.mk_reply ~id ~result:(`List sym) in - LIO.send_json ofmt msg + match doc.final with + | None -> + let msg = LSP.mk_reply ~id ~result:`Null in + LIO.send_json ofmt msg + | Some ss -> + let sym = Pure.get_symbols ss in + let sym = + Extra.StrMap.fold + (fun _ s l -> + let open Term in + (* LIO.log_error "sym" + ( s.sym_name ^ " | " + ^ Format.asprintf "%a" term !(s.sym_type)); *) + Option.map_default + (fun p -> mk_syminfo file + (s.sym_name, s.sym_path, kind_of_type s, p) :: l) l s.sym_pos) + sym [] in + let msg = LSP.mk_reply ~id ~result:(`List sym) in + LIO.send_json ofmt msg + let get_docTextPosition params = let document = dict_field "textDocument" params in @@ -314,45 +333,50 @@ let get_symbol : Range.point -> let do_definition ofmt ~id params = let _, _, doc = grab_doc params in - let ln, pos = get_textPosition params in - - (* Lines send by the client start at 0 *) - let pt = Range.make_point (ln + 1) pos in - let sym_target = - match get_symbol pt doc.map with - | None -> "No symbol found" - | Some(token, _) -> token - in + match doc.final with + | None -> + let msg = LSP.mk_reply ~id ~result:`Null in + LIO.send_json ofmt msg + | Some ss -> + let ln, pos = get_textPosition params in + + (* Lines send by the client start at 0 *) + let pt = Range.make_point (ln + 1) pos in + let sym_target = + match get_symbol pt doc.map with + | None -> "No symbol found" + | Some(token, _) -> token + in - (*Some printing in the log*) - LIO.log_error "token map" (RangeMap.to_string snd doc.map); - LIO.log_error "do_definition" sym_target; - - let sym = Pure.get_symbols doc.final in - let map_pp : string = - Extra.StrMap.bindings sym - |> List.map (fun (key, sym) -> - Format.asprintf "{%s} / %s: @[%a@]" - key sym.Term.sym_name Pos.pp sym.sym_pos) - |> String.concat "\n" - in - LIO.log_error "symbol map" map_pp; + (*Some printing in the log*) + LIO.log_error "token map" (RangeMap.to_string snd doc.map); + LIO.log_error "do_definition" sym_target; + + let sym = Pure.get_symbols ss in + let map_pp : string = + Extra.StrMap.bindings sym + |> List.map (fun (key, sym) -> + Format.asprintf "{%s} / %s: @[%a@]" + key sym.Term.sym_name Pos.pp sym.sym_pos) + |> String.concat "\n" + in + LIO.log_error "symbol map" map_pp; - let sym_info = - match StrMap.find_opt sym_target sym with - | None -> `Null - | Some s -> - match s.sym_pos with + let sym_info = + match StrMap.find_opt sym_target sym with | None -> `Null - | Some pos -> - (* A JSON with the path towards the definition of the term - and its position is returned - /!\ : extension is fixed, only works for .lp files *) - mk_definfo - Library.(file_of_path s.Term.sym_path ^ lp_src_extension) pos - in - let msg = LSP.mk_reply ~id ~result:sym_info in - LIO.send_json ofmt msg + | Some s -> + match s.sym_pos with + | None -> `Null + | Some pos -> + (* A JSON with the path towards the definition of the term + and its position is returned + /!\ : extension is fixed, only works for .lp files *) + mk_definfo + Library.(file_of_path s.Term.sym_path ^ lp_src_extension) pos + in + let msg = LSP.mk_reply ~id ~result:sym_info in + LIO.send_json ofmt msg let hover_symInfo ofmt ~id params = @@ -382,36 +406,40 @@ let hover_symInfo ofmt ~id params = LIO.log_error "hoverSymInfo" sym_target; LIO.log_error "hoverSymInfo" (Range.interval_to_string interval); *) - (* The information about the tokens is stored *) - let sym = Pure.get_symbols doc.final in - - (* The start/finish positions are used to hover the full qualified term, - not just the token *) - let start = Range.interval_start interval - and finish = Range.interval_end interval in - - (* FIXME: types and typed conversion should take care of this *) - let sl, sc, fl, fc = - (Range.line start - 1), - (Range.column start - 1), - (Range.line finish - 1), - (Range.column finish - 1) - in + try + (* The information about the tokens is stored *) + let sym = + match doc.final with + | Some ss -> Pure.get_symbols ss + | None -> raise (Error.fatal_no_pos("Root state is missing + probably because new_doc has raised exception")) in + + (* The start/finish positions are used to hover the full qualified term, + not just the token *) + let start = Range.interval_start interval + and finish = Range.interval_end interval in + + (* FIXME: types and typed conversion should take care of this *) + let sl, sc, fl, fc = + (Range.line start - 1), + (Range.column start - 1), + (Range.line finish - 1), + (Range.column finish - 1) + in - let s = `Assoc["line", `Int sl; "character", `Int sc] in - let f = `Assoc["line", `Int fl; "character", `Int fc] in - let range = `Assoc["start", s; "end", f] in + let s = `Assoc["line", `Int sl; "character", `Int sc] in + let f = `Assoc["line", `Int fl; "character", `Int fc] in + let range = `Assoc["start", s; "end", f] in - let map_pp : string = - Extra.StrMap.bindings sym - |> List.map (fun (key, sym) -> - Format.asprintf "{%s} / %s: @[%a@]" - key sym.Term.sym_name Pos.pp sym.sym_pos) - |> String.concat "\n" - in - LIO.log_error "symbol map" map_pp; + let map_pp : string = + Extra.StrMap.bindings sym + |> List.map (fun (key, sym) -> + Format.asprintf "{%s} / %s: @[%a@]" + key sym.Term.sym_name Pos.pp sym.sym_pos) + |> String.concat "\n" + in + LIO.log_error "symbol map" map_pp; - try let sym_found = let open Timed in let open Term in