
  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 |   ','