Treat unmatched goals as new for diffs (highlighted)

Improve debug output

3 files changed, 15 insertions, 9 deletions

diff --git a/ide/idetop.ml b/ide/idetop.ml
index a2b85041e8..ea7c208314 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -219,7 +219,7 @@ let goals () =
         | Some oldp ->
           let (_,_,_,_,osigma) = Proof.proof oldp in
           (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)"))
+          with Not_found -> None) (* will appear as a new goal *)
         | None -> None
         in
         let (hyps_pp_list, concl_pp) = Proof_diffs.diff_goal_ide og_s ng nsigma in
diff --git a/printing/printer.ml b/printing/printer.ml
index 2bbda279bd..f11c74348d 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -722,11 +722,11 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map
   let get_ogs g =
     match os_map with
     | Some (osigma, _) ->
-      (* if Not_found, returning None treats the goal as new and it will be highlighted;
+      (* if Not_found, returning None treats the goal as new and it will be diff 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)"))
+      with Not_found -> None)
     | None -> None
   in
   let rec pr_rec n = function
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index 3e2093db4a..02acacfe8e 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -545,16 +545,22 @@ module GoalMap = Evar.Map
 
 let goal_to_evar g sigma = Id.to_string (Termops.pr_evar_suggested_name g sigma)
 
+open Goal.Set
+
 [@@@ocaml.warning "-32"]
 let db_goal_map op np ng_to_og =
-  Printf.printf "New Goals: ";
-  let (ngoals,_,_,_,nsigma) = Proof.proof np in
-  List.iter (fun ng -> Printf.printf "%d -> %s  " (Evar.repr ng) (goal_to_evar ng nsigma)) ngoals;
+  let pr_goals title prf =
+    Printf.printf "%s: " title;
+    let (goals,_,_,_,sigma) = Proof.proof prf in
+    List.iter (fun g -> Printf.printf "%d -> %s  " (Evar.repr g) (goal_to_evar g sigma)) goals;
+    let gs = diff (Proof.all_goals prf) (List.fold_left (fun s g -> add g s) empty goals) in
+    List.iter (fun g -> Printf.printf "%d  " (Evar.repr g)) (elements gs);
+  in
+
+  pr_goals "New Goals" np;
   (match op with
   | Some op ->
-    let (ogoals,_,_,_,osigma) = Proof.proof op in
-    Printf.printf "\nOld Goals: ";
-    List.iter (fun og -> Printf.printf "%d -> %s  " (Evar.repr og) (goal_to_evar og osigma)) ogoals
+    pr_goals "\nOld Goals" op
   | None -> ());
   Printf.printf "\nGoal map: ";
   GoalMap.iter (fun og ng -> Printf.printf "%d -> %d  " (Evar.repr og) (Evar.repr ng)) ng_to_og;