Describe non-greedy repetition operators

src/notation.md

@@ -31,6 +31,18 @@ The following notations are used by the *Lexer* and *Syntax* grammar snippets:
 
 Sequences have a higher precedence than `|` alternation.
 
+r[notation.grammar.non-greedy]
+### Non-greedy repetition
+
+Repetition operators marked with "(non-greedy)" indicate that the repetition stops matching as soon as possible rather than matching as much as possible. For example:
+
+```grammar,example
+@root EXAMPLE_STRING ->
+    `"` ~`"`*? `"`
+```
+
+When presented with the input `"one" or "two"`, the EXAMPLE_STRING rule will match `"one"` instead of the entire input.
+
 r[notation.grammar.string-tables]
 ### String table productions
 

tools/mdbook-spec/src/grammar.rs

@@ -168,6 +168,9 @@ pub fn insert_summary(grammar: &Grammar, chapter: &Chapter, diag: &mut Diagnosti
         .collect();
     let mut grammar_summary = String::new();
     for category in categories {
+        if category == "example" {
+            continue;
+        }
         let mut chars = category.chars();
         let cap = chars.next().unwrap().to_uppercase().collect::<String>() + chars.as_str();
         write!(grammar_summary, "\n## {cap} summary\n\n").unwrap();