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, 14 insertions, 14 deletions

diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 681f0f2c8..bd3067d96 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -305,20 +305,20 @@ let eval_call c =
     r
   in
   let handler = {
-    Serialize.interp = interruptible interp;
-    Serialize.rewind = interruptible Backtrack.back;
-    Serialize.goals = interruptible goals;
-    Serialize.evars = interruptible evars;
-    Serialize.hints = interruptible hints;
-    Serialize.status = interruptible status;
-    Serialize.search = interruptible search;
-    Serialize.inloadpath = interruptible inloadpath;
-    Serialize.get_options = interruptible get_options;
-    Serialize.set_options = interruptible set_options;
-    Serialize.mkcases = interruptible Vernacentries.make_cases;
-    Serialize.quit = (fun () -> quit := true);
-    Serialize.about = interruptible about;
-    Serialize.handle_exn = handle_exn; }
+    Interface.interp = interruptible interp;
+    Interface.rewind = interruptible Backtrack.back;
+    Interface.goals = interruptible goals;
+    Interface.evars = interruptible evars;
+    Interface.hints = interruptible hints;
+    Interface.status = interruptible status;
+    Interface.search = interruptible search;
+    Interface.inloadpath = interruptible inloadpath;
+    Interface.get_options = interruptible get_options;
+    Interface.set_options = interruptible set_options;
+    Interface.mkcases = interruptible Vernacentries.make_cases;
+    Interface.quit = (fun () -> quit := true);
+    Interface.about = interruptible about;
+    Interface.handle_exn = handle_exn; }
   in
   (* If the messages of last command are still there, we remove them *)
   ignore (read_stdout ());