diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-09-13 17:19:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-09-20 15:20:32 +0200 |
| commit | 002cd2e8f6ae5722e72a5db136cda7414f9218d5 (patch) | |
| tree | e45f8de4e5c493f08a5cabf4593125f4befe66fb /ide/wg_Command.ml | |
| parent | f20fce1259563f2081fadc62ccab1304bb8161d5 (diff) | |
Rich printing of CoqIDE protocol failure.
Diffstat (limited to 'ide/wg_Command.ml')
| -rw-r--r-- | ide/wg_Command.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index 0ae57ee74..7d8993aa8 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -107,7 +107,7 @@ object(self) let process = Coq.bind (Coq.query ~logger:log (phrase,Stateid.dummy)) (function | Interface.Fail (_,l,str) -> - result#buffer#insert str; + Ideutils.insert_xml result#buffer str; notebook#set_page ~tab_label:(new_tab_lbl "Error") frame#coerce; Coq.return () | Interface.Good res -> |