From 583afaab1033737f61a279c73e2dfb02208ebb1b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 31 Mar 2021 14:28:35 -0700 Subject: [PATCH] chore: indent syntax --- src/Lean/Elab/DeclModifiers.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 =>