option pour supprimer les menus contextuels sur les buts

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4299 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 34 insertions, 9 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 05149f184f..825311a621 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -2849,12 +2849,15 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 	);
   ignore(tv2#event#connect#enter_notify
 	   (fun _ -> 
-	      let w = (out_some (get_active_view ()).analyzed_view) in
-	      !push_info "Computing advanced goal's menus";
-	      prerr_endline "Entering Goal Window. Computing Menus....";
-	      w#show_goals_full;
-	      prerr_endline "....Done with Goal menu";
-	      !pop_info();
+	      if !current.contextual_menus_on_goal then
+		begin
+		  let w = (out_some (get_active_view ()).analyzed_view) in
+		  !push_info "Computing advanced goal's menus";
+		  prerr_endline "Entering Goal Window. Computing Menus....";
+		  w#show_goals_full;
+		  prerr_endline "....Done with Goal menu";
+		  !pop_info();
+		end;
 	      false;
 	   ));
   List.iter load files;
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 1c7f37f7f3..5d127f5a0a 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -87,6 +87,7 @@ type pref =
       mutable library_url : string;
 
       mutable show_toolbar : bool;
+      mutable contextual_menus_on_goal : bool;
       mutable window_width : int;
       mutable window_height :int;
       mutable use_utf8_notation : bool;
@@ -134,6 +135,7 @@ let (current:pref ref) =
     library_url = "http://coq.inria.fr/library/";
     
     show_toolbar = true;
+    contextual_menus_on_goal = true;
     window_width = 800;
     window_height = 600; 
     use_utf8_notation = true;
@@ -144,6 +146,8 @@ let change_font = ref (fun f -> ())
 
 let show_toolbar = ref (fun x -> ())
 
+let contextual_menus_on_goal = ref (fun x -> ())
+
 let resize_window = ref (fun () -> ())
 
 let save_pref () =
@@ -187,6 +191,8 @@ let save_pref () =
     add "doc_url" [p.doc_url] ++
     add "library_url" [p.library_url] ++
     add "show_toolbar" [string_of_bool p.show_toolbar] ++
+    add "contextual_menus_on_goal" 
+      [string_of_bool p.contextual_menus_on_goal] ++
     add "window_height" [string_of_int p.window_height] ++
     add "window_width" [string_of_int p.window_width] ++
     Config_lexer.print_file pref_file
@@ -239,6 +245,8 @@ let load_pref () =
     set_hd "doc_url" (fun v -> np.doc_url <- v);
     set_hd "library_url" (fun v -> np.library_url <- v);
     set_bool "show_toolbar" (fun v -> np.show_toolbar <- v);
+    set_bool "contextual_menus_on_goal" 
+      (fun v -> np.contextual_menus_on_goal <- v);
     set_int "window_width" (fun v -> np.window_width <- v);
     set_int "window_height" (fun v -> np.window_height <- v);
 
@@ -422,12 +430,23 @@ let configure () =
     let (w,get_data) = Editable_cells.create !current.automatic_tactics in
     box#add w#coerce;
     custom
-      ~label:"Wizzard tactics to try in order"
+      ~label:"Wizard tactics to try in order"
       box
       (fun () -> let d = get_data () in !current.automatic_tactics <- d)
       true
 
   in
+
+  let contextual_menus_on_goal =
+    bool 
+      ~f:(fun s -> 
+	    !current.contextual_menus_on_goal <- s; 
+	    !contextual_menus_on_goal s) 
+      "Contextual menus on goal" !current.contextual_menus_on_goal
+  in 
+
+  let misc = [contextual_menus_on_goal] in
+   
   let cmds =
     [Section("Fonts",
 	     [config_font]);
@@ -442,11 +461,13 @@ let configure () =
 	     ]);
      Section("Browser",
 	     [cmd_browse;doc_url;library_url]);
-     Section("Tactics Wizzard",
+     Section("Tactics Wizard",
 	     [automatic_tactics]);
      Section("Shortcuts",
 	     [modifiers_valid; modifier_for_tactics;
-	      modifier_for_templates; modifier_for_navigation;mod_msg])]
+	      modifier_for_templates; modifier_for_navigation;mod_msg]);
+     Section("Misc",
+	     misc)]
   in
   match edit ~width:500 "Customizations" cmds
   with 
diff --git a/ide/preferences.mli b/ide/preferences.mli
index abee44d626..d46ad050c3 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -42,6 +42,7 @@ type pref =
       mutable library_url : string;
 
       mutable show_toolbar : bool;
+      mutable contextual_menus_on_goal : bool;
       mutable window_width : int;
       mutable window_height : int;
       mutable use_utf8_notation : bool;