From a7121ed7ba1a5a55845b5ffa4846b8aa0e293e5d Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Wed, 7 Nov 2018 00:23:07 -0800
Subject: 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

---
 printing/printer.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index da364c8b9e..a91ad63ac1 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -674,10 +674,6 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map
     | None -> GoalMap.empty
   in
 
-  let map_goal_for_diff ng = (* todo: move to proof_diffs.ml *)
-    try GoalMap.find ng diff_goal_map  with Not_found -> ng
-  in
-
   (** Printing functions for the extra informations. *)
   let rec print_stack a = function
     | [] -> Pp.int a
@@ -713,7 +709,12 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map
 
   let get_ogs g =
     match os_map with
-    | Some (osigma, _) -> Some { it = map_goal_for_diff g; sigma = osigma }
+    | Some (osigma, _) ->
+      (* if Not_found, returning None treats the goal as new and it will be highlighted;
+         returning Some { it = g; sigma = sigma } will compare the new goal
+         to itself and it won't be highlighted *)
+      (try Some { it = GoalMap.find g diff_goal_map; sigma = osigma }
+      with Not_found -> raise (Pp_diff.Diff_Failure "Unable to match goals between old and new proof states (7)"))
     | None -> None
   in
   let rec pr_rec n = function
-- 
cgit v1.2.3