0 | module Data.Container.Base.Display2D.CharacterMap
 1 |
 2 | public export
 3 | padCharacter : Char
 4 | padCharacter = ' '
 5 |
 6 | public export
 7 | record Tree where
 8 |   constructor MkTree
 9 |   horizontal : Char
10 |   branchMid : Char
11 |   branchLast : Char
12 |   vertical : Char
13 |   gap : Char
14 |   placeholder : Char
15 |
16 | ||| Used for drawing a box border
17 | public export
18 | record Box where
19 |   constructor MkBox
20 |   topLeft : Char
21 |   topRight : Char
22 |   bottomLeft : Char
23 |   bottomRight : Char
24 |   horizontal : Char
25 |   vertical : Char
26 |
27 | ||| Used for rendering list-like syntax
28 | public export
29 | record ListSyntax where
30 |   constructor MkListSyntax
31 |   left : Char
32 |   right : Char
33 |   separator : Char
34 |
35 | ||| Used for rendering pair-like syntax
36 | public export
37 | record PairSyntax where
38 |   constructor MkPairSyntax
39 |   left : Char
40 |   right : Char
41 |   separator : Char
42 |
43 | public export
44 | SingleLineTree : Tree
45 | SingleLineTree = MkTree
46 |   '─'
47 |   '├'
48 |   '└'
49 |   '│'
50 |   ' '
51 |   '\x00B7'
52 |
53 | ||| Double-line, to separate from tree lines
54 | public export
55 | DoubleLineBox : Box
56 | DoubleLineBox = MkBox
57 |   '╔'
58 |   '╗'
59 |   '╚'
60 |   '╝'
61 |   '═'
62 |   '║'
63 |
64 | public export
65 | AsciiListSyntax : ListSyntax
66 | AsciiListSyntax = MkListSyntax
67 |   '['
68 |   ']'
69 |   ','
70 |
71 | public export
72 | AsciiPairSyntax : PairSyntax
73 | AsciiPairSyntax = MkPairSyntax
74 |   '('
75 |   ')'
76 |   ','