Réorganisation fenêtre d'accueil CoqIDE et About; nouvelle image de

coq (mais ça ne rend pas très bien -- faudrait centrer l'image)



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

4 files changed, 52 insertions, 34 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 889e4bff5..ca28d1948 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -50,26 +50,31 @@ let init () =
 
 let i = ref 0
 
-let version () =
+let get_version_date () =
   let date =
     if Glib.Utf8.validate Coq_config.date
     then Coq_config.date
     else "<date not printable>" in
-  let get_version_date () =
-    try
-      let ch = open_in (Coq_config.coqtop^"/revision") in
-      let ver = input_line ch in
-      let rev = input_line ch in
-	(ver,rev)
-    with _ -> (Coq_config.version,date) in
-  let (rev,ver) = get_version_date () in
+  try
+    let ch = open_in (Coq_config.coqtop^"/revision") in
+    let ver = input_line ch in
+    let rev = input_line ch in
+    (ver,rev)
+  with _ -> (Coq_config.version,date)
+
+let short_version () =
+  let (ver,date) = get_version_date () in
+  Printf.sprintf "The Coq Proof Assistant, version %s (%s)\n" ver date
+
+let version () =
+  let (ver,date) = get_version_date () in
     Printf.sprintf 
       "The Coq Proof Assistant, version %s (%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"
-      rev ver
+      ver date
       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") 
diff --git a/ide/coq.mli b/ide/coq.mli
index 1d5a1f2e6..930687eae 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -13,6 +13,7 @@ open Term
 open Environ
 open Evd
 
+val short_version : unit -> string
 val version : unit -> string
 
 type printing_state = {
diff --git a/ide/coq.png b/ide/coq.png
index 011203f7a..a9254495c 100644
--- a/ide/coq.png
+++ b/ide/coq.png
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 9f99a8a6e..73ce38072 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -3424,34 +3424,46 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 								   (fun {view=view} -> view#misc#modify_font fd)
 								   input_views;
 							      );
-							    let about (b:GText.buffer) =
-(*
-							      (try 
-								   let image = lib_ide_file "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 _ -> ());
-*)
-							      let about_string =
-								"\nCoqIDE: an Integrated Development Environment for Coq\n\
+							    let about_full_string =
+							      "\nCoq is developed by the Coq Development Team\
+       \n(INRIA - CNRS - University Paris 11 and partners)\
+       \nWeb site: http://coq.inria.fr\
+       \nFeature wish or bug report: http://logical.saclay.inria.fr/coq-bugs\
+       \n\
+       \nCredits for CoqIDE, the 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://logical.saclay.inria.fr/coq-bugs\n\
+       \n               Pierre Letouzey, Claude Marché\
+       \n               Bruno Barras, Pierre Corbineau\
+       \n               Julien Narboux, Hugo Herbelin, ... \
+       \n\
        \nVersion information\
-       \n-------------------\n"
-							      in
-								if Glib.Utf8.validate about_string
-								then b#insert about_string;
-								let coq_version = Coq.version () in
-								  if Glib.Utf8.validate coq_version
-								  then b#insert coq_version;
-								  
+       \n-------------------\
+       \n"
+							    in
+							    let initial_about (b:GText.buffer) =
+							      (try 
+								let image = lib_ide_file "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 _ -> ());
+							      let coq_version = Coq.short_version () in
+							      b#insert ~iter:b#start_iter "\n\n";
+							      if Glib.Utf8.validate coq_version then b#insert ~iter:b#start_iter coq_version;
+							      b#insert ~iter:b#start_iter "\n   "
+							    in
+
+							    let about (b:GText.buffer) =
+							      if Glib.Utf8.validate about_full_string
+							      then b#insert about_full_string;
+							      let coq_version = Coq.version () in
+							      if Glib.Utf8.validate coq_version
+							      then b#insert coq_version
+
 							    in
-							      about  tv2#buffer;
+							      initial_about tv2#buffer;
 							      w#add_accel_group accel_group;
 							      (* Remove default pango menu for textviews *)
 							      ignore (tv2#event#connect#button_press ~callback: