Imported Upstream version 8.3.pl3upstream/8.3.pl3

1 files changed, 45 insertions, 33 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index ce4f0666..162728ad 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqide.ml 13751 2010-12-24 09:56:05Z letouzey $ *)
+(* $Id: coqide.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Preferences
 open Vernacexpr
@@ -306,7 +306,8 @@ let remove_current_view_page () =
       kill_input_view c
   in
   let current = session_notebook#current_term in
-    if current.script#buffer#modified then
+    if not current.script#buffer#modified then do_remove ()
+    else
       match GToolbox.question_box ~title:"Close"
               ~buttons:["Save Buffer and Close";
                         "Close without Saving";
@@ -1680,34 +1681,42 @@ let choose_save session =
     save_dialog#show ()
  *)
 
+(* Nota: using && here has the advantage of working both under win32 and unix.
+   If someday we want the main command to be tried even if the "cd" has failed,
+   then we should use " ; " under unix but " & " under win32 (cf. #2363).
+*)
+
+let local_cd file =
+  "cd " ^ Filename.quote (Filename.dirname file) ^ " && "
+
 let do_print session =
   let av = session.analyzed_view in
-    if session.filename = ""
-    then flash_info "Cannot print: this buffer has no name"
-    else begin
-      let cmd =
-        "cd " ^ Filename.quote (Filename.dirname session.filename) ^ "; " ^
-        !current.cmd_coqdoc ^ " -ps " ^ Filename.quote (Filename.basename session.filename) ^
-        " | " ^ !current.cmd_print
-      in
-      let print_window = GWindow.window ~title:"Print" ~modal:true ~position:`CENTER ~wm_class:"CoqIDE" ~wm_name: "CoqIDE"  () in
-      let vbox_print = GPack.vbox ~spacing:10 ~border_width:10 ~packing:print_window#add () in
-      let _ = GMisc.label ~justify:`LEFT ~text:"Print using the following command:" ~packing:vbox_print#add () in
-      let print_entry = GEdit.entry ~text:cmd ~editable:true ~width_chars:80 ~packing:vbox_print#add () in
-      let hbox_print = GPack.hbox ~spacing:10 ~packing:vbox_print#add () in
-      let print_cancel_button = GButton.button ~stock:`CANCEL ~label:"Cancel" ~packing:hbox_print#add () in
-      let print_button  = GButton.button ~stock:`PRINT  ~label:"Print"  ~packing:hbox_print#add () in
-      let callback_print () =
-        let cmd = print_entry#text in
-        let s,_ = run_command av#insert_message cmd in
-          flash_info (cmd ^ if s = Unix.WEXITED 0 then " succeeded" else " failed");
-          print_window#destroy ()
-      in
-        ignore (print_cancel_button#connect#clicked ~callback:print_window#destroy) ;
-        ignore (print_button#connect#clicked ~callback:callback_print);
-        print_window#misc#show ()
-    end
-
+    match av#filename with
+      |None -> flash_info "Cannot print: this buffer has no name"
+      |Some f_name -> begin
+	  let cmd =
+	local_cd session.filename ^
+              !current.cmd_coqdoc ^ " --coqlib_path " ^ Envars.coqlib () ^
+	      " -ps " ^ Filename.quote (Filename.basename f_name) ^
+              " | " ^ !current.cmd_print
+	  in
+	  let print_window = GWindow.window ~title:"Print" ~modal:true ~position:`CENTER ~wm_class:"CoqIDE" ~wm_name: "CoqIDE"  () in
+	  let vbox_print = GPack.vbox ~spacing:10 ~border_width:10 ~packing:print_window#add () in
+	  let _ = GMisc.label ~justify:`LEFT ~text:"Print using the following command:" ~packing:vbox_print#add () in
+	  let print_entry = GEdit.entry ~text:cmd ~editable:true ~width_chars:80 ~packing:vbox_print#add () in
+	  let hbox_print = GPack.hbox ~spacing:10 ~packing:vbox_print#add () in
+	  let print_cancel_button = GButton.button ~stock:`CANCEL ~label:"Cancel" ~packing:hbox_print#add () in
+	  let print_button  = GButton.button ~stock:`PRINT  ~label:"Print"  ~packing:hbox_print#add () in
+	  let callback_print () =
+            let cmd = print_entry#text in
+            let s,_ = run_command av#insert_message cmd in
+              flash_info (cmd ^ if s = Unix.WEXITED 0 then " succeeded" else " failed");
+              print_window#destroy ()
+	  in
+            ignore (print_cancel_button#connect#clicked ~callback:print_window#destroy) ;
+            ignore (print_button#connect#clicked ~callback:callback_print);
+            print_window#misc#show ()
+	end
 
 let main files =
   (* Statup preferences *)
@@ -1956,8 +1965,11 @@ let main files =
 				  | _ -> assert false
 			    in
 			    let cmd =
-			      "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^
-				!current.cmd_coqdoc ^ " --" ^ kind ^ " -o " ^ (Filename.quote output) ^ " " ^ (Filename.quote basef)
+			      local_cd f ^
+				!current.cmd_coqdoc ^ " --coqlib_path " ^
+				Envars.coqlib () ^ " --" ^ kind ^
+				" -o " ^ (Filename.quote output) ^ " " ^
+				(Filename.quote basef)
 			    in
 			    let s,_ = run_command av#insert_message cmd in
 			      flash_info (cmd ^
@@ -2862,7 +2874,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 						    flash_info "Cannot make: this buffer has no name"
 						| Some f ->
 						    let cmd =
-						      "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ !current.cmd_make in
+						      local_cd f ^ !current.cmd_make in
 
 						      (*
 							save_f ();
@@ -2929,7 +2941,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 						    flash_info "Cannot make makefile: this buffer has no name"
 						| Some f ->
 						    let cmd =
-						      "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ !current.cmd_coqmakefile in
+						      local_cd 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")