From 4767d724d489a7ad67f696e9401e70b9f9ae2143 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Mon, 15 Oct 2007 19:55:12 +0000 Subject: Imported Upstream version 8.1.pl2+dfsg --- ide/command_windows.ml | 5 +++-- ide/coq.ml | 3 ++- ide/coqide.ml | 41 +++++++++++++++++++++++++++-------------- 3 files changed, 32 insertions(+), 17 deletions(-) (limited to 'ide') 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 -- cgit v1.2.3