diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-17 23:30:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-09-20 15:20:32 +0200 |
| commit | 06d1ad739b952febce3220c372aa2dedf18e1c79 (patch) | |
| tree | e930f49b5b825dd6cb5562fb98855b6a96cc35d8 /ide/preferences.mli | |
| parent | 8bba34395e520ac606fc3efd0a875699fe968e69 (diff) | |
Adding a tag preference
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 |