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/

1 files changed, 0 insertions, 267 deletions

diff --git a/lib/interface.mli b/lib/interface.mli
deleted file mode 100644
index c8fe068e60..0000000000
--- a/lib/interface.mli
+++ /dev/null
@@ -1,267 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** * Declarative part of the interface of CoqIde calls to Coq *)
-
-(** * Generic structures *)
-
-type raw = bool
-type verbose = bool
-
-(** The type of coqtop goals *)
-type goal = {
-  goal_id : string;
-  (** Unique goal identifier *)
-  goal_hyp : string list;
-  (** List of hypotheses *)
-  goal_ccl : string;
-  (** Goal conclusion *)
-}
-
-type evar = {
-  evar_info : string;
-  (** A string describing an evar: type, number, environment *)
-}
-
-type status = {
-  status_path : string list;
-  (** Module path of the current proof *)
-  status_proofname : string option;
-  (** Current proof name. [None] if no focussed proof is in progress *)
-  status_allproofs : string list;
-  (** List of all pending proofs. Order is not significant *)
-  status_proofnum : int;
-  (** An id describing the state of the current proof. *)
-}
-
-type goals = {
-  fg_goals : goal list;
-  (** List of the focussed goals *)
-  bg_goals : (goal list * goal list) list;
-  (** Zipper representing the unfocussed background goals *)
-  shelved_goals : goal list;
-  (** List of the goals on the shelf. *)
-  given_up_goals : goal list;
-  (** List of the goals that have been given up *)
-}
-
-type hint = (string * string) list
-(** A list of tactics applicable and their appearance *)
-
-type option_name = string list
-
-type option_value =
-  | BoolValue   of bool
-  | IntValue    of int option
-  | StringValue of string
-
-(** Summary of an option status *)
-type option_state = {
-  opt_sync  : bool;
-  (** Whether an option is synchronous *)
-  opt_depr  : bool;
-  (** Wheter an option is deprecated *)
-  opt_name  : string;
-  (** A short string that is displayed when using [Test] *)
-  opt_value : option_value;
-  (** The current value of the option *)
-}
-
-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
-
-(** A list of search constraints; the boolean flag is set to [false] whenever
-    the flag should be negated. *)
-type search_flags = (search_constraint * bool) list
-
-(** A named object in Coq. [coq_object_qualid] is the shortest path defined for
-    the user. [coq_object_prefix] is the missing part to recover the fully
-    qualified name, i.e [fully_qualified = coq_object_prefix + coq_object_qualid].
-    [coq_object_object] is the actual content of the object. *)
-type 'a coq_object = {
-  coq_object_prefix : string list;
-  coq_object_qualid : string list;
-  coq_object_object : 'a;
-}
-
-type coq_info = {
-  coqtop_version : string;
-  protocol_version : string;
-  release_date : string;
-  compile_date : string;
-}
-
-(** Coq unstructured messages *)
-
-type message_level =
-  | Debug of string
-  | Info
-  | Notice
-  | Warning
-  | Error
-
-type message = {
-  message_level : message_level;
-  message_content : string;
-}
-
-(** Coq "semantic" infos obtained during parsing/execution *)
-type edit_id = int
-type state_id = Stateid.t
-type edit_or_state_id = Edit of edit_id | State of state_id
-
-type feedback_content =
-  | AddedAxiom
-  | Processed
-  | Incomplete
-  | Complete
-  | GlobRef of Loc.t * string * string * string * string
-  | GlobDef of Loc.t * string * string * string
-  | ErrorMsg of Loc.t * string
-  | InProgress of int
-  | SlaveStatus of int * string
-  | ProcessingInMaster
-
-type feedback = {
-  id : edit_or_state_id;
-  content : feedback_content;
-}
-
-(** Calls result *)
-
-type location = (int * int) option (* start and end of the error *)
-
-(* The fail case carries the current state_id of the prover, the GUI
-   should probably retract to that point *)
-type 'a value =
-  | Good of 'a
-  | Fail of (state_id * location * string)
-
-type ('a, 'b) union = ('a, 'b) Util.union
-
-(* Request/Reply message protocol between Coq and CoqIde *)
-
-(**  [add ((s,eid),(sid,v))] adds the phrase [s] with edit id [eid]
-     on top of the current edit position (that is asserted to be [sid])
-     verbosely if [v] is true.  The response [(id,(rc,s)] is the new state
-     [id] assigned to the phrase, some output [s].  [rc] is [Inl] if the new
-     state id is the tip of the edit point, or [Inr tip] if the new phrase
-     closes a focus and [tip] is the new edit tip *)
-type add_sty = (string * edit_id) * (state_id * verbose)
-type add_rty = state_id * ((unit, state_id) union * string)
-
-(** [edit_at id] declares the user wants to edit just after [id].
-    The response is [Inl] if the document has been rewound to that point,
-    [Inr (start,(stop,tip))] if [id] is in a zone that can be focused.
-    In that case the zone is delimited by [start] and [stop] while [tip]
-    is the new document [tip].  Edits made by subsequent [add] are always
-    performend on top of [id]. *)
-type edit_at_sty = state_id
-type edit_at_rty = (unit, state_id * (state_id * state_id)) union
-
-(** [query s id] executes [s] at state [id] and does not record any state
-    change but for the printings that are sent in response *)
-type query_sty = string * state_id
-type query_rty = string
-
-(** Fetching the list of current goals. Return [None] if no proof is in
-    progress, [Some gl] otherwise. *)
-type goals_sty = unit
-type goals_rty = goals option
-
-(** Retrieve the list of unintantiated evars in the current proof. [None] if no
-    proof is in progress. *)
-type evars_sty = unit
-type evars_rty = evar list option
-
-(** Retrieving the tactics applicable to the current goal. [None] if there is
-    no proof in progress. *)
-type hints_sty = unit
-type hints_rty = (hint list * hint) option
-
-(** The status, for instance "Ready in SomeSection, proving Foo", the
-    input boolean (if true) forces the evaluation of all unevaluated
-    statements *)
-type status_sty = bool
-type status_rty = status
-
-(** Search for objects satisfying the given search flags. *)
-type search_sty = search_flags
-type search_rty = string coq_object list
-
-(** Retrieve the list of options of the current toplevel *)
-type get_options_sty = unit
-type get_options_rty = (option_name * option_state) list
-
-(** Set the options to the given value. Warning: this is not atomic, so whenever
-    the call fails, the option state can be messed up... This is the caller duty
-    to check that everything is correct. *)
-type set_options_sty = (option_name * option_value) list
-type set_options_rty = unit
-
-(** Create a "match" template for a given inductive type.
-    For each branch of the match, we list the constructor name
-    followed by enough pattern variables. *)
-type mkcases_sty = string
-type mkcases_rty = string list list
-
-(** Quit gracefully the interpreter. *)
-type quit_sty = unit
-type quit_rty = unit
-
-(* Initialize, and return the initial state id.  The argument is the filename.
- * If its directory is not in dirpath, it adds it.  It also loads
- * compilation hints for the filename. *)
-type init_sty = string option
-type init_rty = state_id
-
-type about_sty = unit
-type about_rty = coq_info
-
-type handle_exn_sty = exn
-type handle_exn_rty = state_id * location * string
-
-(* Retrocompatibility stuff *)
-type interp_sty = (raw * verbose) * string
-(* spiwack: [Inl] for safe and [Inr] for unsafe. *)
-type interp_rty = state_id * (string,string) Util.union
-
-type stop_worker_sty = int
-type stop_worker_rty = unit
-
-
-type handler = {
-  add         : add_sty         -> add_rty;
-  edit_at     : edit_at_sty     -> edit_at_rty;
-  query       : query_sty       -> query_rty;
-  goals       : goals_sty       -> goals_rty;
-  evars       : evars_sty       -> evars_rty;
-  hints       : hints_sty       -> hints_rty;
-  status      : status_sty      -> status_rty;
-  search      : search_sty      -> search_rty;
-  get_options : get_options_sty -> get_options_rty;
-  set_options : set_options_sty -> set_options_rty;
-  mkcases     : mkcases_sty     -> mkcases_rty;
-  about       : about_sty       -> about_rty;
-  stop_worker : stop_worker_sty -> stop_worker_rty;
-  handle_exn  : handle_exn_sty  -> handle_exn_rty;
-  init        : init_sty        -> init_rty;
-  quit        : quit_sty        -> quit_rty;
-  (* Retrocompatibility stuff *)
-  interp      : interp_sty      -> interp_rty;
-}
-