interface.mli and serialize.ml reworked to avoid copy/paste of types

With this commit the types involved in the protocol between Coq and
Coqide are written once and for all in interface.mli

serialize.ml is monkey code that contains a reified version of these
types and the related machinery needed to marshal values in these types
to/from xml in a modular way.  This file should be automatically
generated from the spec of the protocol in an ideal world.
Phantom types are used to statically check that the reified form
of the types is in sync with the one declared in interface.mli

The benefit of this commit is that changing the protocol is easier:
one changes the types in interface.mli and lets ocamlc spot all the
places that needs to be modified.
This is a necessity if one plays with the protocol very often, like
in my Paral-ITP branch.

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

1 files changed, 11 insertions, 6 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index fd6de80d1..121981110 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -540,13 +540,18 @@ let eval_call ?(logger=default_logger) call handle k =
   Minilib.log "End eval_call";
   Void
 
-let interp ?(logger=default_logger) ?(raw=false) ?(verbose=true) s =
-  eval_call ~logger (Serialize.interp (raw,verbose,s))
+let interp ?(logger=default_logger) ?(raw=false) ?(verbose=true) s h k =
+  eval_call ~logger (Serialize.interp (raw,verbose,s)) h
+    (function
+     | Interface.Good (Util.Inl v) -> k (Interface.Good v)
+     | Interface.Good (Util.Inr v) -> k (Interface.Unsafe v)
+     | Interface.Fail v -> k (Interface.Fail v)
+     | Interface.Unsafe _ -> assert false)
 let rewind i = eval_call (Serialize.rewind i)
 let inloadpath s = eval_call (Serialize.inloadpath s)
 let mkcases s = eval_call (Serialize.mkcases s)
-let status = eval_call Serialize.status
-let hints = eval_call Serialize.hints
+let status = eval_call (Serialize.status ())
+let hints = eval_call (Serialize.hints ())
 let search flags = eval_call (Serialize.search flags)
 
 module PrintOpt =
@@ -612,7 +617,7 @@ struct
 end
 
 let goals h k =
-  PrintOpt.enforce h (fun () -> eval_call Serialize.goals h k)
+  PrintOpt.enforce h (fun () -> eval_call (Serialize.goals ()) h k)
 
 let evars h k =
-  PrintOpt.enforce h (fun () -> eval_call Serialize.evars h k)
+  PrintOpt.enforce h (fun () -> eval_call (Serialize.evars ()) h k)