aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/preferences.ml
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-05-02 20:37:02 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-05-02 20:37:02 +0000
commitb18eeba9ed6df82a0eb5a749aea0a17ea84ba70c (patch)
treef2c06feb4c2dd93c752f0141001244e967153e61 /ide/preferences.ml
parent1f27f3d9e2df9052197c10eab8c4ccfecd5a5dae (diff)
Added a bunch of new options relative to editor.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15274 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/preferences.ml')
-rw-r--r--ide/preferences.ml84
1 files changed, 79 insertions, 5 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 2ad2cc802..24e93d0cd 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -76,6 +76,7 @@ let inputenc_of_string s =
let refresh_font_hook = ref (fun () -> ())
let refresh_style_hook = ref (fun () -> ())
+let refresh_editor_hook = ref (fun () -> ())
let refresh_background_color_hook = ref (fun () -> ())
let refresh_toolbar_hook = ref (fun () -> ())
let auto_complete_hook = ref (fun x -> ())
@@ -141,6 +142,13 @@ type pref =
mutable processing_color : string;
mutable processed_color : string;
+ mutable dynamic_word_wrap : bool;
+ mutable show_line_number : bool;
+ mutable auto_indent : bool;
+ mutable show_spaces : bool;
+ mutable spaces_instead_of_tabs : bool;
+ mutable tab_length : int;
+
}
let use_default_doc_url = "(automatic)"
@@ -207,6 +215,12 @@ let current = {
processed_color = "light green";
processing_color = "light blue";
+ dynamic_word_wrap = false;
+ show_line_number = false;
+ auto_indent = false;
+ show_spaces = true;
+ spaces_instead_of_tabs = true;
+ tab_length = 2;
}
let save_pref () =
@@ -265,6 +279,12 @@ let save_pref () =
add "background_color" [p.background_color] ++
add "processing_color" [p.processing_color] ++
add "processed_color" [p.processed_color] ++
+ add "dynamic_word_wrap" [string_of_bool p.dynamic_word_wrap] ++
+ add "show_line_number" [string_of_bool p.show_line_number] ++
+ add "auto_indent" [string_of_bool p.auto_indent] ++
+ add "show_spaces" [string_of_bool p.show_spaces] ++
+ add "spaces_instead_of_tabs" [string_of_bool p.spaces_instead_of_tabs] ++
+ add "tab_length" [string_of_int p.tab_length] ++
Config_lexer.print_file pref_file
let load_pref () =
@@ -337,10 +357,14 @@ let load_pref () =
set_bool "opposite_tabs" (fun v -> np.opposite_tabs <- v);
set_hd "background_color" (fun v -> np.background_color <- v);
set_hd "processing_color" (fun v -> np.processing_color <- v);
- set_hd "processed_color" (fun v -> np.processed_color <- v)
-(*
- Format.printf "in load_pref: current.text_font = %s@." (Pango.Font.to_string current.text_font);
-*)
+ set_hd "processed_color" (fun v -> np.processed_color <- v);
+ set_bool "dynamic_word_wrap" (fun v -> np.dynamic_word_wrap <- v);
+ set_bool "show_line_number" (fun v -> np.show_line_number <- v);
+ set_bool "auto_indent" (fun v -> np.auto_indent <- v);
+ set_bool "show_spaces" (fun v -> np.show_spaces <- v);
+ set_bool "spaces_instead_of_tabs" (fun v -> np.spaces_instead_of_tabs <- v);
+ set_int "tab_length" (fun v -> np.tab_length <- v);
+ ()
let configure ?(apply=(fun () -> ())) () =
let cmd_coqtop =
@@ -447,6 +471,55 @@ let configure ?(apply=(fun () -> ())) () =
custom ~label box callback true
in
+ let config_editor =
+ let label = "Editor configuration" in
+ let box = GPack.vbox () in
+ let table = GPack.table
+ ~row_spacings:5
+ ~col_spacings:5
+ ~border_width:2
+ ~packing:(box#pack ~expand:true) ()
+ in
+ let row = ref 0 in
+ let gen_button text active =
+ let button = GButton.check_button
+ ~packing:(table#attach ~left:0 ~top:!row) ()
+ in
+ let _ = GMisc.label ~text ~xalign:0.
+ ~packing:(table#attach ~expand:`X ~left:1 ~top:!row) ()
+ in
+ let () = incr row in
+ let () = button#set_active active in
+ button
+ in
+ let wrap = gen_button "Dynamic word wrap" current.dynamic_word_wrap in
+ let line = gen_button "Show line number" current.show_line_number in
+ let auto_indent = gen_button "Auto indentation" current.auto_indent in
+ let show_spaces = gen_button "Show spaces" current.show_spaces in
+ let spaces_instead_of_tabs =
+ gen_button "Insert spaces instead of tabs"
+ current.spaces_instead_of_tabs
+ in
+(* let lbox = GPack.hbox ~packing:box#pack () in *)
+(* let _ = GMisc.label ~text:"Tab width" *)
+(* ~xalign:0. *)
+(* ~packing:(lbox#pack ~expand:true) () *)
+(* in *)
+(* let tab_width = GEdit.spin_button *)
+(* ~digits:0 ~packing:lbox#pack () *)
+(* in *)
+ let callback () =
+ current.dynamic_word_wrap <- wrap#active;
+ current.show_line_number <- line#active;
+ current.auto_indent <- auto_indent#active;
+ current.show_spaces <- show_spaces#active;
+ current.spaces_instead_of_tabs <- spaces_instead_of_tabs#active;
+(* current.tab_length <- tab_width#value_as_int; *)
+ !refresh_editor_hook ()
+ in
+ custom ~label box callback true
+ in
+
(*
let show_toolbar =
bool
@@ -692,7 +765,8 @@ let configure ?(apply=(fun () -> ())) () =
let cmds =
[Section("Fonts", Some `SELECT_FONT,
[config_font]);
- Section("Colors", Some `SELECT_COLOR, [config_color;source_style]);
+ Section("Colors", Some `SELECT_COLOR, [config_color; source_style]);
+ Section("Editor", Some `EDIT, [config_editor]);
Section("Files", Some `DIRECTORY,
[global_auto_revert;global_auto_revert_delay;
auto_save; auto_save_delay; (* auto_save_name*)