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

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;
 *)