From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- ide/tags.ml | 61 ++++++++++--------------------------------------------------- 1 file changed, 10 insertions(+), 51 deletions(-) (limited to 'ide/tags.ml') 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) - -- cgit v1.2.3