diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-11-30 22:18:30 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-21 15:51:38 +0100 |
commit | a010de9bcaa33fc95a2a7cb6478ac21c95e3ad9e (patch) | |
tree | ebc4c3a345518a6572dbbaa1257b3ff67fff8248 | |
parent | 5b8bfee9d80e550cd81e326ec134430b2a4797a5 (diff) |
[pp] Remove richpp from fake_ide.
-rw-r--r-- | Makefile.build | 7 | ||||
-rw-r--r-- | tools/fake_ide.ml | 25 |
2 files changed, 10 insertions, 22 deletions
diff --git a/Makefile.build b/Makefile.build index c62420326..3b8d82e68 100644 --- a/Makefile.build +++ b/Makefile.build @@ -440,10 +440,9 @@ $(COQWORKMGR): $(call bestobj, lib/clib.cma stm/coqworkmgrApi.cmo tools/coqworkm # fake_ide : for debugging or test-suite purpose, a fake ide simulating # a connection to coqtop -ideslave -FAKEIDECMO:= lib/clib.cma lib/cErrors.cmo lib/spawn.cmo \ - ide/document.cmo ide/serialize.cmo ide/richpp.cmo ide/xml_lexer.cmo \ - ide/xml_parser.cmo ide/xml_printer.cmo ide/xmlprotocol.cmo \ - tools/fake_ide.cmo +FAKEIDECMO:= lib/clib.cma lib/cErrors.cmo lib/spawn.cmo ide/document.cmo \ + ide/serialize.cmo ide/xml_lexer.cmo ide/xml_parser.cmo ide/xml_printer.cmo \ + ide/xmlprotocol.cmo tools/fake_ide.cmo $(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPLOOPCMA:.cma=$(BESTDYN)) $(SHOW)'OCAMLBEST -o $@' 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 |