From 9b24b6d763bb2c7975cd2b93364d7647fd660598 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 17 Apr 2013 18:33:16 +0000 Subject: [PATCH] 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 | 3 + doc/refman/RefMan-ide.tex | 6 +- doc/refman/RefMan-oth.tex | 107 +++++++++++++++------------- doc/tutorial/Tutorial.tex | 8 +-- ide/coq_commands.ml | 3 +- ide/coqide.ml | 4 +- ide/coqide_ui.ml | 2 +- ide/wg_Find.ml | 4 +- parsing/g_vernac.ml4 | 7 +- printing/ppvernac.ml | 4 +- test-suite/output/Search.out | 36 +++++----- test-suite/output/Search.v | 6 +- test-suite/output/SearchPattern.out | 20 +++--- tools/coqdoc/output.ml | 2 +- 14 files changed, 114 insertions(+), 98 deletions(-) diff --git a/CHANGES b/CHANGES index 416f0a117b58..6b6892e1d5d2 100644 --- a/CHANGES +++ b/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 diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex index e0c6c868f722..ec640f4efaa5 100644 --- a/doc/refman/RefMan-ide.tex +++ b/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 diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 0126e686bb4c..a543561b56a5 100644 --- a/doc/refman/RefMan-oth.tex +++ b/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"}. diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex index 43c8bf620b7c..5907edb61520 100755 --- a/doc/tutorial/Tutorial.tex +++ b/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} diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index 26dbcb125b48..ae39a1249d2f 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -207,7 +207,8 @@ let state_preserving = [ "Recursive Extraction Library"; "Search"; - "SearchAbout"; + "SearchAbout (* deprecated *)"; + "SearchHead"; "SearchPattern"; "SearchRewrite"; diff --git a/ide/coqide.ml b/ide/coqide.ml index 8429a9b07a46..616358789938 100644 --- a/ide/coqide.ml +++ b/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"); diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index d88f623eff3e..8732cd83b434 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -110,7 +110,7 @@ let init () = %s - + diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml index e21cc0aa05dd..319342e919fc 100644 --- a/ide/wg_Find.ml +++ b/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 diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 56abf3e1c49a..004dbab7b4d3 100644 --- a/parsing/g_vernac.ml4 +++ b/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) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 415d703162c4..427317a45a0d 100644 --- a/printing/ppvernac.ml +++ b/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 () diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index 2a22a89b6658..120c6a4ea658 100644 --- a/test-suite/output/Search.out +++ b/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 diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v index f1489f22ae03..4ef26347337b 100644 --- a/test-suite/output/Search.v +++ b/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 *) diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out index d546f84daa8e..6595302e13f0 100644 --- a/test-suite/output/SearchPattern.out +++ b/test-suite/output/SearchPattern.out @@ -1,32 +1,32 @@ -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 -S: nat -> nat +xorb: bool -> bool -> bool +negb: bool -> bool O: nat +S: nat -> nat +length: forall A : Type, list A -> nat pred: nat -> nat plus: nat -> nat -> nat mult: nat -> nat -> nat minus: nat -> nat -> nat -min: nat -> nat -> nat max: nat -> nat -> nat -length: forall A : Type, list A -> nat +min: nat -> nat -> nat S: nat -> nat pred: nat -> nat plus: nat -> nat -> nat mult: nat -> nat -> nat minus: nat -> nat -> nat -min: nat -> nat -> nat max: nat -> nat -> nat +min: nat -> nat -> nat mult_n_Sm: forall n m : nat, n * m + n = n * S m -le_n: forall n : nat, n <= n identity_refl: forall (A : Type) (a : A), identity a a -eq_refl: forall (A : Type) (x : A), x = x iff_refl: forall A : Prop, A <-> A +eq_refl: forall (A : Type) (x : A), x = x +le_n: forall n : nat, n <= n pair: forall A B : Type, A -> B -> A * B conj: forall A B : Prop, A -> B -> A /\ B diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 61c18f9e4905..6582b8c7043e 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -41,7 +41,7 @@ let is_keyword = "Mutual"; "Parameter"; "Parameters"; "Print"; "Printing"; "All"; "Proof"; "Proof with"; "Qed"; "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Assumptions"; "Axioms"; "Universes"; "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; - "Search"; "SearchAbout"; "SearchRewrite"; + "Search"; "SearchAbout"; "SearchHead"; "SearchPattern"; "SearchRewrite"; "Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context"; "Notation"; "Reserved Notation"; "Tactic Notation"; "Delimit"; "Bind"; "Open"; "Scope"; "Inline";