diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:04:54 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:04:54 +0100 |
commit | 39efc41237ec906226a3a53d7396d51173495204 (patch) | |
tree | 87cd58d72d43469d2a2a0a127c1060d7c9e0206b /tools/fake_ide.ml | |
parent | 5fe4ac437bed43547b3695664974f492b55cb553 (diff) | |
parent | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff) |
Remove non-DFSG contentsupstream/8.4_beta+dfsg
Diffstat (limited to 'tools/fake_ide.ml')
-rw-r--r-- | tools/fake_ide.ml | 84 |
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..f2255981 --- /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-2010 *) +(* \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 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 |