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

4 files changed, 99 insertions, 43 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index b27b3f362..9f99a8a6e 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 dfcf61ef5..b2773d541 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 6b8307fc5..2c190c4c6 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
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index b2d1eb919..469db5367 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -31,6 +31,7 @@ let usage () =
   prerr_endline "  --texmacs            produce a TeXmacs document";
   prerr_endline "  --dvi                output the DVI";
   prerr_endline "  --ps                 output the PostScript";
+  prerr_endline "  --pdf                output the Pdf";
   prerr_endline "  --stdout             write output to stdout";
   prerr_endline "  -o <file>            write output in file <file>";
   prerr_endline "  -d <dir>             output files into directory <dir>";
@@ -193,6 +194,7 @@ let files_from_file f =
       
 let dvi = ref false
 let ps = ref false
+let pdf = ref false
 
 let parse () =
   let files = ref [] in
@@ -243,6 +245,8 @@ let parse () =
 	usage ()
     | ("-latex" | "--latex") :: rem ->
 	Cdglobals.target_language := LaTeX; parse_rec rem
+    | ("-pdf" | "--pdf") :: rem ->
+	Cdglobals.target_language := LaTeX; pdf := true; parse_rec rem
     | ("-dvi" | "--dvi") :: rem ->
 	Cdglobals.target_language := LaTeX; dvi := true; parse_rec rem
     | ("-ps" | "--ps") :: rem ->
@@ -318,7 +322,7 @@ let parse () =
 (*s The following function produces the output. The default output is
     the \LaTeX\ document: in that case, we just call [Web.produce_document]. 
     If option \verb!-dvi!, \verb!-ps! or \verb!-html! is invoked, then
-    we make calls to \verb!latex! or \verb!dvips!  accordingly. *)
+    we make calls to \verb!latex! or \verb!dvips! or \verb!pdflatex! accordingly. *)
 
 let locally dir f x =
   let cwd = Sys.getcwd () in
@@ -335,6 +339,7 @@ let clean_temp_files basefile =
     remove (basefile ^ ".toc");
     remove (basefile ^ ".dvi");
     remove (basefile ^ ".ps");
+    remove (basefile ^ ".pdf");
     remove (basefile ^ ".haux");
     remove (basefile ^ ".html")
       
@@ -442,7 +447,7 @@ let produce_document l =
 	gen_mult_files l
 	  
 let produce_output fl =
-  if not (!dvi || !ps) then 
+  if not (!dvi || !ps || !pdf) then 
     produce_document fl
   else 
     begin
@@ -452,12 +457,14 @@ let produce_output fl =
 	out_to := File texfile;
 	output_dir := (Filename.dirname texfile);
 	produce_document fl;
+	
+	let latexexe = if !pdf then "pdflatex" else "latex" in
 	let latexcmd = 
 	  let file = Filename.basename texfile in
 	  let file = 
 	    if !quiet then sprintf "'\\nonstopmode\\input{%s}'" file else file 
 	  in
-	    sprintf "latex %s && latex %s 1>&2 %s" file file (if !quiet then "> /dev/null" else "")
+	    sprintf "%s %s && %s %s 1>&2 %s" latexexe file latexexe file (if !quiet then "> /dev/null" else "")
 	in
 	let res = locally (Filename.dirname texfile) Sys.command latexcmd in
 	  if res <> 0 then begin
@@ -472,8 +479,15 @@ let produce_output fl =
 		  | MultFiles | StdOut -> cat dvifile
 		  | File f -> copy dvifile f
 	      end;
+	  let pdffile = basefile ^ ".pdf" in
+	    if !pdf then 
+            begin
+	        match final_out_to with
+		  | MultFiles | StdOut -> cat pdffile
+		  | File f -> copy pdffile f
+	    end;
 	    if !ps then begin
-		let psfile = basefile ^ ".ps" 
+	        let psfile = basefile ^ ".ps" 
 		in
 		let command = 
 		  sprintf "dvips %s -o %s %s" dvifile psfile 
@@ -488,6 +502,7 @@ let produce_output fl =
 		    | MultFiles | StdOut -> cat psfile
 		    | File f -> copy psfile f
 	      end;
+	 
 	    clean_temp_files basefile
     end