diff options
| author |  Stephane Glondu <steph@glondu.net> | 2012-06-04 12:07:52 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:07:52 +0200 |
| commit | 61dc740ed1c3780cccaec00d059a28f0d31d0052 (patch) | |
| tree | d88d05baf35b9b09a034233300f35a694f9fa6c2 /ide/preferences.mli | |
| parent | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff) | |
Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2
Diffstat (limited to 'ide/preferences.mli')
| -rw-r--r-- | ide/preferences.mli | 21 |
1 files changed, 13 insertions, 8 deletions
diff --git a/ide/preferences.mli b/ide/preferences.mli index f55088f1..b680c6f0 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -7,9 +7,11 @@ (************************************************************************) type project_behavior = Ignore_args | Append_args | Subst_args +type inputenc = Elocale | Eutf8 | Emanual of string type pref = { + mutable cmd_coqtop : string option; mutable cmd_coqc : string; mutable cmd_make : string; mutable cmd_coqmakefile : string; @@ -25,9 +27,7 @@ type pref = mutable read_project : project_behavior; mutable project_file_name : string; - mutable encoding_use_locale : bool; - mutable encoding_use_utf8 : bool; - mutable encoding_manual : string; + mutable encoding : inputenc; mutable automatic_tactics : string list; mutable cmd_print : string; @@ -57,9 +57,12 @@ type pref = *) mutable auto_complete : bool; mutable stop_before : bool; - mutable lax_syntax : bool; mutable vertical_tabs : bool; mutable opposite_tabs : bool; + + mutable background_color : string; + mutable processing_color : string; + mutable processed_color : string; } val save_pref : unit -> unit @@ -69,9 +72,11 @@ val current : pref ref val configure : ?apply:(unit -> unit) -> unit -> unit -val change_font : ( Pango.font_description -> unit) ref -val show_toolbar : (bool -> unit) ref -val auto_complete : (bool -> unit) ref -val resize_window : (unit -> unit) ref +(* Hooks *) +val refresh_font_hook : (unit -> unit) ref +val refresh_background_color_hook : (unit -> unit) ref +val refresh_toolbar_hook : (unit -> unit) ref +val resize_window_hook : (unit -> unit) ref +val refresh_tabs_hook : (unit -> unit) ref val use_default_doc_url : string |