Renaming SearchAbout into Search and Search into SearchHead.

I hope I did not forget any place to change.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16423 85f007b7-540e-0410-9357-904b9bb8a0f7

CHANGES

@@ -10,6 +10,9 @@ Vernacular commands
 - The "Open Scope" command can now be given also a delimiter (e.g. Z).
 - The "Definition" command now allows the "Local" modifier.
 - The "Let" command can now define local (co)fixpoints.
+- Command "Search" has been renamed into "SearchHead". The command
+  name "Search" now behaves like former "SearchAbout". The latter name
+  is deprecated.
 
 Specification Language
 

doc/refman/RefMan-ide.tex

@@ -147,16 +147,16 @@ \section{Queries}
 
 
 We call \emph{query} any vernacular command that do not change the
-current state, such as \verb|Check|, \verb|SearchAbout|, etc. Those
+current state, such as \verb|Check|, \verb|Search|, etc. Those
 commands are of course useless during compilation of a file, hence
 should not be included in scripts. To run such commands without
 writing them in the script, \CoqIDE{} offers another input window
 called the \emph{query window}. This window can be displayed on
 demand, either by using the \texttt{Window} menu, or directly using
 shortcuts given in the \texttt{Queries} menu. Indeed, with \CoqIDE{}
-the simplest way to perform a \texttt{SearchAbout} on some identifier
+the simplest way to perform a \texttt{Search} on some identifier
 is to select it using the mouse, and pressing \verb|F2|. This will
-both make appear the query window and run the \texttt{SearchAbout} in
+both make appear the query window and run the \texttt{Search} in
 it, displaying the result. Shortcuts \verb|F3| and \verb|F4| are for
 \verb|Check| and \verb|Print| respectively.
 Figure~\ref{fig:querywindow} displays the query window after selection

doc/refman/RefMan-oth.tex

@@ -164,37 +164,7 @@ \section{Requests to the environment}
   Displays all assumptions and constants {\qualid} relies on.
 \end{Variants}
 
-\subsection[\tt Search {\term}.]{\tt Search {\term}.\comindex{Search}}
-This command displays the name and type of all theorems of the current
-context whose statement's conclusion has the form {\tt ({\term} t1 ..
-  tn)}.  This command is useful to remind the user of the name of
-library lemmas.
-
-\begin{coq_example}
-Search le.
-Search (@eq bool).
-\end{coq_example}
-
-\begin{Variants}
-\item
-{\tt Search} {\term} {\tt inside} {\module$_1$} \ldots{} {\module$_n$}{\tt .}
-
-This restricts the search to constructions defined in modules
-{\module$_1$} \ldots{} {\module$_n$}.
-
-\item {\tt Search} {\term} {\tt outside} {\module$_1$} \ldots{} {\module$_n$}{\tt .}
-
-This restricts the search to constructions not defined in modules
-{\module$_1$} \ldots{} {\module$_n$}.
-
-\begin{ErrMsgs}
-\item \errindex{Module/section \module{} not found}
-No module \module{} has been required (see Section~\ref{Require}).
-\end{ErrMsgs}
-
-\end{Variants}
-
-\subsection[\tt SearchAbout {\qualid}.]{\tt SearchAbout {\qualid}.\comindex{SearchAbout}}
+\subsection[\tt Search {\qualid}.]{\tt Search {\qualid}.\comindex{Search}}
 This command displays the name and type of all objects (theorems,
 axioms, etc) of the current context whose statement contains \qualid.
 This command is useful to remind the user of the name of library
@@ -209,36 +179,36 @@ \section{Requests to the environment}
 \newcommand{\termpatternorstr}{{\termpattern}\textrm{\textsl{-}}{\str}}
 
 \begin{Variants}
-\item {\tt SearchAbout {\str}.}
+\item {\tt Search {\str}.}
 
 If {\str} is a valid identifier, this command displays the name and type
 of all objects (theorems, axioms, etc) of the current context whose
 name contains {\str}. If {\str} is a notation's string denoting some
 reference {\qualid} (referred to by its main symbol as in \verb="+"=
 or by its notation's string as in \verb="_ + _"= or \verb="_ 'U' _"=, see
-Section~\ref{Notation}), the command works like {\tt SearchAbout
+Section~\ref{Notation}), the command works like {\tt Search
 {\qualid}}.
 
-\item {\tt SearchAbout {\str}\%{\delimkey}.}
+\item {\tt Search {\str}\%{\delimkey}.}
 
 The string {\str} must be a notation or the main symbol of a notation
 which is then interpreted in the scope bound to the delimiting key
 {\delimkey} (see Section~\ref{scopechange}).
 
