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.mli | 21 ++------------------- 1 file changed, 2 insertions(+), 19 deletions(-) (limited to 'ide/tags.mli') diff --git a/ide/tags.mli b/ide/tags.mli index 00583f1b..02e15a5a 100644 --- a/ide/tags.mli +++ b/ide/tags.mli @@ -11,6 +11,7 @@ sig val table : GText.tag_table val comment : GText.tag val error : GText.tag + val warning : GText.tag val error_bg : GText.tag val to_process : GText.tag val processed : GText.tag @@ -20,6 +21,7 @@ sig val sentence : GText.tag val tooltip : GText.tag val edit_zone : GText.tag (* for debugging *) + val ephemere : GText.tag list val all : GText.tag list end @@ -41,22 +43,3 @@ end val string_of_color : Gdk.color -> string val color_of_string : string -> Gdk.color - -val get_processed_color : unit -> Gdk.color -val set_processed_color : Gdk.color -> unit - -val get_processing_color : unit -> Gdk.color -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 - -- cgit v1.2.3