all coqide specific files moved into ide/

lib/interface split into:
 - lib/feedback
     subscribe-based feedback bus (also used by coqidetop)
 - ide/interface
     definition of coqide protocol messages
   lib/pp
     structured info/err/warn messages

lib/serialize split into:
 - lib/serialize
     generic xml serialization (list, pairs, int, loc, ...)
     used by coqide but potentially useful to other interfaces
 - ide/xmlprotocol
     serialization of protocol messages as in ide/interface

the only drawback is that coqidetop needs -thread
and I had to pass that option to all files in ide/

5 files changed, 47 insertions, 17 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 45aa980b79..2f778be364 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -95,7 +95,7 @@ let init_load_path () =
     (* main loops *)
     Mltop.add_ml_dir (coqlib/"toploop");
     if Coq_config.local then Mltop.add_ml_dir (coqlib/"stm");
-    if Coq_config.local then Mltop.add_ml_dir (coqlib/"idetop");
+    if Coq_config.local then Mltop.add_ml_dir (coqlib/"ide");
     (* then standard library *)
     add_stdlib_path ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false;
     (* then plugins *)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 0523ffd44a..d64e3d979d 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -389,8 +389,6 @@ let parse_args arglist =
     |"-emacs" -> set_emacs ()
     |"-filteropts" -> filter_opts := true
     |"-h"|"-H"|"-?"|"-help"|"--help" -> usage ()
-    |"--help-XML-protocol" ->
-        Serialize.document Xml_printer.to_string_fmt; exit 0
     |"-ideslave" -> toploop := Some "coqidetop"; Flags.ide_slave := true
     |"-impredicative-set" -> set_engagement Declarations.ImpredicativeSet
     |"-indices-matter" -> Indtypes.enforce_indices_matter ()
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 37403504db..016b9f22b5 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -217,26 +217,39 @@ let search_about items mods =
   let () = generic_search iter in
   format_display !ans
 
+type search_constraint =
+  | Name_Pattern of string
+  | Type_Pattern of string
+  | SubType_Pattern of string
+  | In_Module of string list
+  | Include_Blacklist
+
+type 'a coq_object = {
+  coq_object_prefix : string list;
+  coq_object_qualid : string list;
+  coq_object_object : 'a;
+}
+
 let interface_search flags =
   let env = Global.env () in
   let rec extract_flags name tpe subtpe mods blacklist = function
   | [] -> (name, tpe, subtpe, mods, blacklist)
-  | (Interface.Name_Pattern s, b) :: l ->
+  | (Name_Pattern s, b) :: l ->
     let regexp =
       try Str.regexp s
       with e when Errors.noncritical e ->
         Errors.error ("Invalid regexp: " ^ s)
     in
     extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l
-  | (Interface.Type_Pattern s, b) :: l ->
+  | (Type_Pattern s, b) :: l ->
     let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in
     let (_, pat) = Constrintern.intern_constr_pattern env constr in
     extract_flags name ((pat, b) :: tpe) subtpe mods blacklist l
-  | (Interface.SubType_Pattern s, b) :: l ->
+  | (SubType_Pattern s, b) :: l ->
     let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in
     let (_, pat) = Constrintern.intern_constr_pattern env constr in
     extract_flags name tpe ((pat, b) :: subtpe) mods blacklist l
-  | (Interface.In_Module m, b) :: l ->
+  | (In_Module m, b) :: l ->
     let path = String.concat "." m in
     let m = Pcoq.parse_string Pcoq.Constr.global path in
     let (_, qid) = Libnames.qualid_of_reference m in
@@ -246,7 +259,7 @@ let interface_search flags =
         Errors.error ("Module " ^ path ^ " not found.")
     in
     extract_flags name tpe subtpe ((id, b) :: mods) blacklist l
-  | (Interface.Include_Blacklist, b) :: l ->
+  | (Include_Blacklist, b) :: l ->
     extract_flags name tpe subtpe mods b l
   in
   let (name, tpe, subtpe, mods, blacklist) =
