diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-16 03:57:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-16 04:52:08 +0200 |
| commit | cda147bf2b22e5230abd6fb604e9b8c105828717 (patch) | |
| tree | 88ab3ce142b9e7a214edfb348cdc28052d6299cd /ide/preferences.mli | |
| parent | 5a90c69f8e4699f205ec3e59cfd49ad9fb9f6f87 (diff) | |
Taking advantage of the new type of preferences.
We use uniform functions instead of code duplication.
Likewise, we disentangle the hook mechanisms by using
callbacks connected to preferences instead.
Only the easy hook bits were removed. The most awing one,
the editor refreshing hook, is still alive.
Diffstat (limited to 'ide/preferences.mli')
| -rw-r--r-- | ide/preferences.mli | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/ide/preferences.mli b/ide/preferences.mli index 0a83e609b..1da8b3157 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -105,10 +105,5 @@ val configure : ?apply:(unit -> unit) -> unit -> unit (* Hooks *) val refresh_editor_hook : (unit -> unit) ref -val refresh_style_hook : (unit -> unit) ref -val refresh_language_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 |