diff options
| author | Théo Zimmermann | 2020-05-11 17:41:58 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-15 18:57:28 +0200 |
| commit | de91dd47e1e4f2366eb4f4cc174aadf8fc2ce1ce (patch) | |
| tree | 96c801975fca3c4f8e9ed93d620332fcae5038be /doc/tools/docgram/orderedGrammar | |
| parent | eae7b25e06b75f1c890215d4e6176292f10f854a (diff) | |
Document new Search features.
Diffstat (limited to 'doc/tools/docgram/orderedGrammar')
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 28 |
1 files changed, 25 insertions, 3 deletions
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 3c85b65bca..3a327fc748 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -940,7 +940,7 @@ command: [ | "SearchHead" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) | "SearchPattern" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) | "SearchRewrite" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) -| "Search" LIST1 ( OPT "-" search_item ) OPT ( [ "inside" | "outside" ] LIST1 qualid ) +| "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid ) | "Time" sentence | "Redirect" string sentence | "Timeout" num sentence @@ -996,9 +996,31 @@ comment: [ | num ] +search_query: [ +| search_item +| "-" search_query +| "[" LIST1 ( LIST1 search_query ) SEP "|" "]" +] + search_item: [ -| one_term -| string OPT ( "%" scope_key ) +| OPT ( [ "head" | "hyp" | "concl" | "headhyp" | "headconcl" ] ":" ) string OPT ( "%" scope_key ) +| OPT ( [ "head" | "hyp" | "concl" | "headhyp" | "headconcl" ] ":" ) one_term +| "is" ":" logical_kind +] + +logical_kind: [ +| thm_token +| assumption_token +| "Context" +| "Definition" +| "Example" +| "Coercion" +| "Instance" +| "Scheme" +| "Canonical" +| "Field" +| "Method" +| "Primitive" ] univ_name_list: [ |