[ refactor ] Right-align padded numbers. (#1554)

src/Idris/ModTree.idr

@@ -185,7 +185,7 @@ buildMod loc num len mod
         errs <- if (not needsBuilding) then pure [] else
            do let pad = minus (length $ show len) (length $ show num)
               let msg : Doc IdrisAnn
-                  = pretty num <+> pretty (String.replicate pad ' ')
+                  = pretty (String.replicate pad ' ') <+> pretty num
                     <+> slash <+> pretty len <+> colon
                     <++> pretty "Building" <++> pretty mod.buildNS
                     <++> parens (pretty src)

tests/typedd-book/chapter04/expected

@@ -1,4 +1,4 @@
-1 /12: Building BSTree (BSTree.idr)
+ 1/12: Building BSTree (BSTree.idr)
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   elem is shadowing Prelude.Types.elem
@@ -8,13 +8,13 @@ You may be unintentionally shadowing the associated global definitions:
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   elem is shadowing Prelude.Types.elem
-2 /12: Building DataStore (DataStore.idr)
-3 /12: Building Direction (Direction.idr)
-4 /12: Building Generic (Generic.idr)
-5 /12: Building Picture (Picture.idr)
-6 /12: Building Shape (Shape.idr)
-7 /12: Building SumInputs (SumInputs.idr)
-8 /12: Building Tree (Tree.idr)
+ 2/12: Building DataStore (DataStore.idr)
+ 3/12: Building Direction (Direction.idr)
+ 4/12: Building Generic (Generic.idr)
+ 5/12: Building Picture (Picture.idr)
+ 6/12: Building Shape (Shape.idr)
+ 7/12: Building SumInputs (SumInputs.idr)
+ 8/12: Building Tree (Tree.idr)
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   elem is shadowing Prelude.Types.elem
@@ -24,7 +24,7 @@ You may be unintentionally shadowing the associated global definitions:
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   elem is shadowing Prelude.Types.elem
-9 /12: Building TryIndex (TryIndex.idr)
+ 9/12: Building TryIndex (TryIndex.idr)
 10/12: Building Vect (Vect.idr)
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:

tests/typedd-book/chapter08/expected

@@ -1,4 +1,4 @@
-1 /10: Building AppendVec (AppendVec.idr)
+ 1/10: Building AppendVec (AppendVec.idr)
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   elem is shadowing Data.Vect.elem, Prelude.Types.elem
@@ -8,12 +8,12 @@ You may be unintentionally shadowing the associated global definitions:
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   elem is shadowing Data.Vect.elem, Prelude.Types.elem
-2 /10: Building CheckEqDec (CheckEqDec.idr)
-3 /10: Building CheckEqMaybe (CheckEqMaybe.idr)
-4 /10: Building EqNat (EqNat.idr)
-5 /10: Building ExactLength (ExactLength.idr)
-6 /10: Building ExactLengthDec (ExactLengthDec.idr)
-7 /10: Building ReverseVec (ReverseVec.idr)
-8 /10: Building TCVects (TCVects.idr)
-9 /10: Building Void (Void.idr)
+ 2/10: Building CheckEqDec (CheckEqDec.idr)
+ 3/10: Building CheckEqMaybe (CheckEqMaybe.idr)
+ 4/10: Building EqNat (EqNat.idr)
+ 5/10: Building ExactLength (ExactLength.idr)
+ 6/10: Building ExactLengthDec (ExactLengthDec.idr)
+ 7/10: Building ReverseVec (ReverseVec.idr)
+ 8/10: Building TCVects (TCVects.idr)
+ 9/10: Building Void (Void.idr)
 10/10: Building All (All.idr)

tests/typedd-book/chapter10/expected

@@ -7,15 +7,15 @@ DLFail:3:23--3:25
  3 | describe_list_end (xs ++ [x]) = "Non-empty, initial portion = " ++ show xs
                            ^^
 
-1 /13: Building DataStore (DataStore.idr)
-2 /13: Building DescribeList (DescribeList.idr)
-3 /13: Building DescribeList2 (DescribeList2.idr)
-4 /13: Building IsSuffix (IsSuffix.idr)
-5 /13: Building MergeSort (MergeSort.idr)
-6 /13: Building MergeSortView (MergeSortView.idr)
-7 /13: Building Reverse (Reverse.idr)
-8 /13: Building ReverseSnoc (ReverseSnoc.idr)
-9 /13: Building Shape (Shape.idr)
+ 1/13: Building DataStore (DataStore.idr)
+ 2/13: Building DescribeList (DescribeList.idr)
+ 3/13: Building DescribeList2 (DescribeList2.idr)
+ 4/13: Building IsSuffix (IsSuffix.idr)
+ 5/13: Building MergeSort (MergeSort.idr)
+ 6/13: Building MergeSortView (MergeSortView.idr)
+ 7/13: Building Reverse (Reverse.idr)
+ 8/13: Building ReverseSnoc (ReverseSnoc.idr)
+ 9/13: Building Shape (Shape.idr)
 10/13: Building Shape_abs (Shape_abs.idr)
 11/13: Building SnocList (SnocList.idr)
 12/13: Building TestStore (TestStore.idr)

tests/typedd-book/chapter11/expected

@@ -1,15 +1,15 @@
-1 /12: Building Arith (Arith.idr)
-2 /12: Building ArithCmd (ArithCmd.idr)
-3 /12: Building ArithCmdDo (ArithCmdDo.idr)
-4 /12: Building ArithTotal (ArithTotal.idr)
-5 /12: Building Greet (Greet.idr)
-6 /12: Building InfIO (InfIO.idr)
-7 /12: Building InfList (InfList.idr)
+ 1/12: Building Arith (Arith.idr)
+ 2/12: Building ArithCmd (ArithCmd.idr)
+ 3/12: Building ArithCmdDo (ArithCmdDo.idr)
+ 4/12: Building ArithTotal (ArithTotal.idr)
+ 5/12: Building Greet (Greet.idr)
+ 6/12: Building InfIO (InfIO.idr)
+ 7/12: Building InfList (InfList.idr)
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   elem is shadowing Prelude.Types.elem
-8 /12: Building Label (Label.idr)
-9 /12: Building RunIO (RunIO.idr)
+ 8/12: Building Label (Label.idr)
+ 9/12: Building RunIO (RunIO.idr)
 10/12: Building Streams (Streams.idr)
 11/12: Building StreamFail (StreamFail.idr)
 12/12: Building All (All.idr)

tests/typedd-book/chapter12/expected

@@ -1,5 +1,5 @@
-1 /10: Building ArithState (ArithState.idr)
-2 /10: Building DataStore (DataStore.idr)
+ 1/10: Building ArithState (ArithState.idr)
+ 2/10: Building DataStore (DataStore.idr)
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   schema is shadowing Main.DataStore.schema
@@ -12,11 +12,11 @@ You may be unintentionally shadowing the associated global definitions:
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   schema is shadowing Main.DataStore.schema
-3 /10: Building Record (Record.idr)
-4 /10: Building State (State.idr)
-5 /10: Building StateMonad (StateMonad.idr)
-6 /10: Building Traverse (Traverse.idr)
-7 /10: Building TreeLabel (TreeLabel.idr)
-8 /10: Building TreeLabelState (TreeLabelState.idr)
-9 /10: Building TreeLabelType (TreeLabelType.idr)
+ 3/10: Building Record (Record.idr)
+ 4/10: Building State (State.idr)
+ 5/10: Building StateMonad (StateMonad.idr)
+ 6/10: Building Traverse (Traverse.idr)
+ 7/10: Building TreeLabel (TreeLabel.idr)
+ 8/10: Building TreeLabelState (TreeLabelState.idr)
+ 9/10: Building TreeLabelType (TreeLabelType.idr)
 10/10: Building All (All.idr)