diff options
Diffstat (limited to 'tools/fake_ide.ml')
| -rw-r--r-- | tools/fake_ide.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index e81f4038d..d5ef807b6 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -36,10 +36,10 @@ let base_eval_call ?(print=true) ?(fail=true) call coqtop = Xml_printer.print coqtop.xml_printer xml_query; let rec loop () = let xml = Xml_parser.parse coqtop.xml_parser in - if Pp.is_message xml then - let message = Pp.to_message xml in - let level = message.Pp.message_level in - let content = message.Pp.message_content in + if Feedback.is_message xml then + let message = Feedback.to_message xml in + let level = message.Feedback.message_level in + let content = message.Feedback.message_content in logger level content; loop () else if Feedback.is_feedback xml then |