Merge PR #6801: Highlight differences between successive proof steps (color, underline, etc.)

5 files changed, 30 insertions, 29 deletions

diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 89602c9b56..900964609d 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -68,6 +68,7 @@ type coq_cmdopts = {
   impredicative_set : Declarations.set_predicativity;
   stm_flags   : Stm.AsyncOpts.stm_opt;
   debug       : bool;
+  diffs_set   : bool;
   time        : bool;
 
   filter_opts : bool;
@@ -117,6 +118,7 @@ let init_args = {
   impredicative_set = Declarations.PredicativeSet;
   stm_flags    = Stm.AsyncOpts.default_opts;
   debug        = false;
+  diffs_set    = false;
   time         = false;
 
   filter_opts  = false;
@@ -526,6 +528,12 @@ let parse_args arglist : coq_cmdopts * string list =
     |"-color" -> set_color oval (next ())
     |"-config"|"--config" -> { oval with print_config = true }
     |"-debug" -> Coqinit.set_debug (); oval
+    |"-diffs" -> let opt = next () in
+                  if List.exists (fun x -> opt = x) ["off"; "on"; "removed"] then
+                    Proof_diffs.write_diffs_option opt
+                  else
+                    (prerr_endline ("Error: on|off|removed expected after -diffs"); exit 1);
+                  { oval with diffs_set = true }
     |"-stm-debug" -> Stm.stm_debug := true; oval
     |"-emacs" -> set_emacs oval
     |"-filteropts" -> { oval with filter_opts = true }
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index 9fb6219a61..7b0cdcf127 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -43,6 +43,7 @@ type coq_cmdopts = {
   impredicative_set : Declarations.set_predicativity;
   stm_flags   : Stm.AsyncOpts.stm_opt;
   debug       : bool;
+  diffs_set   : bool;
   time        : bool;
 
   filter_opts : bool;
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 7ae15ac100..7b7e1b16c0 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -318,12 +318,6 @@ let loop_flush_all () =
   Format.pp_print_flush !Topfmt.std_ft ();
   Format.pp_print_flush !Topfmt.err_ft ()
 
-let pr_open_cur_subgoals () =
-  try
-    let proof = Proof_global.give_me_the_proof () in
-    Printer.pr_open_subgoals ~proof
-  with Proof_global.NoCurrentProof -> Pp.str ""
-
 (* Goal equality heuristic. *)
 let pequal cmp1 cmp2 (a1,a2) (b1,b2) = cmp1 a1 b1 && cmp2 a2 b2
 let evleq e1 e2 = CList.equal Evar.equal e1 e2
@@ -346,7 +340,7 @@ let top_goal_print oldp newp =
     let proof_changed = not (Option.equal cproof oldp newp) in
     let print_goals = not !Flags.quiet &&
                       proof_changed && Proof_global.there_are_pending_proofs () in
-    if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ())
+    if print_goals then Printer.print_and_diff oldp newp;
   with
   | exn ->
     let (e, info) = CErrors.push exn in
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index e979d0e544..9b68f303a6 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -339,8 +339,8 @@ let do_vio opts =
 (******************************************************************************)
 (* Color Options                                                              *)
 (******************************************************************************)
-let init_color color_mode =
-  let has_color = match color_mode with
+let init_color opts =
+  let has_color = match opts.color with
   | `OFF -> false
   | `ON -> true
   | `AUTO ->
@@ -350,26 +350,23 @@ let init_color color_mode =
        its TERM variable is set to "dumb". *)
     try Sys.getenv "TERM" <> "dumb" with Not_found -> false
   in
-  if has_color then begin
-    let colors = try Some (Sys.getenv "COQ_COLORS") with Not_found -> None in
-    match colors with
-    | None ->
-      (** Default colors *)
-      Topfmt.default_styles ();
-      Topfmt.init_terminal_output ~color:true
-    | Some "" ->
-      (** No color output *)
-      Topfmt.init_terminal_output ~color:false
-    | Some s ->
-      (** Overwrite all colors *)
-      Topfmt.parse_color_config s;
-      Topfmt.init_terminal_output ~color:true
-  end
-  else
-    Topfmt.init_terminal_output ~color:false
+  let term_color =
+    if has_color then begin
+      let colors = try Some (Sys.getenv "COQ_COLORS") with Not_found -> None in
+      match colors with
+      | None -> Topfmt.default_styles (); true        (** Default colors *)
+      | Some "" -> false                              (** No color output *)
+      | Some s -> Topfmt.parse_color_config s; true   (** Overwrite all colors *)
+    end
+    else
+      false
+  in
+  if Proof_diffs.show_diffs () && not term_color && not opts.batch_mode then
+    CErrors.user_err Pp.(str "Error: -diffs requires enabling -color");
+  Topfmt.init_terminal_output ~color:term_color
 
 let print_style_tags opts =
-  let () = init_color opts.color in
+  let () = init_color opts in
   let tags = Topfmt.dump_tags () in
   let iter (t, st) =
     let opt = Terminal.eval st ^ t ^ Terminal.reset ^ "\n" in
@@ -520,7 +517,7 @@ type custom_toplevel = {
 }
 
 let coqtop_init ~opts extra =
-  init_color opts.color;
+  init_color opts;
   CoqworkmgrApi.(init !async_proofs_worker_priority);
   opts, extra
 
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 504ffa521b..d85fed5f43 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -72,7 +72,8 @@ let print_usage_channel co command =
 \n  -boot                  boot mode (implies -q and -batch)\
 \n  -bt                    print backtraces (requires configure debug flag)\
 \n  -debug                 debug mode (implies -bt)\
-\n  -stm-debug             STM debug mode (will trace every transaction) \
+\n  -diffs (on|off|removed) highlight differences between proof steps\
+\n  -stm-debug             STM debug mode (will trace every transaction)\
 \n  -emacs                 tells Coq it is executed under Emacs\
 \n  -noglob                do not dump globalizations\
 \n  -dump-glob f           dump globalizations in file f (to be used by coqdoc)\