Imported Upstream version 8.1.pl2+dfsgupstream/8.1.pl2+dfsg

3 files changed, 32 insertions, 17 deletions

diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index 768d125c..937098b7 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: command_windows.ml 9189 2006-09-29 12:39:24Z notin $ *)
+(* $Id: command_windows.ml 10197 2007-10-08 13:52:35Z notin $ *)
 
 class command_window () = 
   let window = GWindow.window 
@@ -69,9 +69,10 @@ object(self)
   val notebook = notebook
   method window = window
   method new_command ?command ?term () =
+    let appendp x = ignore (notebook#append_page x) in
     let frame = GBin.frame 
 		  ~shadow_type:`ETCHED_OUT
-		  ~packing:notebook#append_page
+		  ~packing:appendp
 		  ()
     in
     notebook#goto_page (notebook#page_num frame#coerce);
diff --git a/ide/coq.ml b/ide/coq.ml
index 6059f065..d318e339 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq.ml 9537 2007-01-26 10:05:04Z corbinea $ *)
+(* $Id: coq.ml 10174 2007-10-04 13:52:23Z vsiles $ *)
 
 open Vernac
 open Vernacexpr
@@ -152,6 +152,7 @@ let interp verbosely s =
 		  | VernacFixpoint _
 		  | VernacCoFixpoint _
 		  | VernacEndProof _
+                  | VernacScheme _ 
 		    -> Options.make_silent (not verbosely)
 		  | _ -> ()
 	      end;
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