Get hyps and goal the same way Printer does; don't omit info

Allow for new goals that don't map to old goals
Include background_goals in all_goals return value
Fix incorrect change to raw diffs in shorten_diff_span
Fixes #8922

1 files changed, 3 insertions, 8 deletions

diff --git a/ide/idetop.ml b/ide/idetop.ml
index 8a221a93e9..8cb02190e6 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -212,25 +212,20 @@ let goals () =
     if Proof_diffs.show_diffs () then begin
       let oldp = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in
       let diff_goal_map = Proof_diffs.make_goal_map oldp newp in
-      let map_goal_for_diff ng = (* todo: move to proof_diffs.ml *)
-        try Evar.Map.find ng diff_goal_map  with Not_found -> ng
-      in
 
       let process_goal_diffs nsigma ng =
         let open Evd in
-        let og = map_goal_for_diff ng in
         let og_s = match oldp with
         | Some oldp ->
           let (_,_,_,_,osigma) = Proof.proof oldp in
-          Some { it = og; sigma = osigma }
+          (try Some { it = Evar.Map.find ng diff_goal_map; sigma = osigma }
+          with Not_found -> raise (Pp_diff.Diff_Failure "Unable to match goals between old and new proof states (6)"))
         | None -> None
         in
         let (hyps_pp_list, concl_pp) = Proof_diffs.diff_goal_ide og_s ng nsigma in
         { Interface.goal_hyp = hyps_pp_list; Interface.goal_ccl = concl_pp; Interface.goal_id = Goal.uid ng }
       in
-      try
-        Some (export_pre_goals (Proof.map_structured_proof newp process_goal_diffs))
-      with Pp_diff.Diff_Failure _ -> Some (export_pre_goals (Proof.map_structured_proof newp process_goal))
+      Some (export_pre_goals (Proof.map_structured_proof newp process_goal_diffs))
     end else
       Some (export_pre_goals (Proof.map_structured_proof newp process_goal))
   with Proof_global.NoCurrentProof -> None;;