diff options
Diffstat (limited to 'ide/tags.mli')
| -rw-r--r-- | ide/tags.mli | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/ide/tags.mli b/ide/tags.mli index 9c3261d6..14cfd0db 100644 --- a/ide/tags.mli +++ b/ide/tags.mli @@ -21,9 +21,6 @@ sig val tooltip : GText.tag val edit_zone : GText.tag (* for debugging *) val all : GText.tag list - - (* Not part of the all list. Special tags! *) - val read_only : GText.tag end module Proof : @@ -53,3 +50,13 @@ val set_processing_color : Gdk.color -> unit val get_error_color : unit -> Gdk.color val set_error_color : Gdk.color -> unit + +val get_error_fg_color : unit -> Gdk.color +val set_error_fg_color : Gdk.color -> unit + +val default_processed_color : string +val default_processing_color : string +val default_error_color : string +val default_error_fg_color : string +val default_color : string + |