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.

Sign up for GitHub

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

Show the Goal panel if it has lost focus #1081

Merged
merged 3 commits into from
May 7, 2024
Merged

Show the Goal panel if it has lost focus #1081

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
80073a5
vscode: send answer with None goals when exception occurs
Alidra Apr 17, 2024
9a24661
Goals panel focus : change comment in lp_lsp
Alidra Apr 17, 2024
85355b7
vscode : do nothing when goals are null, get focus back for goals pan…
Alidra Apr 17, 2024
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
9 changes: 9 additions & 0 deletions editors/vscode/src/client.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -664,6 +664,15 @@ function sendGoalsRequest(position: Position, panel: WebviewPanel, docUri: Uri,
let cursor = { textDocument: doc, position: position };
const req = new RequestType<ParamsGoals, GoalResp, void>("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);

Expand Down
11 changes: 9 additions & 2 deletions src/lsp/lp_lsp.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 when exception occurs*)
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 =

Expand Down