From ac31e176368b30d725c3753869cb10f2f0ac43e7 Mon Sep 17 00:00:00 2001 From: CodingCellist Date: Mon, 14 Jun 2021 16:29:20 +0200 Subject: [PATCH] [ refactor ] Right-align padded numbers. (#1554) --- src/Idris/ModTree.idr | 2 +- tests/typedd-book/chapter04/expected | 18 +++++++++--------- tests/typedd-book/chapter08/expected | 18 +++++++++--------- tests/typedd-book/chapter10/expected | 18 +++++++++--------- tests/typedd-book/chapter11/expected | 18 +++++++++--------- tests/typedd-book/chapter12/expected | 18 +++++++++--------- 6 files changed, 46 insertions(+), 46 deletions(-) diff --git a/src/Idris/ModTree.idr b/src/Idris/ModTree.idr index cd5497d16..453fe5928 100644 --- a/src/Idris/ModTree.idr +++ b/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) diff --git a/tests/typedd-book/chapter04/expected b/tests/typedd-book/chapter04/expected index 05bf13f45..0a52f30b9 100644 --- a/tests/typedd-book/chapter04/expected +++ b/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: diff --git a/tests/typedd-book/chapter08/expected b/tests/typedd-book/chapter08/expected index 4dac46750..6c319cb35 100644 --- a/tests/typedd-book/chapter08/expected +++ b/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) diff --git a/tests/typedd-book/chapter10/expected b/tests/typedd-book/chapter10/expected index 93153e23a..baba9d38f 100644 --- a/tests/typedd-book/chapter10/expected +++ b/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) diff --git a/tests/typedd-book/chapter11/expected b/tests/typedd-book/chapter11/expected index efad139aa..d03d9cb49 100644 --- a/tests/typedd-book/chapter11/expected +++ b/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) diff --git a/tests/typedd-book/chapter12/expected b/tests/typedd-book/chapter12/expected index d79789953..dde358112 100644 --- a/tests/typedd-book/chapter12/expected +++ b/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)