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.ml84
1 files changed, 84 insertions, 0 deletions
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
new file mode 100644
index 00000000..22a36ede
--- /dev/null
+++ b/tools/fake_ide.ml
@@ -0,0 +1,84 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** Fake_ide : Simulate a [coqide] talking to a [coqtop -ideslave] *)
+
+exception Comment
+
+let coqtop = ref (stdin, stdout)
+
+let p = Xml_parser.make ()
+let () = Xml_parser.check_eof p false
+
+let eval_call (call:'a Ide_intf.call) =
+ prerr_endline (Ide_intf.pr_call call);
+ let xml_query = Ide_intf.of_call call in
+ Xml_utils.print_xml (snd !coqtop) xml_query;
+ flush (snd !coqtop);
+ let xml_answer = Xml_parser.parse p (Xml_parser.SChannel (fst !coqtop)) in
+ let res = Ide_intf.to_answer xml_answer call in
+ prerr_endline (Ide_intf.pr_full_value call res);
+ match res with Interface.Fail _ -> exit 1 | _ -> ()
+
+let commands =
+ [ "INTERPRAWSILENT", (fun s -> eval_call (Ide_intf.interp (true,false,s)));
+ "INTERPRAW", (fun s -> eval_call (Ide_intf.interp (true,true,s)));
+ "INTERPSILENT", (fun s -> eval_call (Ide_intf.interp (false,false,s)));
+ "INTERP", (fun s -> eval_call (Ide_intf.interp (false,true,s)));
+ "REWIND", (fun s -> eval_call (Ide_intf.rewind (int_of_string s)));
+ "GOALS", (fun _ -> eval_call Ide_intf.goals);
+ "HINTS", (fun _ -> eval_call Ide_intf.hints);
+ "GETOPTIONS", (fun _ -> eval_call Ide_intf.get_options);
+ "STATUS", (fun _ -> eval_call Ide_intf.status);
+ "INLOADPATH", (fun s -> eval_call (Ide_intf.inloadpath s));
+ "MKCASES", (fun s -> eval_call (Ide_intf.mkcases s));
+ "#", (fun _ -> raise Comment);
+ ]
+
+let read_eval_print line =
+ let lline = String.length line in
+ let rec find_cmd = function
+ | [] -> prerr_endline ("Error: Unknown API Command :"^line); exit 1
+ | (cmd,fn) :: cmds ->
+ let lcmd = String.length cmd in
+ if lline >= lcmd && String.sub line 0 lcmd = cmd then
+ let arg = try String.sub line (lcmd+1) (lline-lcmd-1) with _ -> ""
+ in fn arg
+ else find_cmd cmds
+ in
+ find_cmd commands
+
+let usage () =
+ Printf.printf
+ "A fake coqide process talking to a coqtop -ideslave.\n\
+ Usage: %s [<coqtop>]\n\
+ Input syntax is one API call per line, the keyword coming first,\n\
+ with the rest of the line as string argument (e.g. INTERP Check plus.)\n\
+ Supported API keywords are:\n" (Filename.basename Sys.argv.(0));
+ List.iter (fun (s,_) -> Printf.printf "\t%s\n" s) commands;
+ exit 1
+
+let main =
+ Sys.set_signal Sys.sigpipe
+ (Sys.Signal_handle
+ (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1));
+ let coqtop_name = match Array.length Sys.argv with
+ | 1 -> "coqtop"
+ | 2 when Sys.argv.(1) <> "-help" -> Sys.argv.(1)
+ | _ -> usage ()
+ in
+ coqtop := Unix.open_process (coqtop_name^" -ideslave");
+ while true do
+ let l = try read_line () with End_of_file -> exit 0
+ in
+ try read_eval_print l
+ with
+ | Comment -> ()
+ | e ->
+ prerr_endline ("Uncaught exception" ^ Printexc.to_string e); exit 1
+ done