CoqIde: externals

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4040 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 38 insertions, 6 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 3b0c3dced..6a9a202e8 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -939,7 +939,8 @@ object(self)
 	  
   method process_next_phrase display_goals do_highlight = 
     begin
-      try self#clear_message;
+      try 
+	self#clear_message;
 	prerr_endline "process_next_phrase starting now";
 	if do_highlight then begin
 	  !push_info "Coq is computing";
@@ -2175,21 +2176,29 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
     | None -> 
 	!flash_info "Active buffer has no name"
     | Some f ->
-	let c = Sys.command (!current.cmd_coqc ^ " " ^ f) in
-	if c = 0 then
+	let s,res = run_command 
+		      av#insert_message 
+		      (!current.cmd_coqc ^ " " ^ f) 
+	in
+	if s = Unix.WEXITED 0 then
 	  !flash_info (f ^ " successfully compiled")
 	else begin
 	  !flash_info (f ^ " failed to compile");
-	  av#process_until_end_or_error
+	  av#process_until_end_or_error;
+	  av#insert_message "Compilation output:\n";
+	  av#insert_message res
 	end
   in
   let compile_m = externals_factory#add_item "_Compile" ~callback:compile_f in
 
   (* Command/Make Menu *)
   let make_f () =
+    let v = get_active_view () in
+    let av = out_some v.analyzed_view in
     save_f ();
-    let c = Sys.command !current.cmd_make in
-    !flash_info (!current.cmd_make ^ if c = 0 then " succeeded" else " failed")
+    av#insert_message "Command output:\n";
+    let s,res = run_command av#insert_message !current.cmd_make in
+    !flash_info (!current.cmd_make ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
   in
   let make_m = externals_factory#add_item "_Make" ~callback:make_f in
   
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index e5edce660..4cf9c1ba2 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -240,3 +240,24 @@ let rec print_list print fmt = function
   | [] -> ()
   | [x] -> print fmt x
   | x :: r -> print fmt x; print_list print fmt r
+
+
+let run_command f c =
+  let result = Buffer.create 127 in
+  let cin,cout,cerr = Unix.open_process_full c [||] in
+  let buff = String.make 127 ' ' in
+  let buffe = String.make 127 ' ' in
+  let n = ref 0 in
+  let ne = ref 0 in
+
+  while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ; 
+    !n+ !ne <> 0
+  do 
+    let r = String.sub buff 0 !n in 
+    f r;
+    Buffer.add_string result r;
+    let r = String.sub buffe 0 !ne in 
+    f r;
+    Buffer.add_string result r 
+  done;
+  (Unix.close_process_full (cin,cout,cerr),  Buffer.contents result)
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 2e98c0594..011fd6d85 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -45,3 +45,5 @@ val stock_to_widget :  ?size:Gtk.Tags.icon_size -> GtkStock.id -> GObj.widget
 
 open Format
 val print_list : (formatter -> 'a -> unit) -> formatter -> 'a list -> unit
+
+val run_command : (string -> unit) -> string -> Unix.process_status*string