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
type style = ASCII | Unicode | None
type glyphs = {
top_left : string;
top_mid : string;
top_right : string;
top_h : string;
mid_left : string;
mid_mid : string;
mid_right : string;
bot_left : string;
bot_mid : string;
bot_right : string;
bot_h : string;
v : string;
}
let glyphs_of = function
| ASCII ->
{ top_left = "+"
; top_mid = "+"
; top_right = "+"
; top_h = "-"
; mid_left = "+"
; mid_mid = "+"
; mid_right = "+"
; bot_left = "+"
; bot_mid = "+"
; bot_right = "+"
; bot_h = "-"
; v = "|"
}
| Unicode ->
{ top_left = "\xe2\x94\x8c"
; top_mid = "\xe2\x94\xac"
; top_right = "\xe2\x94\x90"
; top_h = "\xe2\x94\x80"
; mid_left = "\xe2\x94\x9c"
; mid_mid = "\xe2\x94\xbc"
; mid_right = "\xe2\x94\xa4"
; bot_left = "\xe2\x94\x94"
; bot_mid = "\xe2\x94\xb4"
; bot_right = "\xe2\x94\x98"
; bot_h = "\xe2\x94\x80"
; v = "\xe2\x94\x82"
}
| None ->
{ top_left = ""
; top_mid = ""
; top_right = ""
; top_h = ""
; mid_left = ""
; mid_mid = ""
; mid_right = ""
; bot_left = ""
; bot_mid = ""
; bot_right = ""
; bot_h = ""
; v = ""
}