From 80073a5cd8139463d0013ab22df88ab9fe2ce019 Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Wed, 17 Apr 2024 13:00:32 +0200 Subject: [PATCH 1/3] vscode: send answer with None goals when exception occurs --- src/lsp/lp_lsp.ml | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/lsp/lp_lsp.ml b/src/lsp/lp_lsp.ml index 7023d40f2..99105ae97 100644 --- a/src/lsp/lp_lsp.ml +++ b/src/lsp/lp_lsp.ml @@ -238,7 +238,7 @@ let get_node_at_pos doc line pos = let rec get_goals ~doc ~line ~pos = let node = get_node_at_pos doc line pos in let goals = match node with - | None -> None + | None -> Some([], None) | Some n -> closest_before (line+1, pos) n.goals in match goals with @@ -526,7 +526,14 @@ let process_input ofmt (com : J.t) = | exn -> let bt = Printexc.get_backtrace () in LIO.log_error "[BT]" bt; - LIO.log_error "process_input" (Printexc.to_string exn) + LIO.log_error "process_input" (Printexc.to_string exn); + (*Send an "empty" answer with Null goals that will be treated specifically by the client*) + let id = oint_field "id" (U.to_assoc com) in + let goals = None in + let logs = "" in + let result = LSP.json_of_goals goals ~logs in + let msg = LSP.mk_reply ~id ~result in + LIO.send_json ofmt msg let main std log_file = From 9a2466181320fb2bcc5e6912670e9ee28e16f81e Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Wed, 17 Apr 2024 13:11:57 +0200 Subject: [PATCH 2/3] Goals panel focus : change comment in lp_lsp --- src/lsp/lp_lsp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lsp/lp_lsp.ml b/src/lsp/lp_lsp.ml index 99105ae97..33589863c 100644 --- a/src/lsp/lp_lsp.ml +++ b/src/lsp/lp_lsp.ml @@ -527,7 +527,7 @@ let process_input ofmt (com : J.t) = let bt = Printexc.get_backtrace () in LIO.log_error "[BT]" bt; LIO.log_error "process_input" (Printexc.to_string exn); - (*Send an "empty" answer with Null goals that will be treated specifically by the client*) + (*Send an "empty" answer with Null goals when exception occurs*) let id = oint_field "id" (U.to_assoc com) in let goals = None in let logs = "" in From 85355b7fccc4d01067a6418a750a304d89e972d8 Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Wed, 17 Apr 2024 13:02:07 +0200 Subject: [PATCH 3/3] vscode : do nothing when goals are null, get focus back for goals panel before showing logs and goals --- editors/vscode/src/client.ts | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/editors/vscode/src/client.ts b/editors/vscode/src/client.ts index 7ee27277e..0a7af5a86 100644 --- a/editors/vscode/src/client.ts +++ b/editors/vscode/src/client.ts @@ -664,6 +664,15 @@ function sendGoalsRequest(position: Position, panel: WebviewPanel, docUri: Uri, let cursor = { textDocument: doc, position: position }; const req = new RequestType("proof/goals"); client.sendRequest(req, cursor).then((goals) => { + // If uri is not a lambdapi/dedukti file, do nothing + if(goals.goals == null){ + return; + } + // Take focus back if the goal panel lost it. + window.showErrorMessage("Going through Goals"); + if(!panel.active) { + panel.reveal(2, false); + } updateTerminalText(goals.logs);