Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

1 files changed, 30 insertions, 3 deletions

diff --git a/ide/tags.ml b/ide/tags.ml
index 52ba54dc..eeace465 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -13,6 +13,9 @@ let make_tag (tt:GText.tag_table) ~name prop =
   tt#add new_tag#as_tag;
   new_tag
 
+let processed_color = ref "light green"
+let processing_color = ref "light blue"
+
 module Script =
 struct
   let table = GText.tag_table ()
@@ -23,8 +26,8 @@ struct
   let comment = make_tag table ~name:"comment" [`FOREGROUND "brown"]
   let reserved = make_tag table ~name:"reserved" [`FOREGROUND "dark red"]
   let error = make_tag table ~name:"error" [`UNDERLINE `DOUBLE ; `FOREGROUND "red"]
-  let to_process = make_tag table ~name:"to_process" [`BACKGROUND "light blue" ;`EDITABLE false]
-  let processed = make_tag table ~name:"processed" [`BACKGROUND "light green" ;`EDITABLE false]
+  let to_process = make_tag table ~name:"to_process" [`BACKGROUND !processing_color ;`EDITABLE false]
+  let processed = make_tag table ~name:"processed" [`BACKGROUND !processed_color;`EDITABLE false]
   let unjustified = make_tag table ~name:"unjustified" [`UNDERLINE `SINGLE; `FOREGROUND "red"; `BACKGROUND "gold";`EDITABLE false]
   let found = make_tag table ~name:"found" [`BACKGROUND "blue"; `FOREGROUND "white"]
   let hidden = make_tag table ~name:"hidden" [`INVISIBLE true; `EDITABLE false]
@@ -35,7 +38,7 @@ end
 module Proof =
 struct
   let table = GText.tag_table ()
-  let highlight = make_tag table ~name:"highlight" [`BACKGROUND "light green"]
+  let highlight = make_tag table ~name:"highlight" [`BACKGROUND !processed_color]
   let hypothesis = make_tag table ~name:"hypothesis" []
   let goal = make_tag table ~name:"goal" []
 end
@@ -45,3 +48,27 @@ struct
   let error = make_tag table ~name:"error" [`FOREGROUND "red"]
 end
 
+let string_of_color clr =
+  let r = Gdk.Color.red clr in
+  let g = Gdk.Color.green clr in
+  let b = Gdk.Color.blue clr in
+  Printf.sprintf "#%04X%04X%04X" r g b
+
+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.to_process#set_property (`BACKGROUND s)