diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/fake_ide.ml | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index 8fcca535d1..23c111b371 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -37,14 +37,9 @@ 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 - match Xmlprotocol.is_message xml with - | Some (level, _loc, content) -> - logger level content; + if Xmlprotocol.is_feedback xml then loop () - | None -> - if Xmlprotocol.is_feedback xml then - loop () - else Xmlprotocol.to_answer call xml + else Xmlprotocol.to_answer call xml in let res = loop () in if print then prerr_endline (Xmlprotocol.pr_full_value call res); |