Instances For
- information: Lean.MessageSeverity
- warning: Lean.MessageSeverity
- error: Lean.MessageSeverity
Instances For
- env : Lean.Environment
- mctx : Lean.MetavarContext
- lctx : Lean.LocalContext
- opts : Lean.Options
Instances For
- currNamespace : Lake.Name
- openDecls : List Lean.OpenDecl
A naming context is the information needed to shorten names in pretty printing.
It gives the current namespace and the list of open declarations.
Instances For
Pretty-prints text using surrounding context, if any.
- hasSyntheticSorry : Lean.MetavarContext → Bool
Searches for synthetic sorries in original input. Used to filter out certain messages.
Lazily formatted text to be used in MessageData
.
Instances For
- ofFormat: Lean.Format → Lean.MessageData
Eagerly formatted text. We inspect this in various hacks, so it is not immediately subsumed by
ofPPFormat
. - ofPPFormat: Lean.PPFormat → Lean.MessageData
Lazily formatted text.
- ofGoal: Lean.MVarId → Lean.MessageData
- withContext: Lean.MessageDataContext → Lean.MessageData → Lean.MessageData
withContext ctx d
specifies the pretty printing context(env, mctx, lctx, opts)
for the nested expressions ind
. - withNamingContext: Lean.NamingContext → Lean.MessageData → Lean.MessageData
- nest: Nat → Lean.MessageData → Lean.MessageData
Lifted
Format.nest
- group: Lean.MessageData → Lean.MessageData
Lifted
Format.group
- compose: Lean.MessageData → Lean.MessageData → Lean.MessageData
Lifted
Format.compose
- tagged: Lake.Name → Lean.MessageData → Lean.MessageData
Tagged sections.
Name
should be viewed as a "kind", and is used byMessageData
inspector functions. Example: an inspector that tries to find "definitional equality failures" may look for the tag "DefEqFailure". - trace: Lake.Name → Lean.MessageData → Array Lean.MessageData → optParam Bool false → Lean.MessageData
Structured message data. We use it for reporting errors, trace messages, etc.
Instances For
Determines whether the message contains any content.
Equations
- Lean.MessageData.isEmpty (Lean.MessageData.ofFormat f) = Std.Format.isEmpty f
- Lean.MessageData.isEmpty (Lean.MessageData.withContext a m) = Lean.MessageData.isEmpty m
- Lean.MessageData.isEmpty (Lean.MessageData.withNamingContext a m) = Lean.MessageData.isEmpty m
- Lean.MessageData.isEmpty (Lean.MessageData.nest a m) = Lean.MessageData.isEmpty m
- Lean.MessageData.isEmpty (Lean.MessageData.group m) = Lean.MessageData.isEmpty m
- Lean.MessageData.isEmpty (Lean.MessageData.compose m₁ m₂) = (Lean.MessageData.isEmpty m₁ && Lean.MessageData.isEmpty m₂)
- Lean.MessageData.isEmpty (Lean.MessageData.tagged a m) = Lean.MessageData.isEmpty m
- Lean.MessageData.isEmpty x = false
Instances For
Returns true when the message contains a MessageData.tagged tag ..
constructor where p tag
is true.
Instances For
Wrap the given message in l
and r
. See also Format.bracket
.
Instances For
Wrap the given message in parentheses ()
.
Instances For
Wrap the given message in square brackets []
.
Instances For
Append the given list of messages with the given separarator.
Equations
- Lean.MessageData.joinSep [] x = Lean.MessageData.ofFormat Lean.Format.nil
- Lean.MessageData.joinSep [a] x = a
- Lean.MessageData.joinSep (a :: as) x = a ++ x ++ Lean.MessageData.joinSep as x
Instances For
Write the given list of messages as a list, separating each item with ,\n
and surrounding with square brackets.
Instances For
See MessageData.ofList
.
Instances For
- fileName : String
- pos : Lean.Position
- endPos : Option Lean.Position
- keepFullRange : Bool
If
true
, report range as given; seemsgToInteractiveDiagnostic
. - severity : Lean.MessageSeverity
- data : Lean.MessageData
The content of the message.
A Message
is a richly formatted piece of information emitted by Lean.
They are rendered by client editors in the infoview and in diagnostic windows.
Instances For
Instances For
Instances For
Instances For
Instances For
- addMessageContext : Lean.MessageData → m Lean.MessageData