aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/fake_ide.ml
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-07-09 16:31:11 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-07-09 16:31:11 +0000
commit35dac4a85762924da7fb9b23f2029c2e5642a761 (patch)
tree1912e7eb0f2e8ec62a06ba36316693bb83ac7127 /tools/fake_ide.ml
parent33aa990046792f9617d5135d4b43de3fd0d91c3f (diff)
Fixed fake_ide test-suite.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15564 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/fake_ide.ml')
-rw-r--r--tools/fake_ide.ml15
1 files changed, 13 insertions, 2 deletions
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index b15a0c637..e07607c33 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -16,13 +16,24 @@ type coqtop = {
xml_parser : Xml_parser.t;
}
+let logger level content = ()
+
let eval_call (call:'a Serialize.call) coqtop =
prerr_endline (Serialize.pr_call call);
let xml_query = Serialize.of_call call in
Xml_utils.print_xml coqtop.out_chan xml_query;
flush coqtop.out_chan;
- let xml_answer = Xml_parser.parse coqtop.xml_parser in
- let res = Serialize.to_answer xml_answer in
+ let rec loop () =
+ let xml = Xml_parser.parse coqtop.xml_parser in
+ if Serialize.is_message xml then
+ let message = Serialize.to_message xml in
+ let level = message.Interface.message_level in
+ let content = message.Interface.message_content in
+ let () = logger level content in
+ loop ()
+ else (Serialize.to_answer xml : 'a Interface.value)
+ in
+ let res = loop () in
prerr_endline (Serialize.pr_full_value call res);
match res with Interface.Fail _ -> exit 1 | _ -> ()