*** empty log message ***

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

3 files changed, 55 insertions, 22 deletions

diff --git a/ide/.coqiderc b/ide/.coqiderc
index 89967ce36..68d0a56c4 100644
--- a/ide/.coqiderc
+++ b/ide/.coqiderc
@@ -5,6 +5,7 @@ binding "text" {
 		}
   bind "<ctrl>x" { }
   bind "F13" {"insert-at-cursor" ("∀")}
+  bind "F14" {"insert-at-cursor" ("∃")}
 }
 class "GtkTextView" binding "text"
 
diff --git a/ide/FAQ b/ide/FAQ
index a410dbe64..e6e022973 100644
--- a/ide/FAQ
+++ b/ide/FAQ
@@ -19,24 +19,33 @@ Q3) How to enable antialiased fonts?
 R3) Set the GDK_USE_XFT variable to 1.
 
 Q4) How can use Forall and Exists pretty symbols ?
-R4) Thanks to the Notation features in Coq, you just need to paste these
+R4) Thanks to the Notation features in Coq, you just need to insert these
 	lines in your Coq Buffer :
 ======================================================================
 Notation "∀ x : t | P" := (x:t)P (at level 1, x,t,P at level 10).
-Notation "~ x : t | P" := (EXT x:t|P) (at level 1, x,t,P at level 10).
+Notation "∃ x : t | P" := (EXT x:t|P) (at level 1, x,t,P at level 10).
 ======================================================================
-Then you need an input method for these symbols.
--First solution : type "<CONTROL>2200" to enter a forall. 2200 is the 
-	hexadecimal code for forall in unicode charts.
-	2203 is for exists. See http://www.unicode.org for more.
+Copy/Paste might not work. You need to load a file containing these lines or to enter 
+the "∀" using an input method. As a convenience, you may put these lines in
+a utf8.v file and start coqide with : 
+	coqide -l utf8.v
+
 
--Second solution : rebind "<AltGr>a" to forall. Under X11, you need to 
-	use 
+Input Methods:
+-First solution : type "<CONTROL><SHIFT>2200" to enter a forall in the script widow. 
+	2200 is the hexadecimal code for forall in unicode charts and is encoded as "∀"	
+	in UTF-8.
+	2203 is for exists. See http://www.unicode.org for more.
+-Second solution : rebind "<AltGr>a" to forall and "<AltGr>e" to exists. Under X11, you need to 
+	use something like
 		xmodmap -e "keycode  24 = a A F13 F13" 
+		xmodmap -e "keycode  26 = e E F14 F14" 
 	and then to add   
 		bind "F13" {"insert-at-cursor" ("∀")}
+		bind "F14" {"insert-at-cursor" ("∃")}
 	to your "binding "text"" section in .coqiderc. 
 	The strange ("∀") argument is the UTF-8 encoding for
 	0x2200. It is computed by lablgtk2 by 
 		Glib.Utf8.from_unichar 0x2200;;
-	Further symbols can be found on higher Fxx key symbols.
+	Further symbols can be bound on higher Fxx key symbols.
+
diff --git a/ide/coqide.ml b/ide/coqide.ml
index e8b28ec44..01331ef9b 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1611,14 +1611,45 @@ let main files =
   
   (* Commands Menu *)
   let commands_menu =  factory#add_submenu "_Commands" in
-  let commands_factory = new GMenu.factory commands_menu ~accel_group in
+  let commands_factory = new GMenu.factory commands_menu ~accel_group
+			   ~accel_modi:[]
+  in
   
   (* Command/Show commands *)
   let commands_show_m = commands_factory#add_item 
-			  "_Show commands" 
+			  "_Show Window"
+			  ~key:GdkKeysyms._F12
 			  ~callback:(Command_windows.command_window ())
 			  #window#present
   in  
+  let _ = 
+    commands_factory#add_item "_SearchAbout " ~key:GdkKeysyms._F2
+      ~callback:(fun () -> let term = get_current_word () in
+		 (Command_windows.command_window ())#new_command
+		 ~command:"SearchAbout"
+		   ~term 
+		   ())
+  in
+  let _ = 
+    commands_factory#add_item "_Check " ~key:GdkKeysyms._F3
+      ~callback:(fun () -> let term = get_current_word () in
+		 (Command_windows.command_window ())#new_command
+		 ~command:"Check"
+		   ~term 
+		   ())
+  in
+  let _ = 
+    commands_factory#add_item "_Print " ~key:GdkKeysyms._F4
+      ~callback:(fun () -> let term = get_current_word () in
+		 (Command_windows.command_window ())#new_command
+		 ~command:"Print"
+		   ~term 
+		   ())
+  in
+
+  (* Externals *)
+  let externals_menu =  factory#add_submenu "_Externals" in
+  let externals_factory = new GMenu.factory externals_menu ~accel_group in
   
   (* Command/Compile Menu *)
   let compile_f () =
@@ -1636,7 +1667,7 @@ let main files =
 	    av#process_until_end_or_error
 	  end
   in
-  let compile_m = commands_factory#add_item "_Compile" ~callback:compile_f in
+  let compile_m = externals_factory#add_item "_Compile" ~callback:compile_f in
 
   (* Command/Make Menu *)
   let make_f () =
@@ -1644,7 +1675,7 @@ let main files =
     let c = Sys.command !current.cmd_make in
     !flash_info (!current.cmd_make ^ if c = 0 then " succeeded" else " failed")
   in
-  let make_m = commands_factory#add_item "_Make" ~callback:make_f in
+  let make_m = externals_factory#add_item "_Make" ~callback:make_f in
   
   (* Command/CoqMakefile Menu*)
   let coq_makefile_f () =
@@ -1652,7 +1683,7 @@ let main files =
     !flash_info 
       (!current.cmd_coqmakefile ^ if c = 0 then " succeeded" else " failed")
   in
-  let _ = commands_factory#add_item "_Make Makefile" ~callback:coq_makefile_f 
+  let _ = externals_factory#add_item "_Make Makefile" ~callback:coq_makefile_f 
   in
 
   (* Configuration Menu *)
@@ -1724,14 +1755,6 @@ let main files =
   let av = out_some ((get_current_view ()).analyzed_view) in 
 		 av#help_for_keyword ())
   in
-  let _ = 
-    help_factory#add_item "_SearchAbout " ~key:GdkKeysyms._F2
-      ~callback:(fun () -> let term = get_current_word () in
-		(Command_windows.command_window ())#new_command
-		 ~command:"SearchAbout"
-		  ~term 
-		  ())
-  in
   let _ = help_factory#add_separator () in
   let about_m = help_factory#add_item "_About" in