search: Add an output-name-only search option

When set, search results only display symbol names, instead of
displaying full terms with types. This is useful when the list of
symbols is needed by an external program, in particular for doing
completion in IDEs.

2 files changed, 32 insertions, 3 deletions

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 739a89af4c..c444b5ae05 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -914,6 +914,14 @@ This command turns off the normal displaying.
 \subsection[\tt Unset Silent.]{\tt Unset Silent.\optindex{Silent}}
 This command turns the normal display on.
 
+\subsection[\tt Set Search Output Name Only.]{\tt Set Search Output Name Only.\optindex{Search Output Name Only}
+\label{Search-Output-Name-Only}
+\index{Search Output Name Only mode}}
+This command restricts the output of search commands to identifier names; turning it on causes invocations of {\tt Search}, {\tt SearchHead}, {\tt SearchPattern}, {\tt SearchRewrite} etc. to omit types from their output, printing only identifiers.
+
+\subsection[\tt Unset Search Output Name Only.]{\tt Unset Search Output Name Only.\optindex{Search Output Name Only}}
+This command turns type display in search results back on.
+
 \subsection[\tt Set Printing Width {\integer}.]{\tt Set Printing Width {\integer}.\optindex{Printing Width}}
 \label{SetPrintingWidth}
 This command sets which left-aligned part of the width of the screen
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 9e67eef008..9c32bddad4 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -18,10 +18,28 @@ open Printer
 open Libnames
 open Globnames
 open Nametab
+open Goptions
 
 type filter_function = global_reference -> env -> constr -> bool
 type display_function = global_reference -> env -> constr -> unit
 
+(* This option restricts the output of [SearchPattern ...],
+[SearchAbout ...], etc. to the names of the symbols matching the
+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
@@ -98,11 +116,14 @@ let generic_search glnumopt fn =
   iter_declarations fn
 
 (** Standard display *)
-
 let plain_display accu ref env c =
-  let pc = pr_lconstr_env env Evd.empty c in
   let pr = pr_global ref in
-  accu := hov 2 (pr ++ str":" ++ spc () ++ pc) :: !accu
+  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)