diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 4 | ||||
| -rw-r--r-- | printing/proof_diffs.ml | 28 | ||||
| -rw-r--r-- | printing/proof_diffs.mli | 6 |
3 files changed, 33 insertions, 5 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 14e734f1da..8da1d636f0 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -227,11 +227,11 @@ let tag_var = tag Tag.variable let pr_evar pr id l = hov 0 ( - tag_evar (str "?" ++ pr_id id) ++ + tag_evar (str "?" ++ pr_lident id) ++ (match l with | [] -> mt() | l -> - let f (id,c) = pr_id id ++ str ":=" ++ pr ltop c in + let f (id,c) = pr_lident id ++ str ":=" ++ pr ltop c in str"@{" ++ hov 0 (prlist_with_sep pr_semicolon f (List.rev l)) ++ str"}")) (* Assuming "{" and "}" brackets, prints diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index 43f70dfecc..b2ebc61b4e 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -252,6 +252,9 @@ let pp_of_type env sigma ty = let pr_leconstr_env ?lax ?inctx ?scope env sigma t = Ppconstr.pr_lconstr_expr env sigma (Constrextern.extern_constr ?lax ?inctx ?scope env sigma t) +let pr_econstr_env ?lax ?inctx ?scope env sigma t = + Ppconstr.pr_constr_expr env sigma (Constrextern.extern_constr ?lax ?inctx ?scope env sigma t) + let pr_lconstr_env ?lax ?inctx ?scope env sigma c = pr_leconstr_env ?lax ?inctx ?scope env sigma (EConstr.of_constr c) @@ -511,12 +514,12 @@ let match_goals ot nt = | CHole (k,naming,solve), CHole (k2,naming2,solve2) -> () | CPatVar _, CPatVar _ -> () | CEvar (n,l), CEvar (n2,l2) -> - let oevar = if ogname = "" then Id.to_string n else ogname in - nevar_to_oevar := CString.Map.add (Id.to_string n2) oevar !nevar_to_oevar; + let oevar = if ogname = "" then Id.to_string n.CAst.v else ogname in + nevar_to_oevar := CString.Map.add (Id.to_string n2.CAst.v) oevar !nevar_to_oevar; iter2 (fun x x2 -> let (_, g) = x and (_, g2) = x2 in constr_expr ogname g g2) l l2 | CEvar (n,l), nt' -> (* pass down the old goal evar name *) - match_goals_r (Id.to_string n) nt' nt' + match_goals_r (Id.to_string n.CAst.v) nt' nt' | CSort s, CSort s2 -> () | CCast (c,c'), CCast (c2,c'2) -> constr_expr ogname c c2; @@ -660,3 +663,22 @@ let make_goal_map op np = let ng_to_og = make_goal_map_i op np in (*db_goal_map op np ng_to_og;*) ng_to_og + +let diff_proofs ~diff_opt ?old proof = + let pp_proof p = + let sigma, env = Proof.get_proof_context p in + let pprf = Proof.partial_proof p in + Pp.prlist_with_sep Pp.fnl (pr_econstr_env env sigma) pprf in + match diff_opt with + | DiffOff -> pp_proof proof + | _ -> begin + try + let n_pp = pp_proof proof in + let o_pp = match old with + | None -> Pp.mt() + | Some old -> pp_proof old in + let show_removed = Some (diff_opt = DiffRemoved) in + Pp_diff.diff_pp_combined ~tokenize_string ?show_removed o_pp n_pp + with + | Pp_diff.Diff_Failure msg -> Pp.str msg + end diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli index ea64439456..6bdd7004fb 100644 --- a/printing/proof_diffs.mli +++ b/printing/proof_diffs.mli @@ -25,6 +25,10 @@ val write_color_enabled : bool -> unit (** true indicates that color output is enabled *) val color_enabled : unit -> bool +type diffOpt = DiffOff | DiffOn | DiffRemoved + +val string_to_diffs : string -> diffOpt + open Evd open Environ open Constr @@ -84,3 +88,5 @@ type hyp_info = { } val diff_hyps : string list list -> hyp_info CString.Map.t -> string list list -> hyp_info CString.Map.t -> Pp.t list + +val diff_proofs : diff_opt:diffOpt -> ?old:Proof.t -> Proof.t -> Pp.t |