From 8d616e060be8350959ca85990de272cfc4b58a28 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Thu, 15 Jul 2021 00:39:28 -0700 Subject: [PATCH] doc: fix categoryParenthesizer documentation --- src/Lean/PrettyPrinter/Parenthesizer.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index b7de8dd704..8a5073a0ee 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -137,7 +137,7 @@ unsafe def mkCategoryParenthesizerAttribute : IO (KeyedDeclsAttribute CategoryPa name := `categoryParenthesizer, descr := "Register a parenthesizer for a syntax category. - [parenthesizer cat] registers a declaration of type `Lean.PrettyPrinter.CategoryParenthesizer` for the category `cat`, + [categoryParenthesizer cat] registers a declaration of type `Lean.PrettyPrinter.CategoryParenthesizer` for the category `cat`, which is used when parenthesizing calls of `categoryParser cat prec`. Implementations should call `maybeParenthesize` with the precedence and `cat`. If no category parenthesizer is registered, the category will never be parenthesized, but still be traversed for parenthesizing nested categories.", @@ -146,7 +146,7 @@ unsafe def mkCategoryParenthesizerAttribute : IO (KeyedDeclsAttribute CategoryPa let env ← getEnv let id ← Attribute.Builtin.getId stx if Parser.isParserCategory env id then pure id - else throwError "invalid [parenthesizer] argument, unknown parser category '{toString id}'" + else throwError "invalid [categoryParenthesizer] argument, unknown parser category '{toString id}'" } `Lean.PrettyPrinter.categoryParenthesizerAttribute @[builtinInit mkCategoryParenthesizerAttribute] constant categoryParenthesizerAttribute : KeyedDeclsAttribute CategoryParenthesizer