1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83
|
-- This is taken from README.Text.Tabular
{-# OPTIONS --guardedness #-}
module Main where
open import Function.Base
open import Data.List.Base
open import Data.String.Base
open import Data.Vec.Base
open import IO.Base
open import IO.Finite
open import Text.Tabular.Base
import Text.Tabular.List as Tabularˡ
import Text.Tabular.Vec as Tabularᵛ
main : Main
main = run $ do
putStrLn $
unlines (Tabularᵛ.display unicode
(Right ∷ Left ∷ Center ∷ [])
( ("foo" ∷ "bar" ∷ "baz" ∷ [])
∷ ("1" ∷ "2" ∷ "3" ∷ [])
∷ ("6" ∷ "5" ∷ "4" ∷ [])
∷ []))
let foobar = ("foo" ∷ "bar" ∷ [])
∷ ("1" ∷ "2" ∷ [])
∷ ("4" ∷ "3" ∷ [])
∷ []
putStrLn $
unlines (Tabularᵛ.display unicode
(Right ∷ Left ∷ [])
foobar)
putStrLn $
unlines (Tabularᵛ.display ascii
(Right ∷ Left ∷ [])
foobar)
putStrLn $
unlines (Tabularᵛ.display whitespace
(Right ∷ Left ∷ [])
foobar)
putStrLn $
unlines (Tabularᵛ.display (compact unicode)
(Right ∷ Left ∷ [])
foobar)
putStrLn $
unlines (Tabularᵛ.display (noBorder unicode)
(Right ∷ Left ∷ [])
foobar)
putStrLn $
unlines (Tabularᵛ.display (addSpace unicode)
(Right ∷ Left ∷ [])
foobar)
putStrLn $
unlines (Tabularᵛ.display (compact (addSpace unicode))
(Right ∷ Left ∷ [])
foobar)
putStrLn $
unlines (Tabularˡ.display unicode
(Center ∷ Right ∷ [])
( ("foo" ∷ "bar" ∷ [])
∷ ("partial" ∷ "rows" ∷ "are" ∷ "ok" ∷ [])
∷ ("3" ∷ "2" ∷ "1" ∷ "..." ∷ "surprise!" ∷ [])
∷ []))
putStrLn $
unlines (unsafeDisplay (compact unicode)
( ("foo" ∷ "bar" ∷ [])
∷ (" 1" ∷ " 2" ∷ [])
∷ (" 4" ∷ " 3" ∷ [])
∷ []))
|