ide/{ide_slave.ml, interfaces}: Coerce input and output of requests between internal and external datatypes.

2 files changed, 48 insertions, 7 deletions

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index a0e315d9fe..4186f6cf03 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -119,7 +119,7 @@ let edit_at id =
 let query (s,id) = Stm.query ~at:id s; read_stdout ()
 
 let annotate phrase =
-  Xml_datatype.PCData "NOT_IMPLEMENTED_YET"
+  Xml_datatype.PCData "FIXME"
 
 (** Goal display *)
 
@@ -186,13 +186,21 @@ let process_goal sigma g =
       (Termops.compact_named_context_reverse (Environ.named_context env)) in
   { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }
 
+let export_pre_goals pgs =
+  {
+    Interface.fg_goals       = pgs.Proof.fg_goals;
+    Interface.bg_goals       = pgs.Proof.bg_goals;
+    Interface.shelved_goals  = pgs.Proof.shelved_goals;
+    Interface.given_up_goals = pgs.Proof.given_up_goals
+  }
+
 let goals () =
   Stm.finish ();
   let s = read_stdout () in
   if not (String.is_empty s) then msg_info (str s);
   try
     let pfts = Proof_global.give_me_the_proof () in
-    Some (Proof.map_structured_proof pfts process_goal)
+    Some (export_pre_goals (Proof.map_structured_proof pfts process_goal))
   with Proof_global.NoCurrentProof -> None
 
 let evars () =
@@ -252,15 +260,48 @@ let status force =
     Interface.status_proofnum = Stm.current_proof_depth ();
   }
 
-let search flags = Search.interface_search flags
+let export_coq_object t = {
+  Interface.coq_object_prefix = t.Search.coq_object_prefix;
+  Interface.coq_object_qualid = t.Search.coq_object_qualid;
+  Interface.coq_object_object = t.Search.coq_object_object
+}
+
+let import_search_constraint = function
+  | Interface.Name_Pattern s    -> Search.Name_Pattern s
+  | Interface.Type_Pattern s    -> Search.Type_Pattern s
+  | Interface.SubType_Pattern s -> Search.SubType_Pattern s
+  | Interface.In_Module ms      -> Search.In_Module ms
+  | Interface.Include_Blacklist -> Search.Include_Blacklist
+
+let search flags =
+  List.map export_coq_object (Search.interface_search (
+    List.map (fun (c, b) -> (import_search_constraint c, b)) flags)
+  )
+
+let export_option_value = function
+  | Goptions.BoolValue b   -> Interface.BoolValue b
+  | Goptions.IntValue x    -> Interface.IntValue x
+  | Goptions.StringValue s -> Interface.StringValue s
+
+let import_option_value = function
+  | Interface.BoolValue b   -> Goptions.BoolValue b
+  | Interface.IntValue x    -> Goptions.IntValue x
+  | Interface.StringValue s -> Goptions.StringValue s
+
+let export_option_state s = {
+  Interface.opt_sync  = s.Goptions.opt_sync;
+  Interface.opt_depr  = s.Goptions.opt_depr;
+  Interface.opt_name  = s.Goptions.opt_name;
+  Interface.opt_value = export_option_value s.Goptions.opt_value;
+}
 
 let get_options () =
   let table = Goptions.get_tables () in
-  let fold key state accu = (key, state) :: accu in
+  let fold key state accu = (key, export_option_state state) :: accu in
   Goptions.OptionMap.fold fold table []
 
 let set_options options =
-  let iter (name, value) = match value with
+  let iter (name, value) = match import_option_value value with
   | BoolValue b -> Goptions.set_bool_option_value name b
   | IntValue i -> Goptions.set_int_option_value name i
   | StringValue s -> Goptions.set_string_option_value name s
diff --git a/ide/interface.mli b/ide/interface.mli
index 226d1f8fb1..77a875b7d2 100644
--- a/ide/interface.mli
+++ b/ide/interface.mli
@@ -43,14 +43,14 @@ type 'a pre_goals = {
   fg_goals : 'a list;
   (** List of the focussed goals *)
   bg_goals : ('a list * 'a list) list;
-  (** Zipper representing the unfocussed background goals *)
+  (** Zipper representing the unfocused background goals *)
   shelved_goals : 'a list;
   (** List of the goals on the shelf. *)
   given_up_goals : 'a list;
   (** List of the goals that have been given up *)
 }
 
-type goals =  goal pre_goals
+type goals = goal pre_goals
 
 type hint = (string * string) list
 (** A list of tactics applicable and their appearance *)