diff options
Diffstat (limited to 'ide/preferences.mli')
| -rw-r--r-- | ide/preferences.mli | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/ide/preferences.mli b/ide/preferences.mli index d815c01dd..b5c7ea222 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -12,6 +12,14 @@ val style_manager : GSourceView2.source_style_scheme_manager type project_behavior = Ignore_args | Append_args | Subst_args type inputenc = Elocale | Eutf8 | Emanual of string +type tag = { + tag_fg_color : string option; + tag_bg_color : string option; + tag_bold : bool; + tag_italic : bool; + tag_underline : bool; +} + class type ['a] repr = object method into : string list -> 'a option @@ -33,6 +41,8 @@ object method default : 'a end +val list_tags : unit -> tag preference Util.String.Map.t + val cmd_coqtop : string option preference val cmd_coqc : string preference val cmd_make : string preference |