@@ -295,9 +308,9 @@ let interface_search flags =
     in
     let (prefix, qualid) = prefix fullpath shortpath [Id.to_string basename] in
     let answer = {
-      Interface.coq_object_prefix = prefix;
-      Interface.coq_object_qualid = qualid;
-      Interface.coq_object_object = string_of_ppcmds (pr_lconstr_env env constr);
+      coq_object_prefix = prefix;
+      coq_object_qualid = qualid;
+      coq_object_object = string_of_ppcmds (pr_lconstr_env env constr);
     } in
     ans := answer :: !ans;
   in
diff --git a/toplevel/search.mli b/toplevel/search.mli
index c06a64be17..a69a8db79c 100644
--- a/toplevel/search.mli
+++ b/toplevel/search.mli
@@ -40,8 +40,27 @@ val search_rewrite : constr_pattern -> DirPath.t list * bool -> std_ppcmds
 val search_pattern : constr_pattern -> DirPath.t list * bool -> std_ppcmds
 val search_about   : (bool * glob_search_about_item) list ->
   DirPath.t list * bool -> std_ppcmds
-val interface_search : (Interface.search_constraint * bool) list ->
-  string Interface.coq_object list
+
+type search_constraint =
+  (** Whether the name satisfies a regexp (uses Ocaml Str syntax) *)
+  | Name_Pattern of string
+  (** Whether the object type satisfies a pattern *)
+  | Type_Pattern of string
+  (** Whether some subtype of object type satisfies a pattern *)
+  | SubType_Pattern of string
+  (** Whether the object pertains to a module *)
+  | In_Module of string list
+  (** Bypass the Search blacklist *)
+  | Include_Blacklist
+
+type 'a coq_object = {
+  coq_object_prefix : string list;
+  coq_object_qualid : string list;
+  coq_object_object : 'a;
+}
+
+val interface_search : (search_constraint * bool) list ->
+  string coq_object list
 
 (** {6 Generic search function} *)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 2e97b74d66..b1ed564d81 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -517,7 +517,7 @@ let vernac_exact_proof c =
      called only at the begining of a proof. *)
   let status = by (Tactics.New.exact_proof c) in
   save_proof (Vernacexpr.Proved(true,None));
-  if not status then Pp.feedback Interface.AddedAxiom
+  if not status then Pp.feedback Feedback.AddedAxiom
 
 let vernac_assumption locality poly (local, kind) l nl =
   let local = enforce_locality_exp locality local in
@@ -529,7 +529,7 @@ let vernac_assumption locality poly (local, kind) l nl =
 	if global then Dumpglob.dump_definition lid false "ax"
 	else Dumpglob.dump_definition lid true "var") idl) l;
   let status = do_assumptions kind nl l in
-  if not status then Pp.feedback Interface.AddedAxiom
+  if not status then Pp.feedback Feedback.AddedAxiom
 
 let vernac_record k poly finite infer struc binders sort nameopt cfs =
   let const = match nameopt with
@@ -795,7 +795,7 @@ let vernac_instance abst locality poly sup inst props pri =
   ignore(Classes.new_instance ~abstract:abst ~global poly sup inst props pri)
 
 let vernac_context poly l =
-  if not (Classes.context poly l) then Pp.feedback Interface.AddedAxiom
+  if not (Classes.context poly l) then Pp.feedback Feedback.AddedAxiom
 
 let vernac_declare_instances locality ids pri =
   let glob = not (make_section_locality locality) in
@@ -825,7 +825,7 @@ let vernac_solve n tcom b =
     let p = Proof.maximal_unfocus command_focus p in
     p,status) in
     print_subgoals();
-    if not status then Pp.feedback Interface.AddedAxiom
+    if not status then Pp.feedback Feedback.AddedAxiom
  
 
   (* A command which should be a tactic. It has been