diff options
Diffstat (limited to 'ide/wg_Command.ml')
| -rw-r--r-- | ide/wg_Command.ml | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index 946aaf010..47dad8f19 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 |