diff options
Diffstat (limited to 'ide/tags.ml')
-rw-r--r-- | ide/tags.ml | 50 |
1 files changed, 36 insertions, 14 deletions
diff --git a/ide/tags.ml b/ide/tags.ml index 955dfa96..04ad9a51 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -15,25 +15,37 @@ let make_tag (tt:GText.tag_table) ~name prop = let processed_color = ref "light green" let processing_color = ref "light blue" +let error_color = ref "#FFCCCC" module Script = struct let table = GText.tag_table () - let kwd = make_tag table ~name:"kwd" [`FOREGROUND "blue"] - let qed = make_tag table ~name:"qed" [`FOREGROUND "blue"] - let decl = make_tag table ~name:"decl" [`FOREGROUND "orange red"] - let proof_decl = make_tag table ~name:"proof_decl" [`FOREGROUND "orange red"] - 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 !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 comment = make_tag table ~name:"comment" [] + let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE ; `FOREGROUND "red"] + 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 incomplete = make_tag table ~name:"incomplete" [ + `BACKGROUND !processing_color; + `BACKGROUND_STIPPLE_SET true; + ] + let unjustified = make_tag table ~name:"unjustified" [`BACKGROUND "gold"] let found = make_tag table ~name:"found" [`BACKGROUND "blue"; `FOREGROUND "white"] - let hidden = make_tag table ~name:"hidden" [`INVISIBLE true; `EDITABLE false] - let folded = make_tag table ~name:"locked" [`EDITABLE false; `BACKGROUND "light grey"] - let paren = make_tag table ~name:"paren" [`BACKGROUND "purple"] let sentence = make_tag table ~name:"sentence" [] + let tooltip = make_tag table ~name:"tooltip" [] (* debug:`BACKGROUND "blue" *) + + let all = + [comment; error; error_bg; to_process; processed; incomplete; unjustified; + found; sentence; tooltip] + + let edit_zone = + let t = make_tag table ~name:"edit_zone" [`UNDERLINE `SINGLE] in + t#set_priority (List.length all); + t + let all = edit_zone :: all + + let read_only = make_tag table ~name:"read_only" [`EDITABLE false ] + end module Proof = struct @@ -46,6 +58,8 @@ module Message = struct let table = GText.tag_table () let error = make_tag table ~name:"error" [`FOREGROUND "red"] + let warning = make_tag table ~name:"warning" [`FOREGROUND "orange"] + let item = make_tag table ~name:"item" [`WEIGHT `BOLD] end let string_of_color clr = @@ -71,4 +85,12 @@ 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) |