From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Tue, 21 Nov 2006 21:38:49 +0000 Subject: Imported Upstream version 8.1~gamma --- ide/preferences.ml | 34 +++++++++++++++++++++++++++------- 1 file changed, 27 insertions(+), 7 deletions(-) (limited to 'ide/preferences.ml') diff --git a/ide/preferences.ml b/ide/preferences.ml index 4cf9627c..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 8920 2006-06-08 09:12:48Z notin $ *) +(* $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,9 +120,9 @@ 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 = Options.browser_cmd_fmt; @@ -143,7 +145,9 @@ let (current:pref ref) = (* use_utf8_notation = false; *) - auto_complete = false + auto_complete = false; + stop_before = true; + lax_syntax = true } @@ -205,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 _ -> ()); @@ -257,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); @@ -385,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 " @@ -476,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) *) -- cgit v1.2.3