summaryrefslogtreecommitdiff
path: root/tools/fake_ide.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/fake_ide.ml')
-rw-r--r--tools/fake_ide.ml82
1 files changed, 41 insertions, 41 deletions
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 8fcca535..d48c6d0a 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** Fake_ide : Simulate a [coqide] talking to a [coqtop -ideslave] *)
@@ -12,24 +14,15 @@ let error s =
prerr_endline ("fake_id: error: "^s);
exit 1
+let pperr_endline pp = Format.eprintf "@[%a@]\n%!" Pp.pp_with pp
+
type coqtop = {
xml_printer : Xml_printer.t;
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.repr content)
+let print_error msg =
+ Format.eprintf "fake_id: error: @[%a@]\n%!" Pp.pp_with msg
let base_eval_call ?(print=true) ?(fail=true) call coqtop =
if print then prerr_endline (Xmlprotocol.pr_call call);
@@ -37,20 +30,15 @@ let base_eval_call ?(print=true) ?(fail=true) call coqtop =
Xml_printer.print coqtop.xml_printer xml_query;
let rec loop () =
let xml = Xml_parser.parse coqtop.xml_parser in
- match Xmlprotocol.is_message xml with
- | Some (level, _loc, content) ->
- logger level content;
+ if Xmlprotocol.is_feedback xml then
loop ()
- | None ->
- if Xmlprotocol.is_feedback xml then
- loop ()
- else Xmlprotocol.to_answer call xml
+ else Xmlprotocol.to_answer call xml
in
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.repr s)
- | Interface.Fail (_,_,s) as x -> Printf.eprintf "%a\n%!" print_xml (Richpp.repr s); 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)
@@ -186,7 +174,7 @@ let print_document () =
Str.global_replace (Str.regexp "^[\n ]*") ""
(if String.length s > 20 then String.sub s 0 17 ^ "..."
else s) in
- prerr_endline (Pp.string_of_ppcmds
+ pperr_endline (
(Document.print doc
(fun b state_id { name; text } ->
Pp.str (Printf.sprintf "%s[%10s, %3s] %s"
@@ -199,7 +187,7 @@ let print_document () =
module GUILogic = struct
let after_add = function
- | Interface.Fail (_,_,s) -> error_xml (Richpp.repr 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, _)) ->
@@ -211,7 +199,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 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);
@@ -261,16 +249,14 @@ let eval_print l coq =
let to_id, need_unfocus = get_id id in
after_edit_at (to_id, need_unfocus) (base_eval_call (edit_at to_id) coq)
| [ Tok(_,"QUERY"); Top []; Tok(_,phrase) ] ->
- eval_call (query (phrase,tip_id())) coq
+ eval_call (query (0,(phrase,tip_id()))) coq
| [ Tok(_,"QUERY"); Top [Tok(_,id)]; Tok(_,phrase) ] ->
let to_id, _ = get_id id in
- eval_call (query (phrase, to_id)) coq
+ eval_call (query (0,(phrase, to_id))) coq
| [ Tok(_,"WAIT") ] ->
- let phrase = "Stm Wait." in
- eval_call (query (phrase,tip_id())) coq
+ eval_call (wait ()) coq
| [ Tok(_,"JOIN") ] ->
- let phrase = "Stm JoinDocument." in
- eval_call (query (phrase,tip_id())) coq
+ eval_call (status true) coq
| [ Tok(_,"ASSERT"); Tok(_,"TIP"); Tok(_,id) ] ->
let to_id, _ = get_id id in
if not(Stateid.equal (Document.tip doc) to_id) then error "Wrong tip"
@@ -304,17 +290,31 @@ let usage () =
(Filename.basename Sys.argv.(0))
(Parser.print grammar))
-module Coqide = Spawn.Sync(struct end)
+module Coqide = Spawn.Sync ()
let main =
- Sys.set_signal Sys.sigpipe
+ if Sys.os_type = "Unix" then Sys.set_signal Sys.sigpipe
(Sys.Signal_handle
(fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1));
- let coqtop_name, coqtop_args, input_file = match Sys.argv with
- | [| _; f |] -> "coqtop",[|"-ideslave"|], f
+ let def_args = ["--xml_format=Ppcmds"; "-ideslave"] in
+ let coqtop_name = (* from ide/ideutils.ml *)
+ let prog_name = "fake_ide" in
+ let len_prog_name = String.length prog_name in
+ let fake_ide_path = Sys.executable_name in
+ let fake_ide_path_len = String.length fake_ide_path in
+ let pos = fake_ide_path_len - len_prog_name in
+ let rex = Str.regexp_string prog_name in
+ try
+ let i = Str.search_backward rex fake_ide_path pos in
+ String.sub fake_ide_path 0 i ^ "coqtop" ^
+ String.sub fake_ide_path (i + len_prog_name)
+ (fake_ide_path_len - i - len_prog_name)
+ with Not_found -> assert false in
+ let coqtop_args, input_file = match Sys.argv with
+ | [| _; f |] -> Array.of_list def_args, f
| [| _; f; ct |] ->
let ct = Str.split (Str.regexp " ") ct in
- List.hd ct, Array.of_list ("-ideslave" :: List.tl ct), f
+ Array.of_list (def_args @ ct), f
| _ -> usage () in
let inc = if input_file = "-" then stdin else open_in input_file in
let coq =
@@ -334,7 +334,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 s) in
+ | Interface.Fail (_,_,s) -> print_error s; exit 1 in
(* The main loop *)
init ();
while true do
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 23:05:46 +0000