SearchAbout: who has never been annoyed by the [ ] syntax ?

 Well, hopefully, that belongs to the past: you should now be able
 to do the very same queries as before, without typing the [ ].
 For instance: SearchAbout plus mult.

 This removal of [ ] is optional, the old syntax is still legal:
  - for compatibility reasons
  - for square bracket lovers
  - for those that have "inside" or "outside" as legal identifier
    in their development and want to search about them.

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

4 files changed, 97 insertions, 26 deletions

diff --git a/CHANGES b/CHANGES
index 2d3ac5426..f749f1f1b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -6,6 +6,9 @@ Changes from V8.3 to V8.4
   the universe graph is printed in the DOT language, and can be
   processed by Graphviz tools.
 
+Vernacular commands
+
+- In SearchAbout, the [ ] delimiters are now optional.
 
 Changes from V8.2 to V8.3
 =========================
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 2a0b8051c..ab8e1531f 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -225,8 +225,7 @@ 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 SearchAbout \nelist{\zeroone{-}{\termpatternorstr}}{}.}\\
 
 \noindent where {\termpatternorstr} is a
 {\termpattern} or a {\str}, or a {\str} followed by a scope
@@ -241,25 +240,24 @@ search excludes the objects that mention that {\termpattern} or that
 {\str}.
 
 \item
