Merge PR#390: Updates to the Pretty Printing Infrastructure

1 files changed, 4 insertions, 7 deletions

diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 946aaf010d..47dad8f196 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -100,18 +100,15 @@ object(self)
         if Str.string_match (Str.regexp "\\. *$") com 0 then com
         else com ^ " " ^ arg ^" . "
       in
-      let log level message =
-        Ideutils.insert_xml result#buffer message;
-        result#buffer#insert "\n";
-      in
       let process =
-	Coq.bind (Coq.query ~logger:log (phrase,Stateid.dummy)) (function
+	Coq.bind (Coq.query (phrase,Stateid.dummy)) (function
           | Interface.Fail (_,l,str) ->
-            Ideutils.insert_xml result#buffer str;
+            let width = Ideutils.textview_width result in
+            Ideutils.insert_xml result#buffer (Richpp.richpp_of_pp width str);
             notebook#set_page ~tab_label:(new_tab_lbl "Error") frame#coerce;
 	    Coq.return ()
           | Interface.Good res ->
-            result#buffer#insert res; 
+            result#buffer#insert res;
             notebook#set_page ~tab_label:(new_tab_lbl arg) frame#coerce;
 	    Coq.return ())
       in