changement menu et toolbar

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

5 files changed, 239 insertions, 131 deletions

diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index 3f773b79c..444495ee1 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -30,11 +30,34 @@ class command_window () =
   in
   let accel_group = GtkData.AccelGroup.create () in
   let vbox = GPack.vbox ~homogeneous:false ~packing:window#add () in
+(*
   let menubar = GMenu.menu_bar ~packing:vbox#pack () in
+*)
+(*
+  let handle = GBin.handle_box 
+		 ~show:true
+		 ~handle_position:`LEFT
+		 ~snap_edge:`LEFT
+		 ~packing:vbox#pack
+		 ()
+  in
+*)
+  let toolbar = GButton.toolbar 
+		  ~orientation:`HORIZONTAL 
+		  ~style:`ICONS
+		  ~tooltips:true 
+		  ~packing:(vbox#pack 
+			       ~expand:false
+			       ~fill:false)
+		  ()
+  in
+(*
   let factory = new GMenu.factory menubar
   in
+*)
+(*
   let accel_group = factory#accel_group in
-
+*)
   let notebook = GPack.notebook ~scrollable:true 
 		   ~packing:(vbox#pack 
 			       ~expand:true
@@ -42,18 +65,52 @@ class command_window () =
 			    ) 
 		   ()
   in
+(*
   let hide_menu = factory#add_item "_Hide Window" 
 		    ~callback:window#misc#hide
+*)
+  let _ = 
+    toolbar#insert_button
+      ~tooltip:"Hide Window"
+      ~text:"Hide Window"
+      ~icon:(Ideutils.stock_to_widget ~size:`LARGE_TOOLBAR `CLOSE)
+      ~callback:window#misc#hide
+      ()
   in
