aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/fake_ide.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-09-22 13:27:26 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-09-22 13:27:26 +0200
commitf2f146a997e92f3380d9cd9aa0f7aef80f50dba8 (patch)
tree7375be8edc8dd46192f04212ccaa096d7fa743b2 /tools/fake_ide.ml
parent002cd2e8f6ae5722e72a5db136cda7414f9218d5 (diff)
Fixing fake_ide.
Diffstat (limited to 'tools/fake_ide.ml')
-rw-r--r--tools/fake_ide.ml23
1 files changed, 17 insertions, 6 deletions
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index a9a7251c5..dfe6093d6 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -17,7 +17,18 @@ type coqtop = {
xml_parser : Xml_parser.t;
}
-let logger level content = prerr_endline content
+let print_xml chan xml =
+ let rec print = function
+ | Xml_datatype.PCData s -> output_string chan s
+ | Xml_datatype.Element (_, _, children) -> List.iter print children
+ in
+ print xml
+
+let error_xml s =
+ Printf.eprintf "fake_id: error: %a\n%!" print_xml s;
+ exit 1
+
+let logger level content = Printf.eprintf "%a\n%! " print_xml content
let base_eval_call ?(print=true) ?(fail=true) call coqtop =
if print then prerr_endline (Xmlprotocol.pr_call call);
@@ -38,8 +49,8 @@ let base_eval_call ?(print=true) ?(fail=true) call coqtop =
let res = loop () in
if print then prerr_endline (Xmlprotocol.pr_full_value call res);
match res with
- | Interface.Fail (_,_,s) when fail -> error s
- | Interface.Fail (_,_,s) as x -> prerr_endline s; x
+ | Interface.Fail (_,_,s) when fail -> error_xml (Richpp.repr s)
+ | Interface.Fail (_,_,s) as x -> Printf.eprintf "%a\n%!" print_xml (Richpp.repr s); x
| x -> x
let eval_call c q = ignore(base_eval_call c q)
@@ -188,7 +199,7 @@ let print_document () =
module GUILogic = struct
let after_add = function
- | Interface.Fail (_,_,s) -> error s
+ | Interface.Fail (_,_,s) -> error_xml (Richpp.repr s)
| Interface.Good (id, (Util.Inl (), _)) ->
Document.assign_tip_id doc id
| Interface.Good (id, (Util.Inr tip, _)) ->
@@ -200,7 +211,7 @@ module GUILogic = struct
let at id id' _ = Stateid.equal id' id
let after_edit_at (id,need_unfocus) = function
- | Interface.Fail (_,_,s) -> error s
+ | Interface.Fail (_,_,s) -> error_xml (Richpp.repr s)
| Interface.Good (Util.Inl ()) ->
if need_unfocus then Document.unfocus doc;
ignore(Document.cut_at doc id);
@@ -323,7 +334,7 @@ let main =
let finish () =
match base_eval_call (Xmlprotocol.status true) coq with
| Interface.Good _ -> exit 0
- | Interface.Fail (_,_,s) -> error s in
+ | Interface.Fail (_,_,s) -> error_xml (Richpp.repr s) in
(* The main loop *)
init ();
while true do