aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-06-29 20:05:49 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-06-29 20:05:49 +0000
commit9fa075601e6433504cc7d34387a01cd328f8f271 (patch)
tree1e086655b579f55044d8160abff29d5ea68928b2 /tools
parent223400bd5f9afccdf2405af31cc37a1c92c9246c (diff)
Fixing fake_ide
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15502 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
-rw-r--r--tools/fake_ide.ml29
1 files changed, 19 insertions, 10 deletions
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 31303b5ba..b15a0c637 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -10,17 +10,18 @@
exception Comment
-let coqtop = ref (stdin, stdout)
+type coqtop = {
+ in_chan : in_channel;
+ out_chan : out_channel;
+ xml_parser : Xml_parser.t;
+}
-let p = Xml_parser.make ()
-let () = Xml_parser.check_eof p false
-
-let eval_call (call:'a Serialize.call) =
+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 (snd !coqtop) xml_query;
- flush (snd !coqtop);
- let xml_answer = Xml_parser.parse p (Xml_parser.SChannel (fst !coqtop)) 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
prerr_endline (Serialize.pr_full_value call res);
match res with Interface.Fail _ -> exit 1 | _ -> ()
@@ -72,11 +73,19 @@ let main =
| 2 when Sys.argv.(1) <> "-help" -> Sys.argv.(1)
| _ -> usage ()
in
- coqtop := Unix.open_process (coqtop_name^" -ideslave");
+ let coqtop =
+ let (cin, cout) = Unix.open_process (coqtop_name^" -ideslave") in
+ let p = Xml_parser.make (Xml_parser.SChannel cin) in
+ let () = Xml_parser.check_eof p false in {
+ in_chan = cin;
+ out_chan = cout;
+ xml_parser = p;
+ }
+ in
while true do
let l = try read_line () with End_of_file -> exit 0
in
- try read_eval_print l
+ try read_eval_print l coqtop
with
| Comment -> ()
| e ->