diff options
Diffstat (limited to 'ide/wg_Command.ml')
| -rw-r--r-- | ide/wg_Command.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index 163bd28b1..0ae57ee74 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -100,7 +100,10 @@ object(self) if Str.string_match (Str.regexp "\\. *$") com 0 then com else com ^ " " ^ arg ^" . " in - let log level message = result#buffer#insert (message^"\n") 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 | Interface.Fail (_,l,str) -> |