-\item {\tt SearchAbout {\termpattern}.}
+\item {\tt Search {\termpattern}.}
 
 This searches for all statements or types of definition that contains
 a subterm that matches the pattern {\termpattern} (holes of the
 pattern are either denoted by ``{\texttt \_}'' or
 by ``{\texttt ?{\ident}}'' when non linear patterns are expected).
 
-\item {\tt SearchAbout \nelist{\zeroone{-}{\termpatternorstr}}{}.}\\
+\item {\tt Search \nelist{\zeroone{-}{\termpatternorstr}}{}.}\\
 
 \noindent where {\termpatternorstr} is a
 {\termpattern} or a {\str}, or a {\str} followed by a scope
 delimiting key {\tt \%{\delimkey}}.
 
-This generalization of {\tt SearchAbout} searches for all objects
+This generalization of {\tt Search} searches for all objects
 whose statement or type contains a subterm matching {\termpattern} (or
 {\qualid} if {\str} is the notation for a reference {\qualid}) and
 whose name contains all {\str} of the request that correspond to valid
@@ -247,24 +217,19 @@ \section{Requests to the environment}
 {\str}.
 
 \item
-  {\tt SearchAbout} \nelist{{\termpatternorstr}}{}
+  {\tt Search} \nelist{{\termpatternorstr}}{}
     {\tt inside} {\module$_1$} \ldots{} {\module$_n$}{\tt .}
 
 This restricts the search to constructions defined in modules
 {\module$_1$} \ldots{} {\module$_n$}.
 
 \item
-  {\tt SearchAbout \nelist{{\termpatternorstr}}{}
+  {\tt Search \nelist{{\termpatternorstr}}{}
      outside {\module$_1$}...{\module$_n$}.}
 
 This restricts the search to constructions not defined in modules
 {\module$_1$} \ldots{} {\module$_n$}.
 
-\item {\tt SearchAbout [ ... ]. }
-
-For compatibility with older versions, the list of objects to search
-may be enclosed by optional {\tt [  ]} delimiters.
-
 \end{Variants}
 
 \examples
@@ -273,17 +238,61 @@ \section{Requests to the environment}
 Require Import ZArith.
 \end{coq_example*}
 \begin{coq_example}
-SearchAbout Z.mul Z.add "distr".
-SearchAbout "+"%Z "*"%Z "distr" -positive -Prop.
-SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas.
+Search Z.mul Z.add "distr".
+Search "+"%Z "*"%Z "distr" -positive -Prop.
+Search (?x * _ + ?x * _)%Z outside OmegaLemmas.
 \end{coq_example}
 
+\Warning \comindex{SearchAbout} Up to Coq version 8.4, {\tt Search}
+had the behavior of current {\tt SearchHead} and the behavior of
+current {\tt Search} was obtained with command {\tt SearchAbout}. For
+compatibility, the deprecated name {\tt SearchAbout} can still be used
+as a synonym of {\tt Search}. For compatibility, the list of objects to
+search when using {\tt SearchAbout} may also be enclosed by optional
+{\tt [ ]} delimiters.
+
+\subsection[\tt SearchHead {\term}.]{\tt SearchHead {\term}.\comindex{SearchHead}}
+This command displays the name and type of all theorems of the current
+context whose statement's conclusion has the form {\tt ({\term} t1 ..
+  tn)}.  This command is useful to remind the user of the name of
+library lemmas.
+
+\begin{coq_example*}
+Reset Initial.
+\end{coq_example*}
+
+\begin{coq_example}
+SearchHead le.
+SearchHead (@eq bool).
+\end{coq_example}
+
+\begin{Variants}
+\item
+{\tt SearchHead} {\term} {\tt inside} {\module$_1$} \ldots{} {\module$_n$}{\tt .}
+
+This restricts the search to constructions defined in modules
+{\module$_1$} \ldots{} {\module$_n$}.
+
+\item {\tt SearchHead} {\term} {\tt outside} {\module$_1$} \ldots{} {\module$_n$}{\tt .}
+
+This restricts the search to constructions not defined in modules
+{\module$_1$} \ldots{} {\module$_n$}.
+
+\begin{ErrMsgs}
+\item \errindex{Module/section \module{} not found}
+No module \module{} has been required (see Section~\ref{Require}).
+\end{ErrMsgs}
+
+\end{Variants}
+
+\Warning Up to Coq version 8.4, {\tt SearchHead} was named {\tt Search}.
+
 \subsection[\tt SearchPattern {\termpattern}.]{\tt SearchPattern {\term}.\comindex{SearchPattern}}
 
 This command displays the name and type of all theorems of the current
 context whose statement's conclusion or last hypothesis and conclusion
 matches the expression {\term} where holes in the latter are denoted
