diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-09-22 13:27:26 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-09-22 13:27:26 +0200 |
commit | f2f146a997e92f3380d9cd9aa0f7aef80f50dba8 (patch) | |
tree | 7375be8edc8dd46192f04212ccaa096d7fa743b2 /tools/fake_ide.ml | |
parent | 002cd2e8f6ae5722e72a5db136cda7414f9218d5 (diff) |
Fixing fake_ide.
Diffstat (limited to 'tools/fake_ide.ml')
-rw-r--r-- | tools/fake_ide.ml | 23 |
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 |