From 80a92cceebe20e4b520a35c1180ff21852604b2e Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 6 Apr 2022 16:55:57 +0200
Subject: [PATCH] fix: avoid choice nodes with `LeadingIdentBehavior.both`

---
 src/Lean/Parser/Basic.lean | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 41d4dc3360..968ad0a904 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -1620,9 +1620,13 @@ def indexed {α : Type} (map : TokenMap α) (c : ParserContext) (s : ParserState
       | none    => find identKind
     | LeadingIdentBehavior.both =>
       match map.find? val with
-      | some as => match map.find? identKind with
-        | some as' => (s, as ++ as')
-        | _        => (s, as)
+      | some as =>
+        if val == identKind then
+          (s, as)  -- avoid running the same parsers twice
+        else
+          match map.find? identKind with
+          | some as' => (s, as ++ as')
+          | _        => (s, as)
       | none    => find identKind
   | Except.ok (Syntax.node _ k _)      => find k
   | Except.ok _                        => (s, [])