diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-30 16:10:00 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-30 16:10:00 +0000 |
| commit | 0014a191e8d2fe1198c63fccf5590b1fedab287c (patch) | |
| tree | 276e9ade32cdee84eb409bd4a61e9ba038c63ea5 /tools/fake_ide.ml | |
| parent | 67c8388393c3774c9b574657f7ca8fc3fd2ced46 (diff) | |
fake_ide: call Coq.init as the first action
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16819 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/fake_ide.ml')
| -rw-r--r-- | tools/fake_ide.ml | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index 13151598b..f75e6fe9f 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -17,8 +17,8 @@ type coqtop = { let logger level content = () -let base_eval_call call coqtop = - prerr_endline (Serialize.pr_call call); +let base_eval_call ?(print=true) call coqtop = + if print then prerr_endline (Serialize.pr_call call); let xml_query = Serialize.of_call call in Xml_printer.print coqtop.xml_printer xml_query; let rec loop () = @@ -34,7 +34,7 @@ let base_eval_call call coqtop = else (Serialize.to_answer call xml) in let res = loop () in - prerr_endline (Serialize.pr_full_value call res); + if print then prerr_endline (Serialize.pr_full_value call res); match res with Interface.Fail _ -> exit 1 | x -> x let eval_call c q = ignore(base_eval_call c q) @@ -117,8 +117,14 @@ let main = xml_parser = ip; } in + (match base_eval_call ~print:false (Serialize.init ()) coqtop with + | Interface.Good id -> ids := [id] + | Interface.Fail _ -> assert false); while true do - let l = try read_line () with End_of_file -> exit 0 + let l = try read_line () with End_of_file -> + match base_eval_call ~print:false (Serialize.status true) coqtop with + | Interface.Good _ -> exit 0 + | Interface.Fail _ -> exit 1 in try read_eval_print l coqtop with |