[search] Don't build intermediate lists in search.

This patch converts the `search_*` functions to use an iter-style API.

Consequently, the Search Vernac will produce a message for each search
result, greatly improving roundtrip time as IDEs can effectively display
the results in a streaming way.

It also allows different printers to be used.

I didn't observe a performance difference (as things seem to be
dominated by printing and `Declaremods`).

As a minor tweak, we make search with "Output Name Only" more efficient.

Motivation:
-----------

Currently, the main search API `Search.generic_search` is an effectful,
iteration-based function:

```ocaml
val generic_search : int option -> display_function -> unit
```

This type is imposed by `Declaremods`, which exposes an effectful,
iteration-based API to traverse Coq library objects.

The `Search.search_*` functions try to offer a more functional API by
returning a list of pretty printing commands. They need to build an
internal intermediate list for that purpose.

However, this is a waste of time, as the destination of these lists is
to be flushed out by the printer right away.

3 files changed, 55 insertions, 52 deletions

diff --git a/toplevel/search.ml b/toplevel/search.ml
index 921308f78..ff3c7a4f4 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -29,17 +29,6 @@ query, separated by a newline. This type of output is useful for
 editors (like emacs), to generate a list of completion candidates
 without having to parse thorugh the types of all symbols. *)
 
-let search_output_name_only = ref false
-
-let _ =
-  declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
-      optname  = "output-name-only search";
-      optkey   = ["Search";"Output";"Name";"Only"];
-      optread  = (fun () -> !search_output_name_only);
-      optwrite = (:=) search_output_name_only }
-
 type glob_search_about_item =
   | GlobSearchSubPattern of constr_pattern
   | GlobSearchString of string
@@ -118,18 +107,6 @@ let generic_search glnumopt fn =
   | Some glnum ->  iter_hypothesis glnum fn);
   iter_declarations fn
 
-(** Standard display *)
-let plain_display accu ref env c =
-  let pr = pr_global ref in
-  if !search_output_name_only then
-    accu := pr :: !accu
-  else begin
-    let pc = pr_lconstr_env env Evd.empty c in
-    accu := hov 2 (pr ++ str":" ++ spc () ++ pc) :: !accu
-  end
-
-let format_display l = prlist_with_sep fnl (fun x -> x) (List.rev l)
-
 (** Filters *)
 
 (** This function tries to see whether the conclusion matches a pattern. *)
@@ -181,8 +158,7 @@ let search_about_filter query gr env typ = match query with
 
 (** SearchPattern *)
 
-let search_pattern gopt pat mods =
-  let ans = ref [] in
+let search_pattern gopt pat mods pr_search =
   let blacklist_filter = blacklist_filter_aux () in
   let filter ref env typ =
     module_filter mods ref env typ &&
@@ -190,10 +166,9 @@ let search_pattern gopt pat mods =
     blacklist_filter ref env typ
   in
   let iter ref env typ =
-    if filter ref env typ then plain_display ans ref env typ
+    if filter ref env typ then pr_search ref env typ
   in
-  let () = generic_search gopt iter in
-  format_display !ans
+  generic_search gopt iter
 
 (** SearchRewrite *)
 
@@ -205,10 +180,9 @@ let rewrite_pat1 pat =
 let rewrite_pat2 pat =
   PApp (PRef eq, [| PMeta None; PMeta None; pat |])
 
-let search_rewrite gopt pat mods =
+let search_rewrite gopt pat mods pr_search =
   let pat1 = rewrite_pat1 pat in
   let pat2 = rewrite_pat2 pat in
-  let ans = ref [] in
   let blacklist_filter = blacklist_filter_aux () in
   let filter ref env typ =
     module_filter mods ref env typ &&
@@ -217,15 +191,13 @@ let search_rewrite gopt pat mods =
     blacklist_filter ref env typ
   in
   let iter ref env typ =
-    if filter ref env typ then plain_display ans ref env typ
+    if filter ref env typ then pr_search ref env typ
   in
-  let () = generic_search gopt iter in
-  format_display !ans
+  generic_search gopt iter
 
 (** Search *)
 
-let search_by_head gopt pat mods =
-  let ans = ref [] in
+let search_by_head gopt pat mods pr_search =
   let blacklist_filter = blacklist_filter_aux () in
   let filter ref env typ =
     module_filter mods ref env typ &&
