More type-safe interface to Coq XML API.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15813 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 11 insertions, 7 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index cdc3256517..8607241b4e 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -351,7 +351,7 @@ let try_grab coqtop f g =
 
 (** Cf [Ide_intf] for more details *)
 
-let eval_call coqtop logger (c:'a Serialize.call) =
+let eval_call coqtop logger c =
   (** Retrieve the messages sent by coqtop until an answer has been received *)
   let rec loop () =
     let xml = Xml_parser.parse coqtop.xml_parser in
@@ -361,7 +361,7 @@ let eval_call coqtop logger (c:'a Serialize.call) =
       let content = message.Interface.message_content in
       let () = logger level content  in
       loop ()
-    else (Serialize.to_answer xml : 'a Interface.value)
+    else (Serialize.to_answer xml c)
   in
   try
     Xml_utils.print_xml coqtop.cin (Serialize.of_call c);
diff --git a/lib/serialize.ml b/lib/serialize.ml
index 04405ac1bf..3ad508d74c 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -37,6 +37,8 @@ type 'a call =
   | Quit
   | About
 
+type unknown
+
 (** The structure that coqtop should implement *)
 
 type handler = {
@@ -476,7 +478,7 @@ let of_answer (q : 'a call) (r : 'a value) =
   in
   of_value convert r
 
-let to_answer xml =
+let to_answer xml _ =
   let rec convert elt = match elt with
   | Element (tpe, attrs, l) ->
     begin match tpe with
diff --git a/lib/serialize.mli b/lib/serialize.mli
index ad9a9c2994..33da274f41 100644
--- a/lib/serialize.mli
+++ b/lib/serialize.mli
@@ -16,6 +16,8 @@ type xml =
 
 type 'a call
 
+type unknown
+
 (** Running a command (given as a string).
     - The 1st flag indicates whether to use "raw" mode
       (less sanity checks, no impact on the undo stack).
@@ -107,14 +109,14 @@ val of_value : ('a -> xml) -> 'a value -> xml
 val to_value : (xml -> 'a) -> xml -> 'a value
 
 val of_call : 'a call -> xml
-val to_call : xml -> 'a call
+val to_call : xml -> unknown call
 
 val of_message : message -> xml
 val to_message : xml -> message
 val is_message : xml -> bool
 
 val of_answer : 'a call -> 'a value -> xml
-val to_answer : xml -> 'a value
+val to_answer : xml -> 'a call -> 'a value
 
 (** * Debug printing *)
 
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index f13a8d4357..5fafe2991c 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -18,7 +18,7 @@ type coqtop = {
 
 let logger level content = ()
 
-let eval_call (call:'a Serialize.call) coqtop =
+let eval_call call coqtop =
   prerr_endline (Serialize.pr_call call);
   let xml_query = Serialize.of_call call in
   Xml_utils.print_xml coqtop.out_chan xml_query;
@@ -31,7 +31,7 @@ let eval_call (call:'a Serialize.call) coqtop =
       let content = message.Interface.message_content in
       let () = logger level content in
       loop ()
-    else (Serialize.to_answer xml : 'a Interface.value)
+    else (Serialize.to_answer xml call)
   in
   let res = loop () in
   prerr_endline (Serialize.pr_full_value call res);