diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-17 11:50:37 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-17 11:50:37 +0000 |
| commit | 26f21ad4387a2e9b9c16712859881fee5625f79b (patch) | |
| tree | f826ba272c3bb2e712561ef789b41c19206e9f49 /lib | |
| parent | 2095ca0c9d3b5b989d1c97c896ea9b34622c478f (diff) | |
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
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/serialize.ml | 4 | ||||
| -rw-r--r-- | lib/serialize.mli | 6 |
2 files changed, 7 insertions, 3 deletions
diff --git a/lib/serialize.ml b/lib/serialize.ml index 04405ac1b..3ad508d74 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 ad9a9c299..33da274f4 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 *) |