From ef2fce93057484b015c85713ad83f53f88762271 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sun, 7 Oct 2018 15:14:56 -0700
Subject: Show diffs in error messages if color is enabled

---
 printing/proof_diffs.ml | 24 +++++++++++++++++++-----
 1 file changed, 19 insertions(+), 5 deletions(-)

(limited to 'printing/proof_diffs.ml')

diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index 878e9f477b..07cdc1e8a3 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -39,6 +39,13 @@ uses strikeout on removed text.
 
 open Pp_diff
 
+let term_color = ref true
+
+let write_color_enabled enabled =
+  term_color := enabled
+
+let color_enabled () = !term_color
+
 let diff_option = ref `OFF
 
 let read_diffs_option () = match !diff_option with
@@ -46,11 +53,18 @@ let read_diffs_option () = match !diff_option with
 | `ON -> "on"
 | `REMOVED -> "removed"
 
-let write_diffs_option = function
-| "off" -> diff_option := `OFF
-| "on" -> diff_option := `ON
-| "removed" -> diff_option := `REMOVED
-| _ -> CErrors.user_err Pp.(str "Diffs option only accepts the following values: \"off\", \"on\", \"removed\".")
+let write_diffs_option opt =
+  let enable opt =
+    if not (color_enabled ()) then
+      CErrors.user_err Pp.(str "Enabling Diffs requires setting the \"-color\" command line argument to \"on\" or \"auto\".")
+    else
+      diff_option := opt
+  in
+  match opt with
+  | "off" -> diff_option := `OFF
+  | "on" -> enable `ON
+  | "removed" -> enable `REMOVED
+  | _ -> CErrors.user_err Pp.(str "Diffs option only accepts the following values: \"off\", \"on\", \"removed\".")
 
 let () =
   Goptions.(declare_string_option {
-- 
cgit v1.2.3