-\begin{tabular}[t]{@{}l}
-  {\tt SearchAbout {\termpatternorstr} inside {\module$_1$} \ldots{} {\module$_n$}.} \\
-  {\tt SearchAbout [ \nelist{{\termpatternorstr}}{} ]
+  {\tt SearchAbout \nelist{{\termpatternorstr}}{}
     inside {\module$_1$} \ldots{} {\module$_n$}.}
-\end{tabular}
 
 This restricts the search to constructions defined in modules
 {\module$_1$} \ldots{} {\module$_n$}.
 
 \item
-\begin{tabular}[t]{@{}l}
-  {\tt SearchAbout {\termpatternorstr} outside {\module$_1$}...{\module$_n$}.} \\
-  {\tt SearchAbout [ \nelist{{\termpatternorstr}}{} ]
+  {\tt SearchAbout \nelist{{\termpatternorstr}}{}
      outside {\module$_1$}...{\module$_n$}.}
-\end{tabular}
 
 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
@@ -268,8 +266,8 @@ This restricts the search to constructions not defined in modules
 Require Import ZArith.
 \end{coq_example*}
 \begin{coq_example}
-SearchAbout [ Zmult Zplus "distr" ].
-SearchAbout [ "+"%Z "*"%Z "distr" -positive -Prop].
+SearchAbout Zmult Zplus "distr".
+SearchAbout "+"%Z "*"%Z "distr" -positive -Prop.
 SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas.
 \end{coq_example}
 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f42375a69..cc03acf55 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -676,18 +676,11 @@ GEXTEND Gram
 	  VernacSearch (SearchPattern c, l)
       | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules ->
 	  VernacSearch (SearchRewrite c, l)
-      | IDENT "SearchAbout";
-	  sl = [ "[";
-	         l = LIST1 [
-		   b = positive_search_mark; s = ne_string; sc = OPT scope
-		   -> b, SearchString (s,sc)
-		 | b = positive_search_mark; p = constr_pattern
-		   -> b, SearchSubPattern p
-		 ]; "]" -> l
-   	       | p = constr_pattern -> [true,SearchSubPattern p]
-   	       | s = ne_string; sc = OPT scope -> [true,SearchString (s,sc)] ];
-	  l = in_or_out_modules ->
-	  VernacSearch (SearchAbout sl, l)
+      | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries ->
+	  let (sl,m) = l in VernacSearch (SearchAbout (s::sl), m)
+      (* compatibility format of SearchAbout, with "[ ... ]" *)
+      | IDENT "SearchAbout"; "["; sl = LIST1 searchabout_query; "]";
+	  l = in_or_out_modules -> VernacSearch (SearchAbout sl, l)
 
       | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = ne_string ->
 	  VernacAddMLPath (false, dir)
@@ -795,9 +788,12 @@ GEXTEND Gram
   as_dirpath:
     [ [ d = OPT [ "as"; d = dirpath -> d ] -> d ] ]
   ;
-  in_or_out_modules:
+  ne_in_or_out_modules:
     [ [ IDENT "inside"; l = LIST1 global -> SearchInside l
-      | IDENT "outside"; l = LIST1 global -> SearchOutside l
+      | IDENT "outside"; l = LIST1 global -> SearchOutside l ] ]
+  ;
+  in_or_out_modules:
+    [ [ m = ne_in_or_out_modules -> m
       | -> SearchOutside [] ] ]
   ;
   comment:
@@ -811,6 +807,20 @@ GEXTEND Gram
   scope:
     [ [ "%"; key = IDENT -> key ] ]
   ;
+  searchabout_query:
+    [ [ b = positive_search_mark; s = ne_string; sc = OPT scope ->
+            (b, SearchString (s,sc))
+      | b = positive_search_mark; p = constr_pattern ->
+            (b, SearchSubPattern p)
+      ] ]
+  ;
+  searchabout_queries:
+    [ [ m = ne_in_or_out_modules -> ([],m)
+      | s = searchabout_query; l = searchabout_queries ->
+        let (sl,m) = l in (s::sl,m)
+      | -> ([],SearchOutside [])
+      ] ]
+  ;
 END;
 
 GEXTEND Gram
diff --git a/test-suite/success/searchabout.v b/test-suite/success/searchabout.v
new file mode 100644
index 000000000..d9ade3144
--- /dev/null
+++ b/test-suite/success/searchabout.v
@@ -0,0 +1,60 @@
+
+(** Test of the different syntaxes of SearchAbout, in particular
+    with and without the [ ... ] delimiters *)
+
+SearchAbout plus.
+SearchAbout plus mult.
+SearchAbout "plus_n".
+SearchAbout plus "plus_n".
+SearchAbout "*".
+SearchAbout "*" "+".
+
+SearchAbout plus inside Peano.
+SearchAbout plus mult inside Peano.
+SearchAbout "plus_n" inside Peano.
+SearchAbout plus "plus_n" inside Peano.
+SearchAbout "*" inside Peano.
+SearchAbout "*" "+" inside Peano.
+
+SearchAbout plus outside Peano Logic.
+SearchAbout plus mult outside Peano Logic.
+SearchAbout "plus_n" outside Peano Logic.
+SearchAbout plus "plus_n" outside Peano Logic.
+SearchAbout "*" outside Peano Logic.
+SearchAbout "*" "+" outside Peano Logic.
+
+SearchAbout -"*" "+" outside Logic.
+SearchAbout -"*"%nat "+"%nat outside Logic.
+
+SearchAbout [plus].
+SearchAbout [plus mult].
+SearchAbout ["plus_n"].
+SearchAbout [plus "plus_n"].
+SearchAbout ["*"].
+SearchAbout ["*" "+"].
+
+SearchAbout [plus] inside Peano.
+SearchAbout [plus mult] inside Peano.
+SearchAbout ["plus_n"] inside Peano.
+SearchAbout [plus "plus_n"] inside Peano.
+SearchAbout ["*"] inside Peano.
+SearchAbout ["*" "+"] inside Peano.
+
+SearchAbout [plus] outside Peano Logic.
+SearchAbout [plus mult] outside Peano Logic.
+SearchAbout ["plus_n"] outside Peano Logic.
+SearchAbout [plus "plus_n"] outside Peano Logic.
+SearchAbout ["*"] outside Peano Logic.
+SearchAbout ["*" "+"] outside Peano Logic.
+
+SearchAbout [-"*" "+"] outside Logic.
+SearchAbout [-"*"%nat "+"%nat] outside Logic.
+
+
+(** The example in the Reference Manual *)
+
+Require Import ZArith.
+
+SearchAbout Zmult Zplus "distr".
+SearchAbout "+"%Z "*"%Z "distr" -positive -Prop.
+SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas.