add support for pdf in coqdoc, add export to pdf in coqide, port open and save as dialogs of coqide to a not deprecated widget, add filtering of *.v files in these dialogs

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

3 files changed, 80 insertions, 39 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index b27b3f3628..9f99a8a6e5 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -152,7 +152,6 @@ object('self)
   method revert : unit
   method auto_save : unit
   method save : string -> bool
-  method save_as : string -> bool
   method read_only : bool
   method set_read_only : bool -> unit
   method is_active : bool
@@ -717,7 +716,7 @@ object(self)
 		warning ("Autosave: unexpected error while writing "^fn)
       end	      
       
-  method save_as f =
+(*  method save_as f =
     if Sys.file_exists f then 
       match (GToolbox.question_box ~title:"File exists on disk"
 	       ~buttons:["Overwrite";
@@ -733,7 +732,7 @@ object(self)
       with 1 -> self#save f
 	| _ -> false
     else self#save f
-
+*)
   method set_read_only b = read_only<-b
   method read_only = read_only
   method is_active = is_active
@@ -1921,10 +1920,19 @@ let main files =
 	    | Vector.Found i -> set_current_view i
 	    | e -> !flash_info ("Load failed: "^(Printexc.to_string e))
       in
-      let load_m = file_factory#add_item "_Open/Create" 
+      let load_m = file_factory#add_item "_New" 
+	~key:GdkKeysyms._N in
+      let load_f () = 	  
+	match select_file_for_save ~title:"Create file" () with 
+	  | None -> ()
+	  | Some f -> load f
+      in
+	ignore (load_m#connect#activate (load_f));
+
+      let load_m = file_factory#add_item "_Open" 
 	~key:GdkKeysyms._O in
       let load_f () = 	  
-	match select_file ~title:"Load file" () with 
+	match select_file_for_open ~title:"Load file" () with 
 	  | None -> ()
 	  | Some f -> load f
       in
@@ -1940,11 +1948,11 @@ let main files =
 	    try
 	      (match (Option.get current.analyzed_view)#filename with 
 		 | None ->
-		     begin match GToolbox.select_file ~title:"Save file" ()
+		     begin match select_file_for_save ~title:"Save file" ()
 		       with
 			 | None -> ()
 			 | Some f -> 
-			     if (Option.get current.analyzed_view)#save_as f then begin
+			     if (Option.get current.analyzed_view)#save f then begin
 				 set_current_tab_label (Filename.basename f);
 				 !flash_info ("File " ^ f ^ " saved")
 			       end
@@ -1968,25 +1976,25 @@ let main files =
 	    let current = get_current_view () in
 	      try (match (Option.get current.analyzed_view)#filename with 
 		     | None -> 
-			 begin match GToolbox.select_file ~title:"Save file as" ()
+			 begin match select_file_for_save ~title:"Save file as" ()
 			   with
 			     | None -> ()
 			     | Some f -> 
-				 if (Option.get current.analyzed_view)#save_as f then begin
+				 if (Option.get current.analyzed_view)#save f then begin
 				     set_current_tab_label (Filename.basename f);
 				     !flash_info "Saved"
 				   end
 				 else !flash_info "Save Failed"
 			 end
 		     | Some f -> 
-			 begin match GToolbox.select_file 
+			 begin match select_file_for_save 
 			     ~dir:(ref (Filename.dirname f)) 
 			     ~filename:(Filename.basename f)
 			     ~title:"Save file as" ()
 			   with
 			     | None -> ()
 			     | Some f -> 
-				 if (Option.get current.analyzed_view)#save_as f then begin
+				 if (Option.get current.analyzed_view)#save f then begin
 				     set_current_tab_label (Filename.basename f);
 				     !flash_info "Saved"
 				   end else !flash_info "Save Failed"
@@ -2082,7 +2090,7 @@ let main files =
 			      let basef_we = try Filename.chop_extension basef with _ -> basef in
 				match kind with
 				  | "latex" -> basef_we ^ ".tex"
-				  | "dvi" | "ps" | "html" -> basef_we ^ "." ^ kind
+				  | "dvi" | "ps" | "pdf" | "html" -> basef_we ^ "." ^ kind
 				  | _ -> assert false
 			    in
 			    let cmd = 
@@ -2108,6 +2116,9 @@ let main files =
 		    file_export_factory#add_item "_Dvi" ~callback:(export_f "dvi") 
 		  in
 		  let _ = 
+		    file_export_factory#add_item "_Pdf" ~callback:(export_f "pdf") 
+		  in
+		  let _ = 
 		    file_export_factory#add_item "_Ps" ~callback:(export_f "ps") 
 		  in
 
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index dfcf61ef52..b2773d541d 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -167,33 +167,60 @@ let init_stdout,read_stdout,clear_stdout =
 
 
 let last_dir = ref ""
-let select_file ~title ?(dir = last_dir) ?(filename="") () =
-  let fs =
-    if Filename.is_relative filename then begin
-      if !dir <> "" then
-        let filename = Filename.concat !dir filename in 
-        GWindow.file_selection ~show_fileops:true ~modal:true ~title ~filename ()
-      else
-        GWindow.file_selection ~show_fileops:true ~modal:true ~title ()
-    end else begin
-      dir := Filename.dirname filename;
-      GWindow.file_selection ~show_fileops:true ~modal:true ~title ~filename ()
-    end
-  in
-  fs#complete ~filter:"";
-  ignore (fs#connect#destroy ~callback: GMain.Main.quit);
-  let file = ref None in 
-  ignore (fs#ok_button#connect#clicked ~callback:
-    begin fun () ->
-      file := Some fs#filename; 
-      dir := Filename.dirname fs#filename;
-      fs#destroy ()
-    end);
-  ignore (fs # cancel_button # connect#clicked ~callback:fs#destroy);
-  fs # show ();
-  GMain.Main.main ();
-  !file
 
+let filter_all_files () = GFile.filter 
+  ~name:"All" 
+  ~patterns:["*"] () 
+  
+let filter_coq_files () =  GFile.filter 
+  ~name:"Coq source code" 
+  ~patterns:[ "*.v"] ()
+
+let select_file_for_open ~title ?(dir = last_dir) ?(filename="") () =
+  let file = ref None in 
+  let file_chooser = GWindow.file_chooser_dialog ~action:`OPEN ~modal:true ~title () in
+    file_chooser#add_button_stock `CANCEL `CANCEL ;
+    file_chooser#add_select_button_stock `OPEN `OPEN ;
+    file_chooser#add_filter (filter_coq_files ());
+    file_chooser#add_filter (filter_all_files ());
+    ignore (file_chooser#set_current_folder !dir);
+    begin match file_chooser#run () with
+      | `OPEN -> 
+	  begin 
+	    file := file_chooser#filename;
+	    match !file with
+		None -> ()
+	      | Some s -> dir := Filename.dirname s;
+	  end
+      | `DELETE_EVENT | `CANCEL -> ()
+    end ;
+    file_chooser#destroy ();	    
+    !file
+
+
+let select_file_for_save ~title ?(dir = last_dir) ?(filename="") () =
+  let file = ref None in 
+  let file_chooser = GWindow.file_chooser_dialog ~action:`SAVE ~modal:true ~title () in
+    file_chooser#add_button_stock `CANCEL `CANCEL ;
+    file_chooser#add_select_button_stock `SAVE `SAVE ;
+    file_chooser#add_filter (filter_coq_files ());
+    file_chooser#add_filter (filter_all_files ());
+    file_chooser#set_do_overwrite_confirmation true;
+    ignore (file_chooser#set_current_folder !dir);
+    ignore (file_chooser#set_current_name filename);
+    
+    begin match file_chooser#run () with
+      | `SAVE -> 
+	  begin 
+	    file := file_chooser#filename;
+	    match !file with
+		None -> ()
+	      | Some s -> dir := Filename.dirname s;
+	  end
+      | `DELETE_EVENT | `CANCEL -> ()
+    end ;
+    file_chooser#destroy ();	    
+    !file
 
 let find_tag_start (tag :GText.tag) (it:GText.iter) =
   let it = it#copy in
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 6b8307fc59..2c190c4c67 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -40,7 +40,10 @@ val print_id : 'a -> unit
 val read_stdout : unit -> string
 val revert_timer : GMain.Timeout.id option ref
 val auto_save_timer : GMain.Timeout.id option ref
-val select_file :
+val select_file_for_open :
+  title:string ->
+  ?dir:string ref -> ?filename:string -> unit -> string option
+val select_file_for_save :
   title:string ->
   ?dir:string ref -> ?filename:string -> unit -> string option
 val set_highlight_timer : (unit -> 'a) -> unit