1f4dea8582
Refactors app delaborator, merging in the projection delaborator, to support pretty printing with generalized field notation. Renames option `pp.structureProjections` to `pp.fieldNotation` and adds sub-option `pp.fieldNotation.generalized` to enable/disable generalized field notation. Adds `@[pp_nodot]` attribute to permanently disable using field notation for a given declaration. For now, the default value of `pp.fieldNotation.generalized` is false since we need a stage0 update to add `@[pp_nodot]` to some core definitions (such as `List.toArray`) before updating the tests. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60pp.2EgeneralizedFieldNotation.60/near/425856054)
35 lines
1.1 KiB
Text
35 lines
1.1 KiB
Text
/-
|
|
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Kyle Miller
|
|
-/
|
|
prelude
|
|
import Lean.Attributes
|
|
|
|
/-!
|
|
# Attributes for the pretty printer
|
|
|
|
This module defines attributes that influence pretty printer output.
|
|
-/
|
|
|
|
namespace Lean
|
|
|
|
builtin_initialize ppUsingAnonymousConstructorAttr : TagAttribute ←
|
|
registerTagAttribute `pp_using_anonymous_constructor "mark structure to be pretty printed using `⟨a,b,c⟩` notation"
|
|
|
|
builtin_initialize ppNoDotAttr : TagAttribute ←
|
|
registerTagAttribute `pp_nodot "mark declaration to never be pretty printed using field notation"
|
|
|
|
/--
|
|
Returns whether or not the given declaration has the `@[pp_using_anonymous_constructor]` attribute.
|
|
-/
|
|
def hasPPUsingAnonymousConstructorAttribute (env : Environment) (declName : Name) : Bool :=
|
|
ppUsingAnonymousConstructorAttr.hasTag env declName
|
|
|
|
/--
|
|
Returns whether or not the given declaration has the `@[pp_nodot]` attribute.
|
|
-/
|
|
def hasPPNoDotAttribute (env : Environment) (declName : Name) : Bool :=
|
|
ppNoDotAttr.hasTag env declName
|
|
|
|
end Lean
|