aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
authorHugo Herbelin2018-11-22 01:10:06 +0100
committerHugo Herbelin2018-12-17 07:42:46 +0100
commit06c4f33eedc14bfdf7c6a603ff87feccb57c32f5 (patch)
tree8ad27815e8402f298f67a404a0aa56a147dc039f /ide
parent7e155688331c8f004f34950da67108d7284e4e56 (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.ml34
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]);