From 114cd3e5cd5ebff92abf5fc3bd1e8b4bd1718b18 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Mon, 1 Aug 2022 04:19:49 -0400 Subject: [PATCH] doc: add ParserCategory docs --- src/Lean/Parser/Basic.lean | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index e4b014f66a..e0ae52b477 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -1569,7 +1569,7 @@ structure PrattParsingTables where instance : Inhabited PrattParsingTables := ⟨{}⟩ /-- - The type `leadingIdentBehavior` specifies how the parsing table + The type `LeadingIdentBehavior` specifies how the parsing table lookup function behaves for identifiers. The function `prattParser` uses two tables `leadingTable` and `trailingTable`. They map tokens to parsers. @@ -1612,9 +1612,23 @@ inductive LeadingIdentBehavior where The method `termParser prec` is equivalent to the method above. -/ structure ParserCategory where + /-- The name of a declaration which will be used as the target of + go-to-definition queries and from which doc strings will be extracted. + This is usually a dummy declaration of type `Lean.Parser.Category` + created by `declare_syntax_cat`, but for builtin categories this will + be the `builtin_initialize` command containing the call to + `registerBuiltinParserAttribute`. -/ declName : Name + /-- The list of syntax nodes that can parse into this category. + This can be used to list all syntaxes in the category. -/ kinds : SyntaxNodeKindSet := {} + /-- The parsing tables, which consist of a dynamic set of parser + functions based on the syntaxes that have been declared so far. -/ tables : PrattParsingTables := {} + /-- The `LeadingIdentBehavior`, which specifies how the parsing table + lookup function behaves for the first identifier to be parsed. + This is used by the `tactic` parser to avoid creating a reserved + symbol for each builtin tactic (e.g., `apply`, `assumption`, etc.). -/ behavior : LeadingIdentBehavior deriving Inhabited