diff options
| author | Hugo Herbelin | 2018-11-22 01:10:06 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-12-17 07:42:46 +0100 |
| commit | 06c4f33eedc14bfdf7c6a603ff87feccb57c32f5 (patch) | |
| tree | 8ad27815e8402f298f67a404a0aa56a147dc039f /ide | |
| parent | 7e155688331c8f004f34950da67108d7284e4e56 (diff) | |
CoqIDE: Restoring configuration of default width/height of main window.
Also removing dead code about show_toolbar: this is governed by an
item of the view menu rather than by the preference panel since
aa357d601 (Dec 2003).
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/preferences.ml | 34 |
1 files changed, 9 insertions, 25 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml index 045d650c1c..4aa8c92f73 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -815,33 +815,20 @@ let configure ?(apply=(fun () -> ())) parent = custom ~label box callback true in -(* - let show_toolbar = - bool - ~f:(fun s -> - current.show_toolbar <- s; - !show_toolbar s) - "Show toolbar" current.show_toolbar - in let window_height = string - ~f:(fun s -> current.window_height <- (try int_of_string s with _ -> 600); - !resize_window (); - ) - "Window height" - (string_of_int current.window_height) + ~f:(fun s -> try window_height#set (int_of_string s) with _ -> ()) + "Default window height at starting time" + (string_of_int window_height#get) in + let window_width = string - ~f:(fun s -> current.window_width <- - (try int_of_string s with _ -> 800)) - "Window width" - (string_of_int current.window_width) + ~f:(fun s -> try window_width#set (int_of_string s) with _ -> ()) + "Default window width at starting time" + (string_of_int window_width#get) in -*) -(* - let config_appearance = [show_toolbar; window_width; window_height] in -*) + let global_auto_revert = pbool "Enable global auto revert" global_auto_revert in let global_auto_revert_delay = string @@ -1049,10 +1036,7 @@ let configure ?(apply=(fun () -> ())) parent = Section("Project", Some (`STOCK "gtk-page-setup"), [project_file_name;read_project; ]); -(* - Section("Appearance", - config_appearance); -*) + Section("Appearance", Some `PREFERENCES, [window_width; window_height]); Section("Externals", None, [cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; cmd_print;cmd_editor;cmd_browse;doc_url;library_url]); |
