1 files changed, 10 insertions, 51 deletions
diff --git a/ide/tags.ml b/ide/tags.ml
index 0e4ab96d..e4510e7a 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -13,28 +13,16 @@ let make_tag (tt:GText.tag_table) ~name prop =
   tt#add new_tag#as_tag;
   new_tag
 
-(* These work fine for colorblind people too *)
-let default_processed_color = "light green"
-let default_processing_color = "light blue"
-let default_error_color = "#FFCCCC"
-let default_error_fg_color = "red"
-let default_color = "cornsilk"
-
-let processed_color = ref default_processed_color
-let processing_color = ref default_processing_color
-let error_color = ref default_error_color
-let error_fg_color = ref default_error_fg_color
-
 module Script =
 struct
   let table = GText.tag_table ()
   let comment = make_tag table ~name:"comment" []
-  let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE ; `FOREGROUND !error_fg_color]
-  let error_bg = make_tag table ~name:"error_bg" [`BACKGROUND !error_color]
-  let to_process = make_tag table ~name:"to_process" [`BACKGROUND !processing_color]
-  let processed = make_tag table ~name:"processed" [`BACKGROUND !processed_color]
+  let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE]
+  let warning = make_tag table ~name:"warning" [`UNDERLINE `SINGLE; `FOREGROUND "blue"]
+  let error_bg = make_tag table ~name:"error_bg" []
+  let to_process = make_tag table ~name:"to_process" []
+  let processed = make_tag table ~name:"processed" []
   let incomplete = make_tag table ~name:"incomplete" [
-          `BACKGROUND !processing_color;
           `BACKGROUND_STIPPLE_SET true;
   ]
   let unjustified = make_tag table ~name:"unjustified" [`BACKGROUND "gold"]
@@ -42,9 +30,11 @@ struct
   let sentence = make_tag table ~name:"sentence" []
   let tooltip = make_tag table ~name:"tooltip" [] (* debug:`BACKGROUND "blue" *)
 
+  let ephemere =
+    [error; warning; error_bg; tooltip; processed; to_process; incomplete; unjustified]
+
   let all =
-    [comment; error; error_bg; to_process; processed; incomplete; unjustified;
-     found; sentence; tooltip]
+    comment :: found :: sentence :: ephemere
 
   let edit_zone =
     let t = make_tag table ~name:"edit_zone" [`UNDERLINE `SINGLE] in
@@ -56,7 +46,7 @@ end
 module Proof =
 struct
   let table = GText.tag_table ()
-  let highlight = make_tag table ~name:"highlight" [`BACKGROUND !processed_color]
+  let highlight = make_tag table ~name:"highlight" []
   let hypothesis = make_tag table ~name:"hypothesis" []
   let goal = make_tag table ~name:"goal" []
 end
@@ -77,34 +67,3 @@ let string_of_color clr =
 let color_of_string s =
   let colormap = Gdk.Color.get_system_colormap () in
   Gdk.Color.alloc ~colormap (`NAME s)
-
-let get_processed_color () = color_of_string !processed_color
-
-let set_processed_color clr =
-  let s = string_of_color clr in
-  processed_color := s;
-  Script.processed#set_property (`BACKGROUND s);
-  Proof.highlight#set_property (`BACKGROUND s)
-
-let get_processing_color () = color_of_string !processing_color
-
-let set_processing_color clr =
-  let s = string_of_color clr in
-  processing_color := s;
-  Script.incomplete#set_property (`BACKGROUND s);
-  Script.to_process#set_property (`BACKGROUND s)
-
-let get_error_color () = color_of_string !error_color
-
-let set_error_color clr =
-  let s = string_of_color clr in
-  error_color := s;
-  Script.error_bg#set_property (`BACKGROUND s)
-
-let get_error_fg_color () = color_of_string !error_fg_color
-
-let set_error_fg_color clr =
-  let s = string_of_color clr in
-  error_fg_color := s;
-  Script.error#set_property (`FOREGROUND s)
-