diff options
author | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-04-12 20:49:01 +0000 |
---|---|---|
committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-04-12 20:49:01 +0000 |
commit | 59c9403ceb09a35ed219b522e9f5abdb50615d76 (patch) | |
tree | f7d3e521f6a948defdce70e00c718c6bdc7b696e /tools/fake_ide.ml | |
parent | 1b9428c4e4ce6f2dbe98d0f753b062ae8634a954 (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.ml | 32 |
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); ] |