aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/fake_ide.ml
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-04-12 20:49:01 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-04-12 20:49:01 +0000
commit59c9403ceb09a35ed219b522e9f5abdb50615d76 (patch)
treef7d3e521f6a948defdce70e00c718c6bdc7b696e /tools/fake_ide.ml
parent1b9428c4e4ce6f2dbe98d0f753b062ae8634a954 (diff)
lib directory is cut in 2 cma.
- Clib that does not depend on camlpX and is made to be shared by all coq tools/scripts/... - Lib that is Coqtop specific As a side effect for the build system : - Coq_config is in Clib and does not appears in makefiles - only the BEST version of coqc and coqmktop is made - ocamlbuild build system fails latter but is still broken (ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15144 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/fake_ide.ml')
-rw-r--r--tools/fake_ide.ml32
1 files changed, 16 insertions, 16 deletions
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index f2255981a..31303b5ba 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -15,28 +15,28 @@ 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
+let eval_call (call:'a Serialize.call) =
+ prerr_endline (Serialize.pr_call call);
+ let xml_query = Serialize.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);
+ let res = Serialize.to_answer xml_answer in
+ prerr_endline (Serialize.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));
+ [ "INTERPRAWSILENT", (fun s -> eval_call (Serialize.interp (true,false,s)));
+ "INTERPRAW", (fun s -> eval_call (Serialize.interp (true,true,s)));
+ "INTERPSILENT", (fun s -> eval_call (Serialize.interp (false,false,s)));
+ "INTERP", (fun s -> eval_call (Serialize.interp (false,true,s)));
+ "REWIND", (fun s -> eval_call (Serialize.rewind (int_of_string s)));
+ "GOALS", (fun _ -> eval_call Serialize.goals);
+ "HINTS", (fun _ -> eval_call Serialize.hints);
+ "GETOPTIONS", (fun _ -> eval_call Serialize.get_options);
+ "STATUS", (fun _ -> eval_call Serialize.status);
+ "INLOADPATH", (fun s -> eval_call (Serialize.inloadpath s));
+ "MKCASES", (fun s -> eval_call (Serialize.mkcases s));
"#", (fun _ -> raise Comment);
]