error: align error text

aya-prover · Dec 11, 2022 · be5b7a9 · be5b7a9
1 parent a2ef13f
commit be5b7a9
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 9 deletions.
diff --git a/base/src/test/resources/failure/syntax/issue164.aya.txt b/base/src/test/resources/failure/syntax/issue164.aya.txt
@@ -6,7 +6,7 @@ In file $FILE:3:26 ->
                                 ^^
 
 Error: Parser error: Cannot parse
-
+
 In file $FILE:8:29 ->
 
   6 | def uncurry3 (A : Type) (B : Type) (C : Type) (D : Type)
@@ -15,7 +15,7 @@ In file $FILE:8:29 ->
                                    ^^
 
 Error: Parser error: Cannot parse
-
+
 In file $FILE:1:0 ->
 
   1 | def uncurry (A : Type) (B : Type) (C : Type)
@@ -27,19 +27,19 @@ In file $FILE:1:0 ->
   5 | 
 
 Error: Unsolved meta _
-
+
 In file $FILE:6:0 ->
 
   4 |   => f (p.1) (p.2)
   5 | 
   6 | def uncurry3 (A : Type) (B : Type) (C : Type) (D : Type)
       ^-------------------------------------------------------^ Begin of the 
-  error
+                                                                error
   7 |               (f : Pi A B C -> D)
   8 |               (p : Sig A B  C) : D
       ^---------------------------------^ End of the error
 
 Error: Unsolved meta _
-
-4 error(s), 0 warning(s).
-What are you doing?
+
+4 error(s), 0 warning(s).
+What are you doing?
diff --git a/pretty/src/main/java/org/aya/pretty/error/PrettyError.java b/pretty/src/main/java/org/aya/pretty/error/PrettyError.java
@@ -91,10 +91,10 @@ public record PrettyError(
         } else {
           if (lineNo == primaryRange.startLine()) {
             var hintUnderline = renderHint(primaryRange.startCol(), line.length(), linenoWidth);
-            docs.append(Doc.cat(hintUnderline, Doc.ONE_WS, Doc.english("Begin of the error")));
+            docs.append(Doc.stickySep(hintUnderline, Doc.align(Doc.english("Begin of the error"))));
           } else if (lineNo == primaryRange.endLine()) {
             var hintUnderline = renderHint(primaryRange.startCol(), line.length(), linenoWidth);
-            docs.append(Doc.cat(hintUnderline, Doc.ONE_WS, Doc.english("End of the error")));
+            docs.append(Doc.stickySep(hintUnderline, Doc.align(Doc.english("End of the error"))));
           }
         }
       }