[stm] Break stm/toplevel dependency loop.

Currently, the STM, vernac interpretation, and the toplevel are
intertwined in a mutual dependency that needs to be resolved using
imperative callbacks.

This is problematic for a few reasons, in particular it makes the
interpretation of commands that affect the document quite intricate.

As a first step, we split the `toplevel/` directory into two: "pure"
vernac interpretation is moved to the `vernac/` directory, on which
the STM relies.

Test suite passes, and only one command seems to be disabled with this
approach, "Show Script" which is to my understanding
obsolete. Subsequent commits will fix this and refine some of the
invariants that are not needed anymore.

1 files changed, 84 insertions, 0 deletions

diff --git a/vernac/search.mli b/vernac/search.mli
new file mode 100644
index 000000000..c9167c485
--- /dev/null
+++ b/vernac/search.mli
@@ -0,0 +1,84 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Names
+open Term
+open Environ
+open Pattern
+open Globnames
+
+(** {6 Search facilities. } *)
+
+type glob_search_about_item =
+  | GlobSearchSubPattern of constr_pattern
+  | GlobSearchString of string
+
+type filter_function = global_reference -> env -> constr -> bool
+type display_function = global_reference -> env -> constr -> unit
+
+(** {6 Generic filter functions} *)
+
+val blacklist_filter : filter_function
+(** Check whether a reference is blacklisted. *)
+
+val module_filter : DirPath.t list * bool -> filter_function
+(** Check whether a reference pertains or not to a set of modules *)
+
+val search_about_filter : glob_search_about_item -> filter_function
+(** Check whether a reference matches a SearchAbout query. *)
+
+(** {6 Specialized search functions}
+
+[search_xxx gl pattern modinout] searches the hypothesis of the [gl]th
+goal and the global environment for things matching [pattern] and
+satisfying module exclude/include clauses of [modinout]. *)
+
+val search_by_head : int option -> constr_pattern -> DirPath.t list * bool
+                  -> display_function -> unit
+val search_rewrite : int option -> constr_pattern -> DirPath.t list * bool
+                  -> display_function -> unit
+val search_pattern : int option -> constr_pattern -> DirPath.t list * bool
+                  -> display_function -> unit
+val search_about   : int option -> (bool * glob_search_about_item) list
+                  -> DirPath.t list * bool -> display_function -> unit
+
+type search_constraint =
+  (** Whether the name satisfies a regexp (uses Ocaml Str syntax) *)
+  | Name_Pattern of Str.regexp
+  (** Whether the object type satisfies a pattern *)
+  | Type_Pattern of Pattern.constr_pattern
+  (** Whether some subtype of object type satisfies a pattern *)
+  | SubType_Pattern of Pattern.constr_pattern
+  (** Whether the object pertains to a module *)
+  | In_Module of Names.DirPath.t
+  (** 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 : ?glnum:int -> (search_constraint * bool) list ->
+  string coq_object list
+
+(** {6 Generic search function} *)
+
+val generic_search : int option -> display_function -> unit
+(** This function iterates over all hypothesis of the goal numbered
+    [glnum] (if present) and all known declarations. *)
+
+(** {6 Search function modifiers} *)
+
+val prioritize_search : (display_function -> unit) -> display_function -> unit
+(** [prioritize_search iter] iterates over the values of [iter] (seen
+    as a sequence of declarations), in a relevance order. This requires to
+    perform the entire iteration of [iter] before starting streaming. So
+    [prioritize_search] should not be used for low-latency streaming. *)