@@ -233,15 +205,13 @@ let search_by_head gopt pat mods =
     blacklist_filter ref env typ
   in
   let iter ref env typ =
-    if filter ref env typ then plain_display ans ref env typ
+    if filter ref env typ then pr_search ref env typ
   in
-  let () = generic_search gopt iter in
-  format_display !ans
+  generic_search gopt iter
 
 (** SearchAbout *)
 
-let search_about gopt items mods =
-  let ans = ref [] in
+let search_about gopt items mods pr_search =
   let blacklist_filter = blacklist_filter_aux () in
   let filter ref env typ =
     let eqb b1 b2 = if b1 then b2 else not b2 in
@@ -251,10 +221,9 @@ let search_about gopt items mods =
     blacklist_filter ref env typ
   in
   let iter ref env typ =
-    if filter ref env typ then plain_display ans ref env typ
+    if filter ref env typ then pr_search ref env typ
   in
-  let () = generic_search gopt iter in
-  format_display !ans
+  generic_search gopt iter
 
 type search_constraint =
   | Name_Pattern of Str.regexp
diff --git a/toplevel/search.mli b/toplevel/search.mli
index 9f209a17e..ba3d48efc 100644
--- a/toplevel/search.mli
+++ b/toplevel/search.mli
@@ -39,11 +39,14 @@ val search_about_filter : glob_search_about_item -> filter_function
 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 -> std_ppcmds
-val search_rewrite : int option -> constr_pattern -> DirPath.t list * bool -> std_ppcmds
-val search_pattern : int option -> constr_pattern -> DirPath.t list * bool -> std_ppcmds
+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 -> std_ppcmds
+                  -> DirPath.t list * bool -> display_function -> unit
 
 type search_constraint =
   (** Whether the name satisfies a regexp (uses Ocaml Str syntax) *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index df83f7685..f69bac437 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1665,6 +1665,28 @@ let interp_search_about_item env =
 	errorlabstrm "interp_search_about_item"
           (str "Unable to interp \"" ++ str s ++ str "\" either as a reference or as an identifier component")
 
+(* 05f22a5d6d5b8e3e80f1a37321708ce401834430 introduced the
+   `search_output_name_only` option to avoid excessive printing when
+   searching.
+
+   The motivation was to make search usable for IDE completion,
+   however, it is still too slow due to the non-indexed nature of the
+   underlying search mechanism.
+
+   In the future we should deprecate the option and provide a fast,
+   indexed name-searching interface.
+*)
+let search_output_name_only = ref false
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "output-name-only search";
+      optkey   = ["Search";"Output";"Name";"Only"];
+      optread  = (fun () -> !search_output_name_only);
+      optwrite = (:=) search_output_name_only }
+
 let vernac_search s gopt r =
   let r = interp_search_restriction r in
   let env,gopt =
@@ -1676,16 +1698,25 @@ let vernac_search s gopt r =
     | Some g -> snd (Pfedit.get_goal_context g) , Some g
   in
   let get_pattern c = snd (intern_constr_pattern env c) in
-  let open Feedback in
+  let pr_search ref env c =
+    let pr = pr_global ref in
+    let pp = if !search_output_name_only
+      then pr
+      else begin
+        let pc = pr_lconstr_env env Evd.empty c in
+        hov 2 (pr ++ str":" ++ spc () ++ pc)
+      end
+    in Feedback.msg_notice pp
+  in
   match s with
   | SearchPattern c ->
-      msg_notice (Search.search_pattern gopt (get_pattern c) r)
+      Search.search_pattern gopt (get_pattern c) r pr_search
   | SearchRewrite c ->
-      msg_notice (Search.search_rewrite gopt (get_pattern c) r)
+      Search.search_rewrite gopt (get_pattern c) r pr_search
   | SearchHead c ->
-      msg_notice (Search.search_by_head gopt (get_pattern c) r)
+      Search.search_by_head gopt (get_pattern c) r pr_search
   | SearchAbout sl ->
-     msg_notice (Search.search_about gopt (List.map (on_snd (interp_search_about_item env)) sl) r)
+      Search.search_about gopt (List.map (on_snd (interp_search_about_item env)) sl) r pr_search
 
 let vernac_locate = let open Feedback in function
   | LocateAny (AN qid)  -> msg_notice (print_located_qualid qid)