-by ``{\texttt \_}''. It is a variant of {\tt SearchAbout
+by ``{\texttt \_}''. It is a variant of {\tt Search
   {\termpattern}} that does not look for subterms but searches for
 statements whose conclusion has exactly the expected form, or whose
 statement finishes by the given series of hypothesis/conclusion.
@@ -344,7 +353,7 @@ \section{Requests to the environment}
 \end{Variants}
 
 \subsubsection{Nota Bene:}
-For the {\tt Search}, {\tt SearchAbout}, {\tt SearchPattern} and
+For the {\tt Search}, {\tt SearchHead}, {\tt SearchPattern} and
 {\tt SearchRewrite} queries, it is possible to globally filter
 the search results via the command
 {\tt Add Search Blacklist "substring1"}.

doc/tutorial/Tutorial.tex

@@ -1539,17 +1539,17 @@ \section{Managing the context}
 
 It is often difficult to remember the names of all lemmas and
 definitions available in the current context, especially if large
-libraries have been loaded. A convenient \verb:SearchAbout: command
+libraries have been loaded. A convenient \verb:Search: command
 is available to lookup all known facts 
 concerning a given predicate. For instance, if you want to know all the
 known lemmas about the less or equal relation, just ask:
 \begin{coq_example}
-SearchAbout le.
+Search le.
 \end{coq_example}
-Another command \verb:Search: displays only lemmas where the searched
+Another command \verb:SearchHead: displays only lemmas where the searched
 predicate appears at the head position in the conclusion.
 \begin{coq_example}
-Search le.
+SearchHead le.
 \end{coq_example}
 
 A new and more convenient search tool is \textsf{SearchPattern}

ide/coq_commands.ml

@@ -207,7 +207,8 @@ let state_preserving = [
   "Recursive Extraction Library";
 
   "Search";
-  "SearchAbout";
+  "SearchAbout (* deprecated *)";
+  "SearchHead";
   "SearchPattern";
   "SearchRewrite";
 

ide/coqide.ml

@@ -626,7 +626,7 @@ let otherquery command _ =
     Coq.try_grab sn.coqtop (sn.coqops#raw_coq_query query) ignore
 
 let query command _ =
-  if command = "SearchAbout"
+  if command = "Search" || command = "SearchAbout"
   then searchabout ()
   else otherquery command ()
 
@@ -1054,7 +1054,7 @@ let build_ui () =
   let qitem s accel = item s ~label:("_"^s) ?accel ~callback:(Query.query s) in
   menu queries_menu [
     item "Queries" ~label:"_Queries";
-    qitem "SearchAbout" (Some "F2");
+    qitem "Search" (Some "F2");
     qitem "Check" (Some "F3");
     qitem "Print" (Some "F4");
     qitem "About" (Some "F5");

ide/coqide_ui.ml

@@ -110,7 +110,7 @@ let init () =
     %s
   </menu>
   <menu action='Queries'>
-    <menuitem action='SearchAbout' />
+    <menuitem action='Search' />
     <menuitem action='Check' />
     <menuitem action='Print' />
     <menuitem action='About' />

ide/wg_Find.ml

@@ -253,10 +253,10 @@ class finder (view : GText.view) =
 class info (coqtop : Coq.coqtop) (view : GText.view) (msg_view : Wg_MessageView.message_view) =
 
   let widget = GPack.vbox () in
-  (* SearchAbout part *)
+  (* Search part *)
   let query_box = GPack.hbox ~packing:widget#add () in
   let _ =
-    GMisc.label ~text:"SearchAbout:"
+    GMisc.label ~text:"Search:"
       ~xalign:1.0
       ~packing:query_box#pack ()
   in

parsing/g_vernac.ml4

@@ -766,15 +766,18 @@ GEXTEND Gram
       | IDENT "About"; qid = smart_global -> VernacPrint (PrintAbout qid)
 
       (* Searching the environment *)
-      | IDENT "Search"; c = constr_pattern; l = in_or_out_modules ->
+      | IDENT "SearchHead"; c = constr_pattern; l = in_or_out_modules ->
 	  VernacSearch (SearchHead c, l)
       | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules ->
 	  VernacSearch (SearchPattern c, l)
       | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules ->
 	  VernacSearch (SearchRewrite c, l)
+      | IDENT "Search"; s = searchabout_query; l = searchabout_queries ->
+	  let (sl,m) = l in VernacSearch (SearchAbout (s::sl), m)
+      (* compatibility: SearchAbout *)
       | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries ->
 	  let (sl,m) = l in VernacSearch (SearchAbout (s::sl), m)
-      (* compatibility format of SearchAbout, with "[ ... ]" *)
+      (* compatibility: SearchAbout with "[ ... ]" *)
       | IDENT "SearchAbout"; "["; sl = LIST1 searchabout_query; "]";
 	  l = in_or_out_modules -> VernacSearch (SearchAbout sl, l)
 

printing/ppvernac.ml

@@ -126,10 +126,10 @@ let pr_search_about (b,c) =
   | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
 
 let pr_search a b pr_p = match a with
-  | SearchHead c -> str"Search" ++ spc() ++ pr_p c ++ pr_in_out_modules b
+  | SearchHead c -> str"SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b
   | SearchPattern c -> str"SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b
   | SearchRewrite c -> str"SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b
-  | SearchAbout sl -> str"SearchAbout" ++ spc() ++ str "[" ++ prlist_with_sep spc pr_search_about sl ++ str "]" ++ pr_in_out_modules b
+  | SearchAbout sl -> str"Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b
 
 let pr_locality_full = function
   | None -> mt ()

test-suite/output/Search.out

@@ -1,29 +1,29 @@
-le_S: forall n m : nat, n <= m -> n <= S m
 le_n: forall n : nat, n <= n
+le_S: forall n m : nat, n <= m -> n <= S m
 le_pred: forall n m : nat, n <= m -> pred n <= pred m
 le_S_n: forall n m : nat, S n <= S m -> n <= m
-false: bool
 true: bool
-xorb: bool -> bool -> bool
+false: bool
+andb: bool -> bool -> bool
 orb: bool -> bool -> bool
-negb: bool -> bool
 implb: bool -> bool -> bool
-andb: bool -> bool -> bool
-pred_Sn: forall n : nat, n = pred (S n)
-plus_n_Sm: forall n m : nat, S (n + m) = n + S m
-plus_n_O: forall n : nat, n = n + 0
-plus_Sn_m: forall n m : nat, S n + m = S (n + m)
-plus_O_n: forall n : nat, 0 + n = n
-mult_n_Sm: forall n m : nat, n * m + n = n * S m
-mult_n_O: forall n : nat, 0 = n * 0
-min_r: forall n m : nat, m <= n -> min n m = m
-min_l: forall n m : nat, n <= m -> min n m = n
-max_r: forall n m : nat, n <= m -> max n m = m
-max_l: forall n m : nat, m <= n -> max n m = n
+xorb: bool -> bool -> bool
+negb: bool -> bool
+eq_S: forall x y : nat, x = y -> S x = S y
 f_equal_pred: forall x y : nat, x = y -> pred x = pred y
+pred_Sn: forall n : nat, n = pred (S n)
+eq_add_S: forall n m : nat, S n = S m -> n = m
 f_equal2_plus:
   forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
+plus_n_O: forall n : nat, n = n + 0
+plus_O_n: forall n : nat, 0 + n = n
+plus_n_Sm: forall n m : nat, S (n + m) = n + S m
+plus_Sn_m: forall n m : nat, S n + m = S (n + m)
 f_equal2_mult:
   forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2
-eq_add_S: forall n m : nat, S n = S m -> n = m
-eq_S: forall x y : nat, x = y -> S x = S y
+mult_n_O: forall n : nat, 0 = n * 0
+mult_n_Sm: forall n m : nat, n * m + n = n * S m
+max_l: forall n m : nat, m <= n -> max n m = n
+max_r: forall n m : nat, n <= m -> max n m = m
+min_l: forall n m : nat, n <= m -> min n m = n
+min_r: forall n m : nat, m <= n -> min n m = m

test-suite/output/Search.v

@@ -1,5 +1,5 @@
 (* Some tests of the Search command *)
 
-Search le.				(* app nodes *)
-Search bool. 				(* no apps *)
-Search (@eq nat).			(* complex pattern *)
+SearchHead le.				(* app nodes *)
+SearchHead bool. 				(* no apps *)
+SearchHead (@eq nat).			(* complex pattern *)