From e1cf4df0771d3e07425a9eaa7f796c27348a6f1c Mon Sep 17 00:00:00 2001 From: vgross Date: Mon, 8 Jun 2009 15:44:02 +0000 Subject: Change in UI behaviour : proof folding is now done by double clicking. Delay is configurable through preferences. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12174 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/coqide.ml | 12 ++++++++---- ide/preferences.ml | 14 +++++++++++++- ide/preferences.mli | 1 + 3 files changed, 22 insertions(+), 5 deletions(-) diff --git a/ide/coqide.ml b/ide/coqide.ml index 537da3e43..7ba267c31 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1545,11 +1545,15 @@ object(self) self#recenter_insert end)); - ignore ((input_view :> GText.view)#event#connect#button_release + ignore (let last_left_click = ref 0 in + (input_view :> GText.view)#event#connect#button_release (fun b -> - if GdkEvent.Button.button b = 3 - then let cav = session_notebook#current_term.analyzed_view in - cav#toggle_proof_visibility cav#get_insert; true + let click_time = Int32.to_int (GdkEvent.Button.time b) in + if GdkEvent.Button.button b = 1 + then (if (click_time - !last_left_click < !current.fold_delay_ms) + then (let cav = session_notebook#current_term.analyzed_view in + cav#toggle_proof_visibility cav#get_insert; true) + else (last_left_click := click_time; false)) else false)); diff --git a/ide/preferences.ml b/ide/preferences.ml index 5093c9632..047897883 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -90,6 +90,7 @@ type pref = mutable window_height :int; mutable query_window_width : int; mutable query_window_height : int; + mutable fold_delay_ms : int; (* mutable use_utf8_notation : bool; *) @@ -144,6 +145,7 @@ let (current:pref ref) = window_height = 600; query_window_width = 600; query_window_height = 400; + fold_delay_ms = 400; (* use_utf8_notation = false; *) @@ -214,6 +216,7 @@ let save_pref () = add "window_width" [string_of_int p.window_width] ++ add "query_window_height" [string_of_int p.query_window_height] ++ add "query_window_width" [string_of_int p.query_window_width] ++ + add "fold_delay_ms" [string_of_int p.fold_delay_ms] ++ 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] ++ @@ -275,6 +278,7 @@ let load_pref () = set_int "window_height" (fun v -> np.window_height <- v); 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_int "fold_delay_ms" (fun v -> np.fold_delay_ms <- 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); @@ -408,6 +412,14 @@ let configure ?(apply=(fun () -> ())) () = (string_of_int !current.auto_save_delay) in + let fold_delay_ms = + string + ~f:(fun s -> !current.fold_delay_ms <- + (try int_of_string s with _ -> 300)) + "double click delay to trigger folding (ms)" + (string_of_int !current.fold_delay_ms) + in + let stop_before = bool ~f:(fun s -> !current.stop_before <- s) @@ -570,7 +582,7 @@ let configure ?(apply=(fun () -> ())) () = [automatic_tactics]); Section("Shortcuts", [modifiers_valid; modifier_for_tactics; - modifier_for_templates; modifier_for_display; modifier_for_navigation]); + modifier_for_templates; modifier_for_display; modifier_for_navigation; fold_delay_ms]); Section("Misc", misc)] in diff --git a/ide/preferences.mli b/ide/preferences.mli index 29a7a0040..1f99cd972 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -49,6 +49,7 @@ type pref = mutable window_height : int; mutable query_window_width : int; mutable query_window_height : int; + mutable fold_delay_ms : int; (* mutable use_utf8_notation : bool; *) -- cgit v1.2.3