From 8ca5c2456d8e2a614a48b6d739f133fbcf97f1d1 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Sun, 13 May 2012 01:05:41 +0000
Subject: Added a SearchAbout-like primitive in coqtop interface.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15313 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/interface.mli | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

(limited to 'lib/interface.mli')

diff --git a/lib/interface.mli b/lib/interface.mli
index 02ca25a9de..47692191de 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -70,6 +70,28 @@ type option_state = {
   (** 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
+
+type search_answer = {
+  search_answer_full_path : string list;
+  search_answer_base_name : string;
+  search_answer_type : string;
+}
+
 type coq_info = {
   coqtop_version : string;
   protocol_version : string;
-- 
cgit v1.2.3