coqide: about now displays versions/Fix for alt-enter

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

2 files changed, 25 insertions, 17 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 7b62ef166..6a21e451d 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -47,8 +47,13 @@ let init () =
 let i = ref 0
 
 let version () =
-  Printf.sprintf "The Coq Proof Assistant, version %s (%s)\nCompiled on %s\n"
+  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"
     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)
 
 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 26bb80b05..e2f4fddc3 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1321,13 +1321,12 @@ Please restart and report NOW.";
 	      begin
 		let i= self#get_insert#backward_word_start in
 		prerr_endline "active_kp_hf: Placing cursor";
-		input_buffer#place_cursor i;
-		self#process_until_insert_or_error
+		self#process_until_iter_or_error i
 	      end);
 	  true
       | l when List.mem `CONTROL l -> 
 	  let k = GdkEvent.Key.keyval k in
-	  if GdkKeysyms._m=k
+	  if GdkKeysyms._Break=k
 	  then break ();
 	  false
       | l -> false
@@ -2651,15 +2650,18 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
        (fun {view=view} -> view#misc#modify_font fd)
        input_views;
   );
-  (try 
-     let image = Filename.concat lib_ide "coq.png" in
-     let startup_image = GdkPixbuf.from_file image in
-     tv2#buffer#insert_pixbuf ~iter:tv2#buffer#start_iter 
-       ~pixbuf:startup_image;
-     tv2#buffer#insert ~iter:tv2#buffer#start_iter "\t\t";
-   with _ -> ());
-  tv2#buffer#insert "\nCoqIde: an experimental Gtk2 interface for Coq.\n";
-  tv2#buffer#insert ((Coq.version ()));
+  let about (b:GText.buffer) =
+    (try 
+       let image = Filename.concat lib_ide "coq.png" in
+       let startup_image = GdkPixbuf.from_file image in
+       b#insert_pixbuf ~iter:b#start_iter 
+	 ~pixbuf:startup_image;
+       b#insert ~iter:b#start_iter "\t\t";
+     with _ -> ());
+    b#insert "\nCoqIde: an experimental Gtk2 interface for Coq.\n\nVersion infomation\n--------\n";
+    b#insert ((Coq.version ()));
+    b#insert "\nAuthor: Benjamin Monate\nDo not hesitate to report bugs or missing features." in
+  about  tv2#buffer;
   w#add_accel_group accel_group;
   (* Remove default pango menu for textviews *)
   ignore (tv2#event#connect#button_press ~callback:
@@ -2689,7 +2691,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 () -> tv3#buffer#set_text "by Benjamin Monate"));
+	    ~callback:(fun () -> about tv3#buffer));
   ignore (faq_m#connect#activate 
 	    ~callback:(fun () -> 
 			 load (Filename.concat lib_ide "FAQ")));
@@ -2742,9 +2744,10 @@ let start () =
   GtkData.AccelGroup.set_default_mod_mask 
     (Some [`CONTROL;`SHIFT;`MOD1;`MOD3;`MOD4]);
   cb_ := Some (GtkBase.Clipboard.get Gdk.Atom.primary);
-  Glib.Message.set_log_handler ~domain:"Gtk" ~levels:[`ERROR;`FLAG_FATAL;
-						      `WARNING;`CRITICAL]
-    (fun ~level msg -> failwith ("Coqide internal error: " ^ msg));
+  ignore (
+    Glib.Message.set_log_handler ~domain:"Gtk" ~levels:[`ERROR;`FLAG_FATAL;
+							`WARNING;`CRITICAL]
+	    (fun ~level msg -> failwith ("Coqide internal error: " ^ msg)));
   Command_windows.main ();
   Blaster_window.main 9;
   main files;