aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/coqide.ml35
-rw-r--r--ide/ideutils.ml79
-rw-r--r--ide/ideutils.mli5
-rw-r--r--tools/coqdoc/main.ml23
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 05:30:30 +0000