aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/preferences.mli
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-04-11 16:11:00 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-04-11 16:11:00 +0000
commitb614ad9a111595b7968063c4d6c364ab91e19bec (patch)
treed23ee7dfc02df4dbb32d60e172ce7cfef131d466 /ide/preferences.mli
parentc712bf9d6e15fedb72a745273a38b487f8d2f34a (diff)
Added a background color configuration option in CoqIDE.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15127 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/preferences.mli')
-rw-r--r--ide/preferences.mli4
1 files changed, 3 insertions, 1 deletions
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 245514bd9..292e43972 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -61,6 +61,7 @@ type pref =
mutable vertical_tabs : bool;
mutable opposite_tabs : bool;
+ mutable background_color : string;
mutable processing_color : string;
mutable processed_color : string;
}
@@ -72,7 +73,8 @@ val current : pref ref
val configure : ?apply:(unit -> unit) -> unit -> unit
-val change_font : ( Pango.font_description -> unit) ref
+val change_font : (Pango.font_description -> unit) ref
+val change_background_color : (Gdk.color -> unit) ref
val show_toolbar : (bool -> unit) ref
val auto_complete : (bool -> unit) ref
val resize_window : (unit -> unit) ref