aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coq.ml')
-rw-r--r--ide/coq.ml24
1 files changed, 12 insertions, 12 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index 16a07b01c..cf73749a8 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -176,19 +176,19 @@ let kill_coqtop coqtop =
let p = Xml_parser.make ()
let () = Xml_parser.check_eof p false
-let eval_call coqtop (c:'a Ide_intf.call) =
- Xml_utils.print_xml coqtop.cin (Ide_intf.of_call c);
+let eval_call coqtop (c:'a Serialize.call) =
+ Xml_utils.print_xml coqtop.cin (Serialize.of_call c);
flush coqtop.cin;
let xml = Xml_parser.parse p (Xml_parser.SChannel coqtop.cout) in
- (Ide_intf.to_answer xml : 'a Interface.value)
+ (Serialize.to_answer xml : 'a Interface.value)
let interp coqtop ?(raw=false) ?(verbose=true) s =
- eval_call coqtop (Ide_intf.interp (raw,verbose,s))
-let rewind coqtop i = eval_call coqtop (Ide_intf.rewind i)
-let inloadpath coqtop s = eval_call coqtop (Ide_intf.inloadpath s)
-let mkcases coqtop s = eval_call coqtop (Ide_intf.mkcases s)
-let status coqtop = eval_call coqtop Ide_intf.status
-let hints coqtop = eval_call coqtop Ide_intf.hints
+ eval_call coqtop (Serialize.interp (raw,verbose,s))
+let rewind coqtop i = eval_call coqtop (Serialize.rewind i)
+let inloadpath coqtop s = eval_call coqtop (Serialize.inloadpath s)
+let mkcases coqtop s = eval_call coqtop (Serialize.mkcases s)
+let status coqtop = eval_call coqtop Serialize.status
+let hints coqtop = eval_call coqtop Serialize.hints
module PrintOpt =
struct
@@ -208,7 +208,7 @@ struct
let set coqtop options =
let () = List.iter (fun (name, v) -> Hashtbl.replace state_hack name v) options in
let options = List.map (fun (name, v) -> (name, Interface.BoolValue v)) options in
- match eval_call coqtop (Ide_intf.set_options options) with
+ match eval_call coqtop (Serialize.set_options options) with
| Interface.Good () -> ()
| _ -> raise (Failure "Cannot set options.")
@@ -220,8 +220,8 @@ end
let goals coqtop =
let () = PrintOpt.enforce_hack coqtop in
- eval_call coqtop Ide_intf.goals
+ eval_call coqtop Serialize.goals
let evars coqtop =
let () = PrintOpt.enforce_hack coqtop in
- eval_call coqtop Ide_intf.evars
+ eval_call coqtop Serialize.evars