diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-04-10 16:12:42 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-04-10 19:43:08 +0200 |
| commit | 7477094b353b48f1bd1f8ee97a8cd69c04be9db9 (patch) | |
| tree | 4170869fea6012788ad042a53790d2d83bc0fee2 /ide/preferences.mli | |
| parent | cbd7317516eaac4a5f37c896da5ea984ec1bb77a (diff) | |
CoqIDE: options for syntax highlighting
Diffstat (limited to 'ide/preferences.mli')
| -rw-r--r-- | ide/preferences.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/preferences.mli b/ide/preferences.mli index 26dc51f39..a93767751 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -95,6 +95,7 @@ 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 |