Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix/logs when missing pkg #1075

Merged
merged 4 commits into from
Apr 5, 2024
Merged
Show file tree
Hide file tree
Changes from 3 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions src/lsp/CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
-------
Expand Down
42 changes: 30 additions & 12 deletions src/lsp/lp_doc.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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)*)
Expand Down Expand Up @@ -123,19 +123,30 @@ 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;
version;
root;
final = root;
nodes = [];
logs = [];
logs = logs;
map = RangeMap.empty;
}

Expand All @@ -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 signature is missing
fblanqui marked this conversation as resolved.
Show resolved Hide resolved
probably because new_doc has raised exception")
fblanqui marked this conversation as resolved.
Show resolved Hide resolved
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) ->
Expand Down
183 changes: 105 additions & 78 deletions src/lsp/lp_lsp.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 =

Expand Down Expand Up @@ -382,36 +406,39 @@ 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("Horror")) in
fblanqui marked this conversation as resolved.
Show resolved Hide resolved

(* 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
Expand Down