Fix #2495 (#2496)

- Closes #2495

src/Juvix/Compiler/Concrete/Translation/FromSource.hs

@@ -182,7 +182,7 @@ topModuleDef ::
   (Members '[Error ParserError, Files, PathResolver, InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) =>
   ParsecS r (Module 'Parsed 'ModuleTop)
 topModuleDef = do
-  optional_ stashJudoc
+  space >> optional_ stashJudoc
   optional_ stashPragmas
   m <- top moduleDef
   P.lift (checkPath (m ^. modulePath))

src/Juvix/Prelude/Pretty.hs

@@ -127,6 +127,7 @@ toPlainTextTrim :: (HasTextBackend a) => a -> Text
 toPlainTextTrim =
   Text.unlines
     . map Text.stripEnd
+    . dropWhileEnd Text.null
     . dropWhile Text.null
     . Text.lines
     . toPlainText

tests/negative/230/Foo.juvix

@@ -1,4 +1,3 @@
 module Foo;
 
 import Foo.Data.Bool open;
-

tests/negative/258/M.juvix

@@ -6,4 +6,3 @@ type Nat :=
 
 fun : Nat -> Nat
   | (S {S {x}}) := x;
-

tests/negative/265/M.juvix

@@ -10,4 +10,3 @@ type Pair (A : Type) (B : Type) :=
 f : _ → _
   | (mkPair false true) := true
   | true := false;
-

tests/negative/AppLeftImplicit.juvix

@@ -1,4 +1,3 @@
 module AppLeftImplicit;
 
 x : Type := {x};
-

tests/negative/ConstructorExpectedLeftApplication.juvix

@@ -2,4 +2,3 @@ module ConstructorExpectedLeftApplication;
 
 f : {A : Type} -> A -> A
   | (x y) := x;
-

tests/negative/ImplicitPatternLeftApplication.juvix

@@ -2,4 +2,3 @@ module ImplicitPatternLeftApplication;
 
 f : {A : Type} -> A -> A
   | ({x} y) := y;
-

tests/negative/Internal/IdenFunctionArgsNoExplicit.juvix

@@ -5,4 +5,3 @@ import Stdlib.Prelude open;
 f : {A : Type} → Nat := zero;
 
 main : Nat := f;
-

tests/negative/Internal/LazyBuiltin.juvix

@@ -12,4 +12,3 @@ if : {A : Type} -> Bool -> A -> A -> A
 
 f : Bool -> Bool
   | x := if x;
-

tests/negative/Internal/PatternConstructor.juvix

@@ -6,4 +6,3 @@ type B := b : B;
 
 f : A → B
   | b := b;
-

tests/negative/Internal/Positivity/E1.juvix

@@ -3,4 +3,3 @@ module E1;
 axiom B : Type;
 
 type X := c : (X -> B) -> X;
-

tests/negative/Internal/Positivity/E10.juvix

@@ -5,4 +5,3 @@ type T0 (A : Type) := t : (A -> T0 A) -> T0 A;
 alias : Type -> Type := T0;
 
 type T1 := c : alias T1 -> T1;
-

tests/negative/Internal/Positivity/E11.juvix

@@ -6,4 +6,3 @@ alias : Type -> Type -> Type
   | A B := A -> B;
 
 type T1 := c : alias T1 T1 -> _;
-

tests/negative/Internal/Positivity/E2.juvix

@@ -3,4 +3,3 @@ module E2;
 import NegParam open;
 
 type D := d : T D -> D;
-

tests/negative/Internal/Positivity/E3.juvix

@@ -3,4 +3,3 @@ module E3;
 axiom B : Type;
 
 type X := c : B -> (X -> B) -> X;
-

tests/negative/Internal/Positivity/E4.juvix

@@ -5,4 +5,3 @@ type Tree (A : Type) :=
   | node : (A -> Tree A) -> Tree A;
 
 type Bad := bad : Tree Bad -> Bad;
-

tests/negative/Internal/Positivity/E5.juvix

@@ -7,4 +7,3 @@ axiom B : Type;
 type T1 (A : Type) := c1 : (B -> T0 A) -> T1 A;
 
 type T2 := c2 : (B -> B -> T1 T2) -> T2;
-

tests/negative/Internal/Positivity/E6.juvix

@@ -3,4 +3,3 @@ module E6;
 axiom A : Type;
 
 type T (A : Type) := c : (A -> A -> T A -> A) -> T A;
-

tests/negative/Internal/Positivity/E7.juvix

@@ -3,4 +3,3 @@ module E7;
 type T0 (A : Type) (B : Type) := c0 : (B -> A) -> T0 A B;
 
 type T1 (A : Type) := c1 : (A -> T0 A (T1 A)) -> T1 A;
-

tests/negative/Internal/Positivity/E9.juvix

@@ -3,4 +3,3 @@ module E9;
 type B := b : B;
 
 type T := c : ((B → T) -> T) -> T;
-

tests/negative/Internal/UnsolvedMeta.juvix

@@ -3,4 +3,3 @@ module UnsolvedMeta;
 type Proxy (A : Type) := x : Proxy A;
 
 t : Proxy _ := x;
-

tests/negative/Internal/WrongReturnType.juvix

@@ -3,4 +3,3 @@ module WrongReturnType;
 axiom B : Type;
 
 type A := c : B;
-

tests/negative/Internal/WrongReturnTypeParameters.juvix

@@ -1,4 +1,3 @@
 module WrongReturnTypeParameters;
 
 type A (B : Type) := c : A B B;
-

tests/negative/Internal/WrongReturnTypeTooFewArguments.juvix

@@ -1,4 +1,3 @@
 module WrongReturnTypeTooFewArguments;
 
 type A (B : Type) := c : A;
-

tests/negative/Internal/WrongReturnTypeTooManyArguments.juvix

@@ -1,4 +1,3 @@
 module WrongReturnTypeTooManyArguments;
 
 type A (B : Type) := c : A B B;
-

tests/negative/StdlibConflict/Stdlib/Data/Bool.juvix

@@ -1,2 +1 @@
 module Stdlib.Data.Bool;
-

tests/negative/Termination/Data/Tree.juvix

@@ -11,4 +11,3 @@ f : (A : Type) → Tree A → Tree A → Tree A
 g : (A : Type) → Tree A → Tree A → Tree A
   | A x leaf := x
   | A x (branch y z) := g A z (g A x y);
-

tests/negative/Termination/Mutual.juvix

@@ -8,4 +8,3 @@ f : A -> A -> A
 
 g : A -> A -> A
   | x y := f x x;
-

tests/negative/Termination/TerminatingF.juvix

@@ -9,4 +9,3 @@ f : A -> A -> A
 
 g : A -> A -> A
   | x y := f x x;
-

tests/negative/Termination/TerminatingG.juvix

@@ -9,4 +9,3 @@ f : A -> A -> A
 terminating
 g : A -> A -> A
   | x y := f x x;
-

tests/negative/issue1337/Braces.juvix

@@ -6,4 +6,3 @@ type Nat :=
 
 fun : Nat -> Nat
   | (S {S {x}}) := x;
-

tests/negative/issue1344/D.juvix

@@ -4,4 +4,3 @@ import Other;
 import U;
 
 u : Other.Unit := U.t;
-

tests/negative/issue1344/M.juvix

@@ -5,4 +5,3 @@ import Other;
 type Unit := t : Unit;
 
 u : Other.Unit := t;
-

tests/negative/issue1344/Other.juvix

@@ -1,4 +1,3 @@
 module Other;
 
 type Unit := t : Unit;
-

tests/negative/issue1344/U.juvix

@@ -1,4 +1,3 @@
 module U;
 
 type Unit := t : Unit;
-

tests/negative/issue1700/SelfApplication.juvix

@@ -4,4 +4,3 @@ module SelfApplication;
 import Stdlib.Prelude open;
 
 main : IO := printNatLn (λ {x := x x} id (3 + 4));
-

tests/positive/LocalModWithAxiom.juvix

@@ -1,3 +1,11 @@
+
+
+-- Hola
+
+{-- This is Judoc block comment --}
+
+-- Bonjour
+
 {-# format : false #-}
 module LocalModWithAxiom;                
 

tests/positive/LocalModWithAxiom.juvix.formatted

@@ -1,3 +1,9 @@
+-- Hola
+
+{-- This is Judoc block comment --}
+
+-- Bonjour
+
 {-# format : false #-}
 module LocalModWithAxiom;
 
@@ -18,4 +24,3 @@ module C;
   end;
 
 end;
-

tests/positive/QualifiedSymbol2/M.juvix

@@ -1,2 +1 @@
 module M;
-