diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean index a0f0ae3b94..2dbb1c0d13 100644 --- a/src/Lean/Elab/DeclModifiers.lean +++ b/src/Lean/Elab/DeclModifiers.lean @@ -76,7 +76,7 @@ def expandOptDocComment? [Monad m] [MonadError m] (optDocComment : Syntax) : m ( | none => pure none | some s => match s[1] with | Syntax.atom _ val => pure (some (val.extract 0 (val.bsize - 2))) - | _ => throwErrorAt s "unexpected doc string {s[1]}" + | _ => throwErrorAt s "unexpected doc string{indentD s[1]}" section Methods @@ -93,7 +93,7 @@ def elabModifiers (stx : Syntax) : m Modifiers := do | none => pure none | some s => match s[1] with | Syntax.atom _ val => pure (some (val.extract 0 (val.bsize - 2))) - | _ => throwErrorAt s "unexpected doc string {s[1]}" + | _ => throwErrorAt s "unexpected doc string{indentD s[1]}" let visibility ← match visibilityStx.getOptional? with | none => pure Visibility.regular | some v =>