More XML marshalling functions

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

2 files changed, 79 insertions, 1 deletions

diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml
index 0cf84daf5a..b0815d87b9 100644
--- a/toplevel/ide_intf.ml
+++ b/toplevel/ide_intf.ml
@@ -116,7 +116,7 @@ let of_value f = function
   | None -> []
   | Some (s, e) -> [("loc_s", string_of_int s); ("loc_e", string_of_int e)]
   in
-  Element ("value", ["val", "fail"] @ loc, [])
+  Element ("value", ["val", "fail"] @ loc, [PCData msg])
 
 let to_value f = function
 | Element ("value", attrs, l) ->
@@ -169,6 +169,66 @@ let to_call = function
   end
 | _ -> raise Marshal_error
 
+let of_string s = Element ("string", [], [PCData s])
+
+let to_string = function
+| Element ("string", [], [PCData s]) -> s
+| _ -> raise Marshal_error
+
+let of_int i = Element ("int", [], [PCData (string_of_int i)])
+
+let to_int = function
+| Element ("int", [], [PCData s]) -> int_of_string s
+| _ -> raise Marshal_error
+
+let of_pair f g (x, y) = Element ("pair", [], [f x; g y])
+
+let to_pair f g = function
+| Element ("pair", [], [x; y]) -> (f x, g y)
+| _ -> raise Marshal_error
+
+let of_goals = function
+| Message s ->
+  Element ("goals", ["val", "message"], [of_string s])
+| Goals l ->
+  let of_string_menu = of_pair of_string (of_list (of_pair of_string of_string)) in
+  let xml = of_list (of_pair (of_list of_string_menu) of_string_menu) l in
+  Element ("goals", ["val", "goals"], [xml])
+
+let to_goals = function
+| Element ("goals", ["val", "message"], [s]) -> Message (to_string s)
+| Element ("goals", ["val", "goals"], [xml]) ->
+  let to_string_menu = to_pair to_string (to_list (to_pair to_string to_string)) in
+  let ans = to_list (to_pair (to_list to_string_menu) to_string_menu) xml in
+  Goals ans
+| _ -> raise Marshal_error
+
+let of_answer (q : 'a call) (r : 'a value) =
+  let convert = match q with
+  | Interp _ -> Obj.magic (of_string : string -> xml)
+  | Rewind _ -> Obj.magic (of_int : int -> xml)
+  | Goal -> Obj.magic (of_goals : goals -> xml)
+  | Status -> Obj.magic (of_string : string -> xml)
+  | InLoadPath _ -> Obj.magic (of_bool : bool -> xml)
+  | MkCases _ -> Obj.magic (of_list (of_list of_string) : string list list -> xml)
+  in
+  of_value convert r
+
+let to_answer xml =
+  let rec convert elt = match elt with
+  | Element (tpe, attrs, l) ->
+    begin match tpe with
+    | "string" -> Obj.magic (to_string elt)
+    | "int" -> Obj.magic (to_int elt)
+    | "goals" -> Obj.magic (to_goals elt)
+    | "bool" -> Obj.magic (to_bool elt)
+    | "list" -> Obj.magic (to_list convert elt)
+    | _ -> raise Marshal_error
+    end
+  | _ -> raise Marshal_error
+  in
+  to_value convert xml
+
 (** * Debug printing *)
 
 let pr_call = function
diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli
index 6a24a3cadb..9cb615265c 100644
--- a/toplevel/ide_intf.mli
+++ b/toplevel/ide_intf.mli
@@ -82,6 +82,18 @@ val abstract_eval_call :
 
 exception Marshal_error
 
+val of_bool : bool -> xml
+val to_bool : xml -> bool
+
+val of_string : string -> xml
+val to_string : xml -> string
+
+val of_int : int -> xml
+val to_int : xml -> int
+
+val of_pair : ('a -> xml) -> ('b -> xml) -> ('a * 'b) -> xml
+val to_pair : (xml -> 'a) -> (xml -> 'b) -> xml -> ('a * 'b)
+
 val of_list : ('a -> xml) -> 'a list -> xml
 val to_list : (xml -> 'a) -> xml -> 'a list
 
@@ -91,6 +103,12 @@ val to_value : (xml -> 'a) -> xml -> 'a value
 val of_call : 'a call -> xml
 val to_call : xml -> 'a call
 
+val of_goals : goals -> xml
+val to_goals : xml -> goals
+
+val of_answer : 'a call -> 'a value -> xml
+val to_answer : xml -> 'a value
+
 (** * Debug printing *)
 
 val pr_call : 'a call -> string