Commit 2024-09-02 13:40 bd5475a4

View on Github →

feat: parser for Stacks Project Tags (#16230) Introduce a parser for Stacks Projects Tags: it accepts 4-character sequences of digits and uppercase letter, giving meaningful errors for shorter/empty sequences. See this Zulip thread for the issues with the previous implementation of the attribute and, in particular, parsing 0BR2 as a tag.

Estimated changes

Modified Mathlib/Tactic/StacksAttribute.lean

deleted def Lean.Environment.getSortedStackProjectDeclNames

deleted def Lean.Environment.getSortedStackProjectTags

added def Lean.PrettyPrinter.Formatter.stacksTagNoAntiquot.formatter

added def Lean.PrettyPrinter.Parenthesizer.Lean.Environment.getSortedStackProjectDeclNames

added def Lean.PrettyPrinter.Parenthesizer.Lean.Environment.getSortedStackProjectTags

added def Lean.PrettyPrinter.Parenthesizer.stacksTagAntiquot.parenthesizer

added def Lean.TSyntax.getStacksTag

added def Mathlib.Stacks.stacksTag

added def Mathlib.Stacks.stacksTagFn

added def Mathlib.Stacks.stacksTagNoAntiquot

Modified test/StacksAttribute.lean

added def captureException