diff options
Diffstat (limited to 'ide/wg_Command.ml')
| -rw-r--r-- | ide/wg_Command.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index b83bd107ee..47dad8f196 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -103,11 +103,12 @@ object(self) let process = Coq.bind (Coq.query (phrase,Stateid.dummy)) (function | Interface.Fail (_,l,str) -> - Ideutils.insert_xml result#buffer (Richpp.richpp_of_pp 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 |