+(*
   let new_page_menu = factory#add_item "_New Page" in
+*)
+  let new_page_menu = 
+    toolbar#insert_button
+      ~tooltip:"New Page"
+      ~text:"New Page"
+      ~icon:(Ideutils.stock_to_widget ~size:`LARGE_TOOLBAR `NEW)
+(*
+      ~callback:window#misc#hide
+*)
+      ()
+  in
+
+(*
   let kill_page_menu = 
     factory#add_item "_Kill Page" 
       ~callback:
       (fun () -> notebook#remove_page notebook#current_page)
   in
+*)
+  let kill_page_menu = 
+    toolbar#insert_button
+      ~tooltip:"Kill Page"
+      ~text:"Kill Page"
+      ~icon:(Ideutils.stock_to_widget ~size:`LARGE_TOOLBAR `DELETE)
+      ~callback:(fun () -> notebook#remove_page notebook#current_page)
+      ()
+  in
 object(self)
   val window = window
+(*
   val menubar = menubar
+*)
   val new_page_menu = new_page_menu
   val notebook = notebook
   method window = window
@@ -122,7 +179,7 @@ object(self)
     self#window#present ()
 
   initializer 
-    ignore (new_page_menu#connect#activate self#new_command);
+    ignore (new_page_menu#connect#clicked self#new_command);
     ignore (window#event#connect#delete (fun _ -> window#misc#hide(); true));
 end
 
diff --git a/ide/coq.ml b/ide/coq.ml
index 1f0efbe71..0de38431a 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -48,13 +48,18 @@ let init () =
 let i = ref 0
 
 let version () =
-  Printf.sprintf "The Coq Proof Assistant, version %s (%s)\nConfigured on %s\nThis is the %s version (%s is the best one) for architecture %s on system %s
-Gtk version is %s"
+  Printf.sprintf 
+    "The Coq Proof Assistant, version %s (%s)\
+   \nConfigured on %s\
+   \nArchitecture %s running %s operating system\
+   \nGtk version is %s\
+   \nThis is the %s version (%s is the best one for this architecture and OS)\
+   \n"
     Coq_config.version Coq_config.date Coq_config.compile_date
-    (if Mltop.get () = Mltop.Native then "native" else "byte") 
-    (if Coq_config.best="opt" then "native" else "byte") 
     Coq_config.arch Sys.os_type
     (let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z)
+    (if Mltop.get () = Mltop.Native then "native" else "bytecode") 
+    (if Coq_config.best="opt" then "native" else "bytecode") 
 
 let is_in_coq_lib dir = 
   prerr_endline ("Is it a coq theory ? : "^dir);
diff --git a/ide/coqide.ml b/ide/coqide.ml
index d4bd7def2..ea1c88958 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1369,7 +1369,7 @@ Please restart and report NOW.";
 		   let set_goal i (s,t) = 
 		     let gnb = string_of_int i in
 		     let s = gnb ^":"^s in
-		     let t' = gnb ^": Progress "^t in
+		     let t' = gnb ^": progress "^t in
 		     let t'' = gnb ^": "^t in
 		     c#set
 		       ("Goal "^gnb)
@@ -1381,7 +1381,7 @@ Please restart and report NOW.";
 		     c#set
 		       "Goal 1"
 		       s 
-		       (fun () -> try_interptac ("Progress "^t))
+		       (fun () -> try_interptac ("progress "^t))
 		       (fun () -> self#insert_command t t)
 		   in
 		   begin match current_gls with 
@@ -1723,6 +1723,7 @@ let main files =
   let menubar = GMenu.menu_bar ~packing:vbox#pack () in
 
   (* Tearable Toolbar *)
+(*
   let handle = GBin.handle_box 
 		 ~show:!current.show_toolbar
 		 ~handle_position:`LEFT
@@ -1730,15 +1731,21 @@ let main files =
 		 ~packing:vbox#pack
 		 ()
   in
+*)
   let toolbar = GButton.toolbar 
 		  ~orientation:`HORIZONTAL 
-		  ~style:`BOTH
+		  ~style:`ICONS
 		  ~tooltips:true 
-		  ~packing:handle#add
+		  ~packing:(* handle#add *)
+		     (vbox#pack ~expand:false ~fill:false)
 		  ()
   in
+(*
   show_toolbar := 
   (fun b -> if b then handle#misc#show () else handle#misc#hide ());
+*)
+  show_toolbar := 
+  (fun b -> if b then toolbar#misc#show () else toolbar#misc#hide ());
 
   let factory = new GMenu.factory ~accel_path:"<CoqIde MenuBar>/" menubar in
   let accel_group = factory#accel_group in
@@ -2003,6 +2010,7 @@ let main files =
   *)
   (* File/Quit Menu *)
   let quit_f () =
+    save_pref();
     if has_something_to_save () then 
       match (GToolbox.question_box ~title:"Quit"
 	       ~buttons:["Save Named Buffers and Quit";
@@ -2057,13 +2065,6 @@ let main files =
 		 with _ -> prerr_endline "EMIT PASTE FAILED")));
   ignore (edit_f#add_separator ());
 
-  ignore(edit_f#add_item "Complete" ~key:GdkKeysyms._slash ~callback:
-	 (do_if_not_computing 
-	    (fun () -> 
-	       ignore (
-		 let av = out_some ((get_current_view()).analyzed_view) in 
-		 av#complete_at_offset (av#get_insert)#offset
-	    ))));
 
 (*
    let toggle_auto_complete_i = 
@@ -2089,6 +2090,7 @@ let main files =
   let search_ib = edit_f#add_item "Search _backward"
 		    ~key:GdkKeysyms._less
   in
+(*
   let complete_i = edit_f#add_item "_Complete"
 		     ~key:GdkKeysyms._comma
 		     ~callback:
@@ -2101,7 +2103,16 @@ let main files =
 			))
   in
   complete_i#misc#set_state `INSENSITIVE;
+*)
   
+  ignore(edit_f#add_item "Complete" ~key:GdkKeysyms._slash ~callback:
+	 (do_if_not_computing 
+	    (fun () -> 
+	       ignore (
+		 let av = out_some ((get_current_view()).analyzed_view) in 
+		 av#complete_at_offset (av#get_insert)#offset
+	    ))));
+
   to_do_on_page_switch := 
   (fun i -> 
      prerr_endline ("Switching to tab "^(string_of_int i));
@@ -2109,6 +2120,54 @@ let main files =
      read_only_i#set_active v#read_only
   )::!to_do_on_page_switch;
   
+
+  ignore(edit_f#add_separator ());
+  (* Preferences *)
+  let reset_revert_timer () =
+    disconnect_revert_timer ();
+    if !current.global_auto_revert then 
+      revert_timer := Some
+	(GMain.Timeout.add ~ms:!current.global_auto_revert_delay 
+	   ~callback:
+	   (fun () -> 
+	      do_if_not_computing (fun () -> revert_f ()) ();
+	      true))
+  in reset_revert_timer (); (* to enable statup preferences timer *)
+
+  let auto_save_f () = 
+    Vector.iter 
+      (function 
+	   {view = view ; analyzed_view = Some av} as full -> 
+	     (try 
+		av#auto_save
+	      with _ -> ())
+	 | _ -> ()
+      )  
+      input_views
+  in
+
+  let reset_auto_save_timer () =
+    disconnect_auto_save_timer ();
+    if !current.auto_save then 
+      auto_save_timer := Some
+	(GMain.Timeout.add ~ms:!current.auto_save_delay 
+	   ~callback:
+	   (fun () -> 
+	      do_if_not_computing (fun () -> auto_save_f ()) ();
+	      true))
+  in reset_auto_save_timer (); (* to enable statup preferences timer *)
+
+
+  let edit_prefs_m =
+    edit_f#add_item "_Preferences"
+      ~callback:(fun () -> configure ();reset_revert_timer ())
+  in
+(*
+  let save_prefs_m =
+    configuration_factory#add_item "_Save preferences"
+      ~callback:(fun () -> save_pref ())
+  in
+*)
   (* Navigation Menu *)
   let navigation_menu =  factory#add_submenu "_Navigation" in
   let navigation_factory = 
@@ -2144,19 +2203,19 @@ let main files =
 	      ())
   in
   add_to_menu_toolbar "_Interrupt"
-    ~tooltip:"Interrupt"    
+    ~tooltip:"Interrupt computations"    
     ~key:GdkKeysyms._Break 
     ~callback:break
     `STOP
   ;
   add_to_menu_toolbar 
     "_Forward" 
-    ~tooltip:"Forward" 
+    ~tooltip:"Forward one command" 
     ~key:GdkKeysyms._Down 
     ~callback:(do_or_activate (fun a -> a#process_next_phrase true true))
     `GO_DOWN;
   add_to_menu_toolbar "_Backward"
-    ~tooltip:"Backward" 
+    ~tooltip:"Backward one command" 
     ~key:GdkKeysyms._Up
     ~callback:(do_or_activate (fun a -> a#undo_last_step))
     `GO_UP;
@@ -2176,19 +2235,19 @@ let main files =
 *)
   add_to_menu_toolbar 
     "_Go to" 
-    ~tooltip:"Go to" 
+    ~tooltip:"Go to cursor" 
     ~key:GdkKeysyms._Right
     ~callback:(do_or_activate (fun a-> a#go_to_insert))
-    `GOTO_LAST;
+    `JUMP_TO;
   add_to_menu_toolbar 
     "_Start" 
-    ~tooltip:"Start" 
+    ~tooltip:"Go to start" 
     ~key:GdkKeysyms._Home
     ~callback:(do_or_activate (fun a -> a#reset_initial))
     `GOTO_TOP;
   add_to_menu_toolbar 
     "_End" 
-    ~tooltip:"End" 
+    ~tooltip:"Go to end" 
     ~key:GdkKeysyms._End
     ~callback:(do_or_activate (fun a -> a#process_until_end_or_error))
     `GOTO_BOTTOM;
@@ -2208,53 +2267,57 @@ let main files =
   in
   let do_if_active f = do_if_not_computing (do_if_active_raw f) in
 
-  ignore (tactics_factory#add_item "_Blaster"
+  let blaster_i = 
+    tactics_factory#add_item "_Blaster"
 	    ~key:GdkKeysyms._b
 	    ~callback: (do_if_active_raw (fun a -> a#blaster ()))
 	    (* Custom locking mechanism! *)
-	 )
-	 ;
-
-  ignore (tactics_factory#add_item "_Auto" 
+  in
+  blaster_i#misc#set_state `INSENSITIVE;
+ 
+  ignore (tactics_factory#add_item "_auto" 
 	    ~key:GdkKeysyms._a
-	    ~callback:(do_if_active (fun a -> a#insert_command "Progress Auto.\n" "Auto.\n"))
+	    ~callback:(do_if_active (fun a -> a#insert_command "progress auto.\n" "auto.\n"))
 	 );
-  ignore (tactics_factory#add_item "_Auto with *"
+  ignore (tactics_factory#add_item "_auto with *"
 	    ~key:GdkKeysyms._asterisk
 	    ~callback:(do_if_active (fun a -> a#insert_command 
-				       "Progress Auto with *.\n"
-				       "Auto with *.\n")));
-  ignore (tactics_factory#add_item "_EAuto"
+				       "progress auto with *.\n"
+				       "auto with *.\n")));
+  ignore (tactics_factory#add_item "_eauto"
 	    ~key:GdkKeysyms._e
 	    ~callback:(do_if_active (fun a -> a#insert_command 
-				       "Progress EAuto.\n"
-				       "EAuto.\n"))
+				       "progress eauto.\n"
+				       "eauto.\n"))
 	 );
-  ignore (tactics_factory#add_item "_EAuto with *"
+  ignore (tactics_factory#add_item "_eauto with *"
 	    ~key:GdkKeysyms._ampersand
 	    ~callback:(do_if_active (fun a -> a#insert_command 
-				       "Progress EAuto with *.\n" 
-				       "EAuto with *.\n"))
+				       "progress eauto with *.\n" 
+				       "eauto with *.\n"))
 	 );
-  ignore (tactics_factory#add_item "_Intuition"
+  ignore (tactics_factory#add_item "_intuition"
 	    ~key:GdkKeysyms._i
-	    ~callback:(do_if_active (fun a -> a#insert_command "Progress Intuition.\n" "Intuition.\n"))
+	    ~callback:(do_if_active (fun a -> a#insert_command 
+					 "progress intuition.\n" 
+					 "intuition.\n"))
 	 );
-  ignore (tactics_factory#add_item "_Omega"
+  ignore (tactics_factory#add_item "_omega"
 	    ~key:GdkKeysyms._o
-	    ~callback:(do_if_active (fun a -> a#insert_command "Omega.\n" "Omega.\n"))
+	    ~callback:(do_if_active (fun a -> a#insert_command 
+					 "omega.\n" "omega.\n"))
 	 );
-  ignore (tactics_factory#add_item "_Simpl"
+  ignore (tactics_factory#add_item "_simpl"
 	    ~key:GdkKeysyms._s
-	    ~callback:(do_if_active (fun a -> a#insert_command "Progress Simpl.\n" "Simpl.\n" ))
+	    ~callback:(do_if_active (fun a -> a#insert_command "progress simpl.\n" "simpl.\n" ))
 	 );
-  ignore (tactics_factory#add_item "_Tauto"
+  ignore (tactics_factory#add_item "_tauto"
 	    ~key:GdkKeysyms._p
-	    ~callback:(do_if_active (fun a -> a#insert_command "Tauto.\n" "Tauto.\n" ))
+	    ~callback:(do_if_active (fun a -> a#insert_command "tauto.\n" "tauto.\n" ))
 	 );
-  ignore (tactics_factory#add_item "_Trivial"
+  ignore (tactics_factory#add_item "_trivial"
 	    ~key:GdkKeysyms._v
-	    ~callback:(do_if_active( fun a -> a#insert_command "Progress Trivial.\n"  "Trivial.\n" ))
+	    ~callback:(do_if_active( fun a -> a#insert_command "progress trivial.\n"  "trivial.\n" ))
 	 );
 
 
@@ -2358,6 +2421,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 		  ignore (view#buffer#insert_interactive text))))
   in
   ignore (templates_factory#add_separator ());
+(*
   List.iter (add_simple_template templates_factory)
     [ "_Auto", "Auto ";
       "_Auto with *", "Auto with * ";
@@ -2370,6 +2434,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
       "Tri_vial", "Trivial ";
     ];
   ignore (templates_factory#add_separator ());
+*)
   List.iter 
     (fun l -> 
        match l with 
@@ -2400,12 +2465,6 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
   in
   
   (* Command/Show commands *)
-  let queries_show_m = queries_factory#add_item 
-			  "_Show Query Window"
-			  ~key:GdkKeysyms._F12
-			  ~callback:(Command_windows.command_window ())
-			  #window#present
-  in  
   let _ = 
     queries_factory#add_item "_SearchAbout " ~key:GdkKeysyms._F2
       ~callback:(fun () -> let term = get_current_word () in
@@ -2432,9 +2491,9 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
   in
 
   (* Externals *)
-  let externals_menu =  factory#add_submenu "_Externals" in
+  let externals_menu =  factory#add_submenu "_Compile" in
   let externals_factory = new GMenu.factory externals_menu 
-			    ~accel_path:"<CoqIde MenuBar>/Externals/"
+			    ~accel_path:"<CoqIde MenuBar>/Compile/"
 			    ~accel_group in
   
   (* Command/Compile Menu *)
@@ -2460,7 +2519,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 	  av#insert_message res
 	end
   in
-  let compile_m = externals_factory#add_item "_Compile" ~callback:compile_f in
+  let compile_m = externals_factory#add_item "_Compile Buffer" ~callback:compile_f in
 
   (* Command/Make Menu *)
   let make_f () =
@@ -2481,56 +2540,29 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
     !flash_info 
       (!current.cmd_coqmakefile ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
   in
-  let _ = externals_factory#add_item "_Make Makefile" ~callback:coq_makefile_f 
+  let _ = externals_factory#add_item "_Make makefile" ~callback:coq_makefile_f 
   in
-  (* Configuration Menu *)
-  let reset_revert_timer () =
-    disconnect_revert_timer ();
-    if !current.global_auto_revert then 
-      revert_timer := Some
-	(GMain.Timeout.add ~ms:!current.global_auto_revert_delay 
-	   ~callback:
-	   (fun () -> 
-	      do_if_not_computing (fun () -> revert_f ()) ();
-	      true))
-  in reset_revert_timer (); (* to enable statup preferences timer *)
-
-  let auto_save_f () = 
-    Vector.iter 
-      (function 
-	   {view = view ; analyzed_view = Some av} as full -> 
-	     (try 
-		av#auto_save
-	      with _ -> ())
-	 | _ -> ()
-      )  
-      input_views
+  (* Windows Menu *)
+  let configuration_menu = factory#add_submenu "_Windows" in
+  let configuration_factory = new GMenu.factory configuration_menu ~accel_path:"<CoqIde MenuBar>/Windows" ~accel_group
   in
-
-  let reset_auto_save_timer () =
-    disconnect_auto_save_timer ();
-    if !current.auto_save then 
-      auto_save_timer := Some
-	(GMain.Timeout.add ~ms:!current.auto_save_delay 
-	   ~callback:
-	   (fun () -> 
-	      do_if_not_computing (fun () -> auto_save_f ()) ();
-	      true))
-  in reset_auto_save_timer (); (* to enable statup preferences timer *)
-
-  let configuration_menu = factory#add_submenu "Confi_guration" in
-  let configuration_factory = new GMenu.factory configuration_menu ~accel_path:"<CoqIde MenuBar>/Configuration" ~accel_group
-  in
-  let edit_prefs_m =
-    configuration_factory#add_item "Edit _preferences"
-      ~callback:(fun () -> configure ();reset_revert_timer ())
-  in
-  let save_prefs_m =
-    configuration_factory#add_item "_Save preferences"
-      ~callback:(fun () -> save_pref ())
+  let queries_show_m = 
+    configuration_factory#add_item 
+      "Show _Query Window"
+      (*
+	~key:GdkKeysyms._F12
+      *)
+      ~callback:(Command_windows.command_window ())#window#present
+  in  
+  let toolbar_show_m = 
+    configuration_factory#add_item 
+      "Show/Hide _Toolbar"	       
+      ~callback:(fun () ->  
+		   !current.show_toolbar <- not !current.show_toolbar; 
+		   !show_toolbar !current.show_toolbar) 
   in
   let detach_menu = configuration_factory#add_item 
-		      "_Detach Scripting Window"
+		      "Detach _Script Window"
 		      ~callback:
 		      (do_if_not_computing
 			 (fun () -> 
@@ -2548,7 +2580,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 			 ))
   in
   let detach_current_view = configuration_factory#add_item 
-			      "De_tach View"
+			      "Detach _View"
 			      ~callback:
 			      (do_if_not_computing
 				 (fun () -> 
@@ -2874,14 +2906,14 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
        b#insert ~iter:b#start_iter "\t\t";
      with _ -> ());
     b#insert 
-      "\n\tCoqIDE: a Gtk2 interface for Coq\n\
-      \nMain author  : Benjamin Monate\
-      \nContributors : Jean-Christophe Filliâtre\
-      \n               Pierre Letouzey, Claude Marché\n\
-      \nFeature wish or bug report: use Web interface\n\
-      \n\thttp://coq.inria.fr/bin/coq-bugs\n\
-      \nVersion information\
-      \n-------------------\n";
+      "\nCoqIDE: an Integrated Development Environment for Coq\n\
+       \nMain author  : Benjamin Monate\
+       \nContributors : Jean-Christophe Filliâtre\
+       \n               Pierre Letouzey, Claude Marché\n\
+       \nFeature wish or bug report: use Web interface\n\
+       \n\thttp://coq.inria.fr/bin/coq-bugs\n\
+       \nVersion information\
+       \n-------------------\n";
     b#insert ((Coq.version ()))
       
   in
@@ -2915,7 +2947,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
   tv2#misc#modify_font !current.text_font; 
   tv3#misc#modify_font !current.text_font;
   ignore (about_m#connect#activate 
-	    ~callback:(fun () -> about tv3#buffer));
+	    ~callback:(fun () -> tv2#buffer#set_text ""; about tv2#buffer));
   ignore (faq_m#connect#activate 
 	    ~callback:(fun () -> 
 			 load (Filename.concat lib_ide "FAQ")));
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 2bc92eeb5..64bb9c488 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -90,6 +90,8 @@ type pref =
       mutable contextual_menus_on_goal : bool;
       mutable window_width : int;
       mutable window_height :int;
+      mutable query_window_width : int;
+      mutable query_window_height : int;
 (*
       mutable use_utf8_notation : bool;
 *)
@@ -100,7 +102,7 @@ let (current:pref ref) =
   ref {
     cmd_coqc = "coqc";
     cmd_make = "make";
-    cmd_coqmakefile = "coq_makefile -o Makefile *.v";
+    cmd_coqmakefile = "coq_makefile -o makefile *.v";
     cmd_coqdoc = "coqdoc -q -g";
     cmd_print = "lpr";
 
@@ -115,12 +117,12 @@ let (current:pref ref) =
     encoding_use_utf8 = false;
     encoding_manual = "ISO_8859-1";
 
-    automatic_tactics = ["Progress Trivial.","Trivial.";
-			 "Tauto.","Tauto.";
-			 "Progress Auto.","Auto.";
-			 "Omega.","Omega.";
-			 "Progress Auto with *.","Auto with *.";
-			 "Progress Intuition.","Intuition.";
+    automatic_tactics = ["progress trivial.","trivial.";
+			 "tauto.","tauto.";
+			 "progress auto.","auto.";
+			 "omega.","omega.";
+			 "progress auto with *.","auto with *.";
+			 "progress intuition.","intuition.";
 			];
     
     modifier_for_navigation = [`CONTROL; `MOD1];
@@ -140,6 +142,8 @@ let (current:pref ref) =
     contextual_menus_on_goal = true;
     window_width = 800;
     window_height = 600; 
+    query_window_width = 600;
+    query_window_height = 400;
 (*
     use_utf8_notation = false;
 *)
@@ -202,6 +206,8 @@ let save_pref () =
       [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] ++
+    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] ++
     Config_lexer.print_file pref_file
   with _ -> prerr_endline "Could not save preferences."
@@ -257,6 +263,8 @@ let load_pref () =
       (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);
+    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);
     current := np
   with e -> 
@@ -295,6 +303,7 @@ let configure () =
 	 !change_font !current.text_font)
       true
   in
+(*
   let show_toolbar = 
     bool 
       ~f:(fun s -> 
@@ -317,6 +326,7 @@ let configure () =
       "Window width" 
       (string_of_int !current.window_width)
   in  
+*)
   let auto_complete = 
     bool 
       ~f:(fun s -> 
@@ -333,8 +343,9 @@ let configure () =
       "Use Unicode Notation: " !current.use_utf8_notation
   in
 *)  
+(*
   let config_appearance = [show_toolbar; window_width; window_height] in
-
+*)
   let global_auto_revert = 
     bool 
       ~f:(fun s -> !current.global_auto_revert <- s) 
@@ -463,19 +474,20 @@ let configure () =
   let misc = [contextual_menus_on_goal;auto_complete] in
    
   let cmds =
-    [Section("Fonts",
-	     [config_font]);
-     Section("Appearance",
-	     config_appearance);
-     Section("Commands",
-	     [cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; cmd_print]);
-     Section("Files",
+    [Section("Files",
 	     [global_auto_revert;global_auto_revert_delay;
 	     auto_save; auto_save_delay; (* auto_save_name*)
 	     encodings;
 	     ]);
-     Section("Browser",
-	     [cmd_browse;doc_url;library_url]);
+     Section("Fonts",
+	     [config_font]);
+(*
+     Section("Appearance",
+	     config_appearance);
+*)
+     Section("Externals",
+	     [cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; cmd_print;
+	      cmd_browse;doc_url;library_url]);
      Section("Tactics Wizard",
 	     [automatic_tactics]);
      Section("Shortcuts",
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 5cf26c90e..f6d163cb0 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -45,6 +45,8 @@ type pref =
       mutable contextual_menus_on_goal : bool;
       mutable window_width : int;
       mutable window_height : int;
+      mutable query_window_width : int;
+      mutable query_window_height : int;
 (*
       mutable use_utf8_notation : bool;
 *)