From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 4 Jun 2012 12:07:52 +0200 Subject: Imported Upstream version 8.4~gamma0+really8.4beta2 --- ide/preferences.ml | 210 ++++++++++++++++++++++++++++++++++++----------------- 1 file changed, 143 insertions(+), 67 deletions(-) (limited to 'ide/preferences.ml') diff --git a/ide/preferences.ml b/ide/preferences.ml index 02673098..d320ddda 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -10,9 +10,22 @@ open Configwin open Printf let pref_file = Filename.concat Minilib.xdg_config_home "coqiderc" - let accel_file = Filename.concat Minilib.xdg_config_home "coqide.keys" +let get_config_file name = + let find_config dir = Sys.file_exists (Filename.concat dir name) in + let config_dir = List.find find_config Minilib.xdg_config_dirs in + Filename.concat config_dir name + +(* Small hack to handle v8.3 to v8.4 change in configuration file *) +let loaded_pref_file = + try get_config_file "coqiderc" + with Not_found -> Filename.concat Minilib.home ".coqiderc" + +let loaded_accel_file = + try get_config_file "coqide.keys" + with Not_found -> Filename.concat Minilib.home ".coqide.keys" + let mod_to_str (m:Gdk.Tags.modifier) = match m with | `MOD1 -> "" @@ -40,8 +53,32 @@ let project_behavior_of_string s = else if s = "appended to arguments" then Append_args else Ignore_args +type inputenc = Elocale | Eutf8 | Emanual of string + +let string_of_inputenc = function + |Elocale -> "LOCALE" + |Eutf8 -> "UTF-8" + |Emanual s -> s + +let inputenc_of_string s = + (if s = "UTF-8" then Eutf8 + else if s = "LOCALE" then Elocale + else Emanual s) + + +(** Hooks *) + +let refresh_font_hook = ref (fun () -> ()) +let refresh_background_color_hook = ref (fun () -> ()) +let refresh_toolbar_hook = ref (fun () -> ()) +let auto_complete_hook = ref (fun x -> ()) +let contextual_menus_on_goal_hook = ref (fun x -> ()) +let resize_window_hook = ref (fun () -> ()) +let refresh_tabs_hook = ref (fun () -> ()) + type pref = { + mutable cmd_coqtop : string option; mutable cmd_coqc : string; mutable cmd_make : string; mutable cmd_coqmakefile : string; @@ -57,9 +94,7 @@ type pref = mutable read_project : project_behavior; mutable project_file_name : string; - mutable encoding_use_locale : bool; - mutable encoding_use_utf8 : bool; - mutable encoding_manual : string; + mutable encoding : inputenc; mutable automatic_tactics : string list; mutable cmd_print : string; @@ -89,15 +124,20 @@ type pref = *) mutable auto_complete : bool; mutable stop_before : bool; - mutable lax_syntax : bool; mutable vertical_tabs : bool; mutable opposite_tabs : bool; + + mutable background_color : string; + mutable processing_color : string; + mutable processed_color : string; + } let use_default_doc_url = "(automatic)" let (current:pref ref) = ref { + cmd_coqtop = None; cmd_coqc = "coqc"; cmd_make = "make"; cmd_coqmakefile = "coq_makefile -o makefile *.v"; @@ -114,9 +154,7 @@ let (current:pref ref) = read_project = Ignore_args; project_file_name = "_CoqProject"; - encoding_use_locale = true; - encoding_use_utf8 = false; - encoding_manual = "ISO_8859-1"; + encoding = if Sys.os_type = "Win32" then Eutf8 else Elocale; automatic_tactics = ["trivial"; "tauto"; "auto"; "omega"; "auto with *"; "intuition" ]; @@ -150,32 +188,25 @@ let (current:pref ref) = *) auto_complete = false; stop_before = true; - lax_syntax = true; vertical_tabs = false; opposite_tabs = false; - } - - -let change_font = ref (fun f -> ()) -let show_toolbar = ref (fun x -> ()) + background_color = "cornsilk"; + processed_color = "light green"; + processing_color = "light blue"; -let auto_complete = ref (fun x -> ()) - -let contextual_menus_on_goal = ref (fun x -> ()) - -let resize_window = ref (fun () -> ()) + } let save_pref () = if not (Sys.file_exists Minilib.xdg_config_home) then Unix.mkdir Minilib.xdg_config_home 0o700; - (try GtkData.AccelMap.save accel_file - with _ -> ()); + let () = try GtkData.AccelMap.save accel_file with _ -> () in let p = !current in let add = Minilib.Stringmap.add in let (++) x f = f x in Minilib.Stringmap.empty ++ + add "cmd_coqtop" (match p.cmd_coqtop with | None -> [] | Some v-> [v]) ++ add "cmd_coqc" [p.cmd_coqc] ++ add "cmd_make" [p.cmd_make] ++ add "cmd_coqmakefile" [p.cmd_coqmakefile] ++ @@ -190,9 +221,7 @@ let save_pref () = add "project_options" [string_of_project_behavior p.read_project] ++ add "project_file_name" [p.project_file_name] ++ - add "encoding_use_locale" [string_of_bool p.encoding_use_locale] ++ - add "encoding_use_utf8" [string_of_bool p.encoding_use_utf8] ++ - add "encoding_manual" [p.encoding_manual] ++ + add "encoding" [string_of_inputenc p.encoding] ++ add "automatic_tactics" p.automatic_tactics ++ add "cmd_print" [p.cmd_print] ++ @@ -217,19 +246,18 @@ let save_pref () = add "query_window_width" [string_of_int p.query_window_width] ++ add "auto_complete" [string_of_bool p.auto_complete] ++ add "stop_before" [string_of_bool p.stop_before] ++ - add "lax_syntax" [string_of_bool p.lax_syntax] ++ add "vertical_tabs" [string_of_bool p.vertical_tabs] ++ add "opposite_tabs" [string_of_bool p.opposite_tabs] ++ + add "background_color" [p.background_color] ++ + add "processing_color" [p.processing_color] ++ + add "processed_color" [p.processed_color] ++ Config_lexer.print_file pref_file let load_pref () = - let accel_dir = List.find - (fun x -> Sys.file_exists (Filename.concat x "coqide.keys")) - Minilib.xdg_config_dirs in - GtkData.AccelMap.load (Filename.concat accel_dir "coqide.keys"); + let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in let p = !current in - let m = Config_lexer.load_file pref_file in + let m = Config_lexer.load_file loaded_pref_file in let np = { p with cmd_coqc = p.cmd_coqc } in let set k f = try let v = Minilib.Stringmap.find k m in f v with _ -> () in let set_hd k f = set k (fun v -> f (List.hd v)) in @@ -239,6 +267,8 @@ let load_pref () = let set_command_with_pair_compat k f = set k (function [v1;v2] -> f (v1^"%s"^v2) | [v] -> f v | _ -> raise Exit) in + let set_option k f = set k (fun v -> f (match v with |[] -> None |h::_ -> Some h)) in + set_option "cmd_coqtop" (fun v -> np.cmd_coqtop <- v); set_hd "cmd_coqc" (fun v -> np.cmd_coqc <- v); set_hd "cmd_make" (fun v -> np.cmd_make <- v); set_hd "cmd_coqmakefile" (fun v -> np.cmd_coqmakefile <- v); @@ -249,9 +279,7 @@ let load_pref () = set_bool "auto_save" (fun v -> np.auto_save <- v); set_int "auto_save_delay" (fun v -> np.auto_save_delay <- v); set_pair "auto_save_name" (fun v1 v2 -> np.auto_save_name <- (v1,v2)); - set_bool "encoding_use_locale" (fun v -> np.encoding_use_locale <- v); - set_bool "encoding_use_utf8" (fun v -> np.encoding_use_utf8 <- v); - set_hd "encoding_manual" (fun v -> np.encoding_manual <- v); + set_hd "encoding_manual" (fun v -> np.encoding <- (inputenc_of_string v)); set_hd "project_options" (fun v -> np.read_project <- (project_behavior_of_string v)); set_hd "project_file_name" (fun v -> np.project_file_name <- v); @@ -290,15 +318,21 @@ let load_pref () = set_int "query_window_height" (fun v -> np.query_window_height <- v); set_bool "auto_complete" (fun v -> np.auto_complete <- v); set_bool "stop_before" (fun v -> np.stop_before <- v); - set_bool "lax_syntax" (fun v -> np.lax_syntax <- v); set_bool "vertical_tabs" (fun v -> np.vertical_tabs <- v); 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); current := np (* Format.printf "in load_pref: current.text_font = %s@." (Pango.Font.to_string !current.text_font); *) let configure ?(apply=(fun () -> ())) () = + let cmd_coqtop = + string + ~f:(fun s -> !current.cmd_coqtop <- if s = "AUTO" then None else Some s) + " coqtop" (match !current.cmd_coqtop with |None -> "AUTO" | Some x -> x) in let cmd_coqc = string ~f:(fun s -> !current.cmd_coqc <- s) @@ -325,7 +359,7 @@ let configure ?(apply=(fun () -> ())) () = let w = GMisc.font_selection () in w#set_preview_text "Goal (∃n : nat, n ≤ 0)∧(∀x,y,z, x∈y⋃z↔x∈y∨x∈z)."; - box#pack w#coerce; + box#pack ~expand:true w#coerce; ignore (w#misc#connect#realize ~callback:(fun () -> w#set_font_name (Pango.Font.to_string !current.text_font))); @@ -338,9 +372,67 @@ let configure ?(apply=(fun () -> ())) () = (* Format.printf "in config_font: current.text_font = %s@." (Pango.Font.to_string !current.text_font); *) - !change_font !current.text_font) + !refresh_font_hook ()) true in + + let config_color = + 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 background_label = GMisc.label + ~text:"Background color" + ~packing:(table#attach ~expand:`X ~left:0 ~top:0) () + in + let processed_label = GMisc.label + ~text:"Background color of processed text" + ~packing:(table#attach ~expand:`X ~left:0 ~top:1) () + in + let processing_label = GMisc.label + ~text:"Background color of text being processed" + ~packing:(table#attach ~expand:`X ~left:0 ~top:2) () + in + let () = background_label#set_xalign 0. in + let () = processed_label#set_xalign 0. in + let () = processing_label#set_xalign 0. in + let background_button = GButton.color_button + ~color:(Tags.color_of_string (!current.background_color)) + ~packing:(table#attach ~left:1 ~top:0) () + in + let processed_button = GButton.color_button + ~color:(Tags.get_processed_color ()) + ~packing:(table#attach ~left:1 ~top:1) () + in + let processing_button = GButton.color_button + ~color:(Tags.get_processing_color ()) + ~packing:(table#attach ~left:1 ~top:2) () + in + let reset_button = GButton.button + ~label:"Reset" + ~packing:box#pack () + in + let reset_cb () = + background_button#set_color (Tags.color_of_string "cornsilk"); + processing_button#set_color (Tags.color_of_string "light blue"); + processed_button#set_color (Tags.color_of_string "light green"); + in + let _ = reset_button#connect#clicked ~callback:reset_cb in + let label = "Color configuration" in + let callback () = + !current.background_color <- Tags.string_of_color background_button#color; + !current.processing_color <- Tags.string_of_color processing_button#color; + !current.processed_color <- Tags.string_of_color processed_button#color; + !refresh_background_color_hook (); + Tags.set_processing_color processing_button#color; + Tags.set_processed_color processed_button#color + in + custom ~label box callback true + in + (* let show_toolbar = bool @@ -369,7 +461,7 @@ let configure ?(apply=(fun () -> ())) () = bool ~f:(fun s -> !current.auto_complete <- s; - !auto_complete s) + !auto_complete_hook s) "Auto Complete" !current.auto_complete in @@ -416,44 +508,28 @@ let configure ?(apply=(fun () -> ())) () = "Stop interpreting before the current point" !current.stop_before in - let lax_syntax = - bool - ~f:(fun s -> !current.lax_syntax <- s) - "Relax read-only constraint at end of command" !current.lax_syntax - in - let vertical_tabs = bool - ~f:(fun s -> !current.vertical_tabs <- s) + ~f:(fun s -> !current.vertical_tabs <- s; !refresh_tabs_hook ()) "Vertical tabs" !current.vertical_tabs in let opposite_tabs = bool - ~f:(fun s -> !current.opposite_tabs <- s) + ~f:(fun s -> !current.opposite_tabs <- s; !refresh_tabs_hook ()) "Tabs on opposite side" !current.opposite_tabs in let encodings = combo "File charset encoding " - ~f:(fun s -> - match s with - | "UTF-8" -> - !current.encoding_use_utf8 <- true; - !current.encoding_use_locale <- false - | "LOCALE" -> - !current.encoding_use_utf8 <- false; - !current.encoding_use_locale <- true - | _ -> - !current.encoding_use_utf8 <- false; - !current.encoding_use_locale <- false; - !current.encoding_manual <- s; - ) + ~f:(fun s -> !current.encoding <- (inputenc_of_string s)) ~new_allowed: true - ["UTF-8";"LOCALE";!current.encoding_manual] - (if !current.encoding_use_utf8 then "UTF-8" - else if !current.encoding_use_locale then "LOCALE" else !current.encoding_manual) + ("UTF-8"::"LOCALE":: match !current.encoding with + |Emanual s -> [s] + |_ -> [] + ) + (string_of_inputenc !current.encoding) in let read_project = combo @@ -579,11 +655,11 @@ let configure ?(apply=(fun () -> ())) () = bool ~f:(fun s -> !current.contextual_menus_on_goal <- s; - !contextual_menus_on_goal s) + !contextual_menus_on_goal_hook s) "Contextual menus on goal" !current.contextual_menus_on_goal in - let misc = [contextual_menus_on_goal;auto_complete;stop_before;lax_syntax; + let misc = [contextual_menus_on_goal;auto_complete;stop_before; vertical_tabs;opposite_tabs] in (* ATTENTION !!!!! L'onglet Fonts doit etre en premier pour eviter un bug !!!! @@ -591,6 +667,7 @@ let configure ?(apply=(fun () -> ())) () = let cmds = [Section("Fonts", Some `SELECT_FONT, [config_font]); + Section("Colors", Some `SELECT_COLOR, [config_color]); Section("Files", Some `DIRECTORY, [global_auto_revert;global_auto_revert_delay; auto_save; auto_save_delay; (* auto_save_name*) @@ -604,9 +681,8 @@ let configure ?(apply=(fun () -> ())) () = config_appearance); *) Section("Externals", None, - [cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; cmd_print; - cmd_editor; - cmd_browse;doc_url;library_url]); + [cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; + cmd_print;cmd_editor;cmd_browse;doc_url;library_url]); Section("Tactics Wizard", None, [automatic_tactics]); Section("Shortcuts", Some `PREFERENCES, @@ -618,7 +694,7 @@ let configure ?(apply=(fun () -> ())) () = (* Format.printf "before edit: current.text_font = %s@." (Pango.Font.to_string !current.text_font); *) - let x = edit ~apply ~width:500 "Customizations" cmds in + let x = edit ~apply "Customizations" cmds in (* Format.printf "after edit: current.text_font = %s@." (Pango.Font.to_string !current.text_font); *) -- cgit v1.2.3