Imported Upstream version 8.6

1 files changed, 2 insertions, 19 deletions

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
-