diff options
Diffstat (limited to 'ide/preferences.ml')
-rw-r--r-- | ide/preferences.ml | 79 |
1 files changed, 38 insertions, 41 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml index 8743b99b..c01fa602 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: preferences.ml,v 1.27.2.2 2004/07/16 19:30:20 herbelin Exp $ *) +(* $Id: preferences.ml 9350 2006-11-07 15:04:42Z notin $ *) open Configwin open Printf @@ -93,7 +93,9 @@ type pref = mutable use_utf8_notation : bool; *) mutable auto_complete : bool; - } + mutable stop_before : bool; + mutable lax_syntax : bool; +} let (current:pref ref) = ref { @@ -118,15 +120,12 @@ let (current:pref ref) = "auto with *"; "intuition" ]; modifier_for_navigation = [`CONTROL; `MOD1]; - modifier_for_templates = [`MOD4]; + modifier_for_templates = [`CONTROL; `SHIFT]; modifier_for_tactics = [`CONTROL; `MOD1]; - modifiers_valid = [`SHIFT; `CONTROL; `MOD1; `MOD4]; + modifiers_valid = [`SHIFT; `CONTROL; `MOD1]; - cmd_browse = - if Sys.os_type = "Win32" - then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE ", "" - else "netscape -remote \"OpenURL(", ")\""; + cmd_browse = Options.browser_cmd_fmt; cmd_editor = if Sys.os_type = "Win32" then "NOTEPAD ", "" @@ -146,7 +145,9 @@ let (current:pref ref) = (* use_utf8_notation = false; *) - auto_complete = false + auto_complete = false; + stop_before = true; + lax_syntax = true } @@ -183,8 +184,7 @@ let save_pref () = add "encoding_use_utf8" [string_of_bool p.encoding_use_utf8] ++ add "encoding_manual" [p.encoding_manual] ++ - add "automatic_tactics" - (List.rev p.automatic_tactics) ++ + add "automatic_tactics" p.automatic_tactics ++ add "cmd_print" [p.cmd_print] ++ add "modifier_for_navigation" (List.map mod_to_str p.modifier_for_navigation) ++ @@ -209,9 +209,11 @@ let save_pref () = add "query_window_height" [string_of_int p.query_window_height] ++ 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] ++ Config_lexer.print_file pref_file with _ -> prerr_endline "Could not save preferences." - + let load_pref () = (try GtkData.AccelMap.load accel_file with _ -> ()); @@ -261,6 +263,8 @@ let load_pref () = set_int "query_window_width" (fun v -> np.query_window_width <- v); 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); current := np; (* Format.printf "in laod_pref: current.text_font = %s@." (Pango.Font.to_string !current.text_font); @@ -269,6 +273,13 @@ let load_pref () = prerr_endline ("Could not load preferences ("^ (Printexc.to_string e)^").") +let split_string_format s = + try + let i = Util.string_index_from s 0 "%s" in + let pre = (String.sub s 0 i) in + let post = String.sub s (i+2) (String.length s - i - 2) in + pre,post + with Not_found -> s,"" let configure () = let cmd_coqc = @@ -382,6 +393,18 @@ let configure () = (string_of_int !current.auto_save_delay) in + let stop_before = + bool + ~f:(fun s -> !current.stop_before <- s) + "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 encodings = combo "File charset encoding " @@ -439,40 +462,14 @@ let configure () = let cmd_editor = string - ~f:(fun s -> - !current.cmd_editor <- - try - let i = String.index s '%' in - let pre = (String.sub s 0 i) in - if String.length s - 1 = i then - pre,"" - else - let post = String.sub s (i+2) (String.length s - i - 2) in - prerr_endline pre; - prerr_endline post; - pre,post - with Not_found -> s,"" - ) + ~f:(fun s -> !current.cmd_editor <- split_string_format s) ~help:"(%s for file name)" "External editor" ((fst !current.cmd_editor)^"%s"^(snd !current.cmd_editor)) in let cmd_browse = string - ~f:(fun s -> - !current.cmd_browse <- - try - let i = String.index s '%' in - let pre = (String.sub s 0 i) in - if String.length s - 1 = i then - pre,"" - else - let post = String.sub s (i+2) (String.length s - i - 2) in - prerr_endline pre; - prerr_endline post; - pre,post - with Not_found -> s,"" - ) + ~f:(fun s -> !current.cmd_browse <- split_string_format s) ~help:"(%s for url)" " Browser" ((fst !current.cmd_browse)^"%s"^(snd !current.cmd_browse)) @@ -499,7 +496,7 @@ let configure () = "Contextual menus on goal" !current.contextual_menus_on_goal in - let misc = [contextual_menus_on_goal;auto_complete] in + let misc = [contextual_menus_on_goal;auto_complete;stop_before;lax_syntax] in (* ATTENTION !!!!! L'onglet Fonts doit etre en premier pour eviter un bug !!!! (shame on Benjamin) *) |