From 99c665774cecdec76b0f63ec5d32783726b1954d Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Mon, 15 Jul 2024 18:44:35 -0700 Subject: [PATCH] [ fix ] check indentation after = in declarations --- libs/base/System/Clock.idr | 8 ++++---- src/Idris/Parser.idr | 1 + src/Idris/Pretty.idr | 2 +- tests/idris2/error/perror033/DeclIndent.idr | 4 ++++ tests/idris2/error/perror033/expected | 11 +++++++++++ tests/idris2/error/perror033/run | 3 +++ 6 files changed, 24 insertions(+), 5 deletions(-) create mode 100644 tests/idris2/error/perror033/DeclIndent.idr create mode 100644 tests/idris2/error/perror033/expected create mode 100644 tests/idris2/error/perror033/run diff --git a/libs/base/System/Clock.idr b/libs/base/System/Clock.idr index f16057f27e..356a51587d 100644 --- a/libs/base/System/Clock.idr +++ b/libs/base/System/Clock.idr @@ -53,10 +53,10 @@ Eq (Clock type) where public export Ord (Clock type) where compare (MkClock seconds1 nanoseconds1) (MkClock seconds2 nanoseconds2) = - case compare seconds1 seconds2 of - LT => LT - GT => GT - EQ => compare nanoseconds1 nanoseconds2 + case compare seconds1 seconds2 of + LT => LT + GT => GT + EQ => compare nanoseconds1 nanoseconds2 public export Show (Clock type) where diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 0b8cfdeb2c..fd941c347a 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1231,6 +1231,7 @@ mutual = do b <- bounds $ do decoratedSymbol fname "=" mustWork $ do + continue indents rhs <- typeExpr pdef fname indents ws <- option [] $ whereBlock fname col pure (rhs, ws) diff --git a/src/Idris/Pretty.idr b/src/Idris/Pretty.idr index b324c4b656..87313d7a4a 100644 --- a/src/Idris/Pretty.idr +++ b/src/Idris/Pretty.idr @@ -313,7 +313,7 @@ mutual prettyPrec d (PDelay _ tm) = parenthesise (d > startPrec) $ "Delay" <++> prettyPrec appPrec tm prettyPrec d (PForce _ tm) = parenthesise (d > startPrec) $ "Force" <++> prettyPrec appPrec tm prettyPrec d (PAutoApp _ f a) = - parenthesise (d > startPrec) $ group $ prettyPrec leftAppPrec f <++> "@" <+> braces (pretty a) + parenthesise (d > startPrec) $ group $ prettyPrec leftAppPrec f <++> "@" <+> braces (pretty a) prettyPrec d (PNamedApp _ f n (PRef _ a)) = parenthesise (d > startPrec) $ group $ if n == rawName a diff --git a/tests/idris2/error/perror033/DeclIndent.idr b/tests/idris2/error/perror033/DeclIndent.idr new file mode 100644 index 0000000000..55bc57ffaf --- /dev/null +++ b/tests/idris2/error/perror033/DeclIndent.idr @@ -0,0 +1,4 @@ +namespace A + test : (x : Type -> Type) -> Type + test x = + x Type diff --git a/tests/idris2/error/perror033/expected b/tests/idris2/error/perror033/expected new file mode 100644 index 0000000000..fc54852e22 --- /dev/null +++ b/tests/idris2/error/perror033/expected @@ -0,0 +1,11 @@ +1/1: Building DeclIndent (DeclIndent.idr) +Error: Couldn't parse any alternatives: +1: Unexpected end of expression. + +DeclIndent:4:2--4:3 + 1 | namespace A + 2 | test : (x : Type -> Type) -> Type + 3 | test x = + 4 | x Type + ^ +... (2 others) diff --git a/tests/idris2/error/perror033/run b/tests/idris2/error/perror033/run new file mode 100644 index 0000000000..06fa6c1008 --- /dev/null +++ b/tests/idris2/error/perror033/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +check DeclIndent.idr