diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-02 19:07:52 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-02 19:07:52 +0000 |
| commit | 1f27f3d9e2df9052197c10eab8c4ccfecd5a5dae (patch) | |
| tree | b983d05dad28950b8a0de7ebb7604aaa47d7b527 /ide | |
| parent | 8a72970933994c9670e570fb6f3f768e14143237 (diff) | |
Better style handling in CoqIDE
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15273 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide.ml | 6 | ||||
| -rw-r--r-- | ide/preferences.ml | 13 | ||||
| -rw-r--r-- | ide/preferences.mli | 1 |
3 files changed, 16 insertions, 4 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index dcece7aed..579d638df 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -2368,6 +2368,12 @@ let main files = refresh_toolbar_hook := (fun () -> if current.show_toolbar then toolbar#misc#show () else toolbar#misc#hide ()); + refresh_style_hook := + (fun () -> + let style = style_manager#style_scheme current.source_style in + let iter_page p = p.script#source_buffer#set_style_scheme style in + List.iter iter_page session_notebook#pages; + ); refresh_font_hook := (fun () -> let fd = current.text_font in diff --git a/ide/preferences.ml b/ide/preferences.ml index b976eba3d..2ad2cc802 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -75,6 +75,7 @@ let inputenc_of_string s = (** Hooks *) let refresh_font_hook = ref (fun () -> ()) +let refresh_style_hook = ref (fun () -> ()) let refresh_background_color_hook = ref (fun () -> ()) let refresh_toolbar_hook = ref (fun () -> ()) let auto_complete_hook = ref (fun x -> ()) @@ -546,8 +547,12 @@ let configure ?(apply=(fun () -> ())) () = in let source_style = - combo "Highlighting style" - ~f:(fun s -> current.source_style <- s) ~new_allowed:false + let f s = + current.source_style <- s; + !refresh_style_hook () + in + combo "Highlighting style:" + ~f ~new_allowed:false style_manager#style_scheme_ids current.source_style in @@ -687,11 +692,11 @@ let configure ?(apply=(fun () -> ())) () = let cmds = [Section("Fonts", Some `SELECT_FONT, [config_font]); - Section("Colors", Some `SELECT_COLOR, [config_color]); + Section("Colors", Some `SELECT_COLOR, [config_color;source_style]); Section("Files", Some `DIRECTORY, [global_auto_revert;global_auto_revert_delay; auto_save; auto_save_delay; (* auto_save_name*) - encodings;source_style; + encodings; ]); Section("Project", Some (`STOCK "gtk-page-setup"), [project_file_name;read_project; diff --git a/ide/preferences.mli b/ide/preferences.mli index 92a748ef9..c5945e25a 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -80,6 +80,7 @@ val configure : ?apply:(unit -> unit) -> unit -> unit (* Hooks *) val refresh_font_hook : (unit -> unit) ref +val refresh_style_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 |