diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqloop.ml | 44 | ||||
| -rw-r--r-- | toplevel/g_toplevel.mlg | 3 |
2 files changed, 47 insertions, 0 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 1f319d2bfd..97f0e57d2e 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -418,6 +418,50 @@ let rec vernac_loop ~state = Feedback.msg_notice (v 0 (goal ++ evars)); vernac_loop ~state + | Some VernacShowProofDiffs removed -> + (* extension of Vernacentries.show_proof *) + let to_pp pstate = + let p = Option.get pstate in + let sigma, env = Pfedit.get_proof_context p in + let pprf = Proof.partial_proof p in + Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf + (* We print nothing if there are no goals left *) + in + + if not (Proof_diffs.color_enabled ()) then + CErrors.user_err Pp.(str "Show Proof Diffs requires setting the \"-color\" command line argument to \"on\" or \"auto\".") + else begin + let out = + try + let n_pp = to_pp state.proof in + if true (*Proof_diffs.show_diffs ()*) then + let doc = state.doc in + let oproof = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in + try + let o_pp = to_pp oproof in + let tokenize_string = Proof_diffs.tokenize_string in + let show_removed = Some removed in + Pp_diff.diff_pp_combined ~tokenize_string ?show_removed o_pp n_pp + with + | Pfedit.NoSuchGoal + | Option.IsNone -> n_pp + | Pp_diff.Diff_Failure msg -> begin + (* todo: print the unparsable string (if we know it) *) + Feedback.msg_warning Pp.(str ("Diff failure: " ^ msg) ++ cut() + ++ str "Showing results without diff highlighting" ); + n_pp + end + else + n_pp + with + | Pfedit.NoSuchGoal + | Option.IsNone -> + CErrors.user_err (str "No goals to show.") + in + Feedback.msg_notice out; + end; + vernac_loop ~state + | None -> top_stderr (fnl ()); exit 0 diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg index e180d9e750..56fda58a25 100644 --- a/toplevel/g_toplevel.mlg +++ b/toplevel/g_toplevel.mlg @@ -22,6 +22,7 @@ type vernac_toplevel = | VernacQuit | VernacControl of vernac_control | VernacShowGoal of { gid : int; sid: int } + | VernacShowProofDiffs of bool module Toplevel_ : sig val vernac_toplevel : vernac_toplevel option Entry.t @@ -59,6 +60,8 @@ GRAMMAR EXTEND Gram (* show a goal for the specified proof state *) | test_show_goal; IDENT "Show"; IDENT "Goal"; gid = natural; IDENT "at"; sid = natural; "." -> { Some (VernacShowGoal {gid; sid}) } + | IDENT "Show"; IDENT "Proof"; IDENT "Diffs"; removed = OPT [ IDENT "removed" -> { () } ]; "." -> + { Some (VernacShowProofDiffs (removed <> None)) } | cmd = Pvernac.Vernac_.main_entry -> { match cmd with | None -> None |