From 2f5f00ed4fd01adc3f8b5d5bfbb5e648252e28b7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 13 Jan 2020 16:42:49 -0800 Subject: [PATCH] feat: improve `leadingIdentAsSymbol` trick --- src/Init/Lean/Parser/Parser.lean | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean index 05cb57ec48..6edf588e9f 100644 --- a/src/Init/Lean/Parser/Parser.lean +++ b/src/Init/Lean/Parser/Parser.lean @@ -1239,11 +1239,10 @@ instance ParsingTables.inhabited : Inhabited ParsingTables := ⟨{}⟩ The field `leadingIdentAsSymbol` specifies how the parsing table lookup function behaves for identifiers. The function `prattParser` uses two tables `leadingTable` and `trailingTable`. They map tokens to parsers. If `leadingIdentAsSymbol == false` and the leading token is an identifier, then `prattParser` - just executes the parsers associated with the token "ident". + just executes the parsers associated with the auxiliary token "ident". If `leadingIdentAsSymbol == true` and the leading token is an identifier ``, then `prattParser` - first checks whether the `leadingTable` has parsers associated with `` or not. If there are parsers, - then they are executed. Otherwise, we search for the token "ident". - We use this feature and the `nonReservedSymbol` parser to implement the `tactic` parsers. + combines the parsers associated with the token `` with the parsers associated with the auxiliary token "ident". + We use this feature and a variant of the `nonReservedSymbol` parser to implement the `tactic` parsers. We use this approach to avoid creating a reserved symbol for each builtin tactic (e.g., `apply`, `assumption`, etc.). That is, users may still use these symbols as identifiers (e.g., naming a function). -/ @@ -1280,7 +1279,9 @@ match stx with | some (Syntax.ident _ _ val _) => if leadingIdentAsSymbol then match map.find val with - | some as => (s, as) + | some as => match map.find `ident with + | some as' => (s, as ++ as') + | _ => (s, as) | none => find `ident else find `ident