diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index a9b58721ae..efe4e83db5 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -618,7 +618,9 @@ actually rendered. Consider using this function in lazy message data to avoid un computation for messages that are not displayed. -/ private def MessageData.formatLength (ctx : PPContext) (msg : MessageData) : BaseIO Nat := do - let { env, mctx, lctx, opts, ..} := ctx + let { env, mctx, lctx, opts, currNamespace, openDecls } := ctx + -- Simulate the naming context that will be added to the actual message + let msg := MessageData.withNamingContext { currNamespace, openDecls } msg let fmt ← msg.format (some { env, mctx, lctx, opts }) return fmt.pretty.length diff --git a/tests/lean/run/inlineExpr.lean b/tests/lean/run/inlineExpr.lean index 1d335a35f0..b122968082 100644 --- a/tests/lean/run/inlineExpr.lean +++ b/tests/lean/run/inlineExpr.lean @@ -16,23 +16,48 @@ def runTest (e : Expr) : MetaM Unit := do let msg := inlineExpr e (maxInlineLength := 30) logInfo m!"Before{msg}After" -def testShort : MetaM Unit := do - runTest <| .app (.const ``shortFun []) (.const ``shortConst []) - /-- info: Before `shortFun shortConst` After -/ #guard_msgs in -#eval testShort +#eval runTest <| .app (.const ``shortFun []) (.const ``shortConst []) opaque functionWithLongName : Nat → Nat opaque constantWithLongName : Nat -def testLong : MetaM Unit := do - runTest <| .app (.const ``functionWithLongName []) (.const ``constantWithLongName []) - /-- info: Before functionWithLongName constantWithLongName After -/ #guard_msgs in -#eval testLong +#eval runTest <| .app (.const ``functionWithLongName []) (.const ``constantWithLongName []) + +/-! Ensure that length computation accounts for namespace occlusion: -/ + +namespace ExceptionallyLongNamespaceThatWillNotBePrinted +opaque Bar.Baz : Nat → Nat + +/-- +info: Before `Bar.Baz Nat.zero` After +-/ +#guard_msgs in +#eval runTest <| .app (.const ``Bar.Baz []) (.const ``Nat.zero []) + +end ExceptionallyLongNamespaceThatWillNotBePrinted + +/-! Test `trailing` variant: -/ + +def runTestTrailing (e : Expr) : MetaM Unit := do + let msg := inlineExprTrailing e (maxInlineLength := 30) + logInfo m!"Before{msg}" + + +/-- info: Before `shortFun shortConst` -/ +#guard_msgs in +#eval runTestTrailing <| .app (.const ``shortFun []) (.const ``shortConst []) + +/-- +info: Before + functionWithLongName constantWithLongName +-/ +#guard_msgs in +#eval runTestTrailing <| .app (.const ``functionWithLongName []) (.const ``constantWithLongName [])