diff options
| -rw-r--r-- | ide/idetop.ml | 2 | ||||
| -rw-r--r-- | printing/printer.ml | 4 | ||||
| -rw-r--r-- | printing/proof_diffs.ml | 18 |
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; |