LSP: leave goals unchanged in case of error when handling a tactic (#…

…1145)
Deducteam · Nov 7, 2024 · fb45b54 · fb45b54
1 parent 3223066
commit fb45b54
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/lsp/lp_doc.ml b/src/lsp/lp_doc.ml
@@ -65,7 +65,8 @@ let process_pstep (pstate,diags,logs) tac nb_subproofs =
     pstate, (tac_loc, 4, qres, goals) :: diags, logs
   | Tac_Error(loc,msg) ->
     let loc = option_default loc tac_loc in
-    pstate, (loc, 1, msg, None) :: diags, ((1, msg), loc) :: logs
+    let goals = Some (current_goals pstate) in
+    pstate, (loc, 1, msg, goals) :: diags, ((1, msg), loc) :: logs
 
 let process_proof pstate tacs logs =
   Pure.ProofTree.fold process_pstep (pstate,[],logs) tacs