summaryrefslogtreecommitdiff
path: root/ide/coqide.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2007-10-15 19:55:12 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2007-10-15 19:55:12 +0000
commit4767d724d489a7ad67f696e9401e70b9f9ae2143 (patch)
tree142a99bc1cd3beef403f1942908de090f70c5e07 /ide/coqide.ml
parent72b9a7df489ea47b3e5470741fd39f6100d31676 (diff)
Imported Upstream version 8.1.pl2+dfsgupstream/8.1.pl2+dfsg
Diffstat (limited to 'ide/coqide.ml')
-rw-r--r--ide/coqide.ml41
1 files changed, 27 insertions, 14 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index fb650cbf..fdc344e8 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqide.ml 9307 2006-10-28 18:48:48Z herbelin $ *)
+(* $Id: coqide.ml 10220 2007-10-12 13:25:54Z notin $ *)
open Preferences
open Vernacexpr
@@ -1719,9 +1719,10 @@ let create_input_tab filename =
let v_box = GPack.hbox ~homogeneous:false () in
let _ = GMisc.image ~packing:v_box#pack () in
let _ = GMisc.label ~text:filename ~packing:v_box#pack () in
+ let appendp x = ignore ((notebook ())#append_page
+ ~tab_label:v_box#coerce x) in
let fr1 = GBin.frame ~shadow_type:`ETCHED_OUT
- ~packing:((notebook ())#append_page
- ~tab_label:v_box#coerce) ()
+ ~packing:appendp ()
in
let sw1 = GBin.scrolled_window
~vpolicy:`AUTOMATIC
@@ -2035,8 +2036,8 @@ let main files =
!flash_info "Cannot print: this buffer has no name"
| Some f ->
let cmd =
- "cd " ^ Filename.dirname f ^ "; " ^
- !current.cmd_coqdoc ^ " -ps " ^ Filename.basename f ^
+ "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^
+ !current.cmd_coqdoc ^ " -ps " ^ Filename.quote (Filename.basename f) ^
" | " ^ !current.cmd_print
in
let s,_ = run_command av#insert_message cmd in
@@ -2063,8 +2064,8 @@ let main files =
| _ -> assert false
in
let cmd =
- "cd " ^ Filename.dirname f ^ "; " ^
- !current.cmd_coqdoc ^ " --" ^ kind ^ " -o " ^ output ^ " " ^ basef
+ "cd " ^ (Filename.quote (Filename.dirname f)) ^ "; " ^
+ !current.cmd_coqdoc ^ " --" ^ kind ^ " -o " ^ (Filename.quote output) ^ " " ^ (Filename.quote basef)
in
let s,_ = run_command av#insert_message cmd in
!flash_info (cmd ^
@@ -2411,7 +2412,7 @@ let main files =
| Some f ->
save_f ();
let l,r = !current.cmd_editor in
- let _ = run_command av#insert_message (l ^ f ^ r) in
+ let _ = run_command av#insert_message (l ^ (Filename.quote f) ^ r) in
av#revert)
in
let _ = edit_f#add_separator () in
@@ -2857,7 +2858,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
| Some f ->
let s,res = run_command
av#insert_message
- (!current.cmd_coqc ^ " " ^ f)
+ (!current.cmd_coqc ^ " " ^ (Filename.quote f))
in
if s = Unix.WEXITED 0 then
!flash_info (f ^ " successfully compiled")
@@ -2877,11 +2878,17 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
let make_f () =
let v = get_active_view () in
let av = out_some v.analyzed_view in
+ match av#filename with
+ | None ->
+ !flash_info "Cannot print: this buffer has no name"
+ | Some f ->
+ let cmd =
+ "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ !current.cmd_make in
(*
save_f ();
*)
av#insert_message "Command output:\n";
- let s,res = run_command av#insert_message !current.cmd_make in
+ let s,res = run_command av#insert_message cmd in
last_make := res;
last_make_index := 0;
!flash_info (!current.cmd_make ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
@@ -2937,9 +2944,15 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
let coq_makefile_f () =
let v = get_active_view () in
let av = out_some v.analyzed_view in
- let s,res = run_command av#insert_message !current.cmd_coqmakefile in
- !flash_info
- (!current.cmd_coqmakefile ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
+ match av#filename with
+ | None ->
+ !flash_info "Cannot make makefile: this buffer has no name"
+ | Some f ->
+ let cmd =
+ "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ !current.cmd_coqmakefile in
+ let s,res = run_command av#insert_message cmd in
+ !flash_info
+ (!current.cmd_coqmakefile ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
in
let _ = externals_factory#add_item "_Make makefile" ~callback:coq_makefile_f
in
@@ -3313,7 +3326,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
\nContributors : Jean-Christophe Filliâtre\
\n Pierre Letouzey, Claude Marché\n\
\nFeature wish or bug report: use Web interface\n\
- \n\thttp://coq.inria.fr/bin/coq-bugs\n\
+ \n\thttp://logical.futurs.inria.fr/coq-bugs\n\
\nVersion information\
\n-------------------\n"
in