diff options
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 8 | ||||
| -rw-r--r-- | toplevel/search.ml | 27 |
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) |