Show the Goal panel if it has lost focus (#1081)

* vscode: send answer with None goals when exception occurs

* Goals panel focus : change comment in lp_lsp

* vscode : do nothing when goals are null, get focus back for goals panel before showing logs and goals

editors/vscode/src/client.ts

@@ -699,6 +699,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);
 

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 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 =