aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/fake_ide.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2016-11-30 22:18:30 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-03-21 15:51:38 +0100
commita010de9bcaa33fc95a2a7cb6478ac21c95e3ad9e (patch)
treeebc4c3a345518a6572dbbaa1257b3ff67fff8248 /tools/fake_ide.ml
parent5b8bfee9d80e550cd81e326ec134430b2a4797a5 (diff)
[pp] Remove richpp from fake_ide.
Diffstat (limited to 'tools/fake_ide.ml')
-rw-r--r--tools/fake_ide.ml25
1 files changed, 7 insertions, 18 deletions
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index e89f19041..b538ba1d0 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -17,19 +17,8 @@ type coqtop = {
xml_parser : Xml_parser.t;
}
-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 Richpp.(content |> richpp_of_pp |> repr)
+let print_error msg =
+ Format.eprintf "fake_id: error: @[%a@]\n%!" (Pp.pp_with ?pp_tag:None) msg
let base_eval_call ?(print=true) ?(fail=true) call coqtop =
if print then prerr_endline (Xmlprotocol.pr_call call);
@@ -44,8 +33,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_xml Richpp.(s |> richpp_of_pp |> repr)
- | Interface.Fail (_,_,s) as x -> Printf.eprintf "%a\n%!" print_xml Richpp.(s |> richpp_of_pp |> repr); x
+ | Interface.Fail (_,_,s) when fail -> print_error s; exit 1
+ | Interface.Fail (_,_,s) as x -> print_error s; x
| x -> x
let eval_call c q = ignore(base_eval_call c q)
@@ -194,7 +183,7 @@ let print_document () =
module GUILogic = struct
let after_add = function
- | Interface.Fail (_,_,s) -> error_xml Richpp.(repr (richpp_of_pp s))
+ | Interface.Fail (_,_,s) -> print_error s; exit 1
| Interface.Good (id, (Util.Inl (), _)) ->
Document.assign_tip_id doc id
| Interface.Good (id, (Util.Inr tip, _)) ->
@@ -206,7 +195,7 @@ module GUILogic = struct
let at id id' _ = Stateid.equal id' id
let after_edit_at (id,need_unfocus) = function
- | Interface.Fail (_,_,s) -> error_xml Richpp.(repr (richpp_of_pp s))
+ | Interface.Fail (_,_,s) -> print_error s; exit 1
| Interface.Good (Util.Inl ()) ->
if need_unfocus then Document.unfocus doc;
ignore(Document.cut_at doc id);
@@ -329,7 +318,7 @@ let main =
let finish () =
match base_eval_call (Xmlprotocol.status true) coq with
| Interface.Good _ -> exit 0
- | Interface.Fail (_,_,s) -> error_xml Richpp.(repr (richpp_of_pp s)) in
+ | Interface.Fail (_,_,s) -> print_error s; exit 1 in
(* The main loop *)
init ();
while true do