terminal user interface to jujutsu. Focused on speed and clarity
finish adding border stuff
+106
-181
+43
-6
forks/nottui/lib/nottui/nottui_main.ml
+43
-6
forks/nottui/lib/nottui/nottui_main.ml
···
292
292
; v = make_uchar "|"
293
293
}
294
294
;;
295
-
295
+
296
296
let unicode =
297
297
{ tl = make_uchar "┌"
298
298
; tr = make_uchar "┐"
···
309
309
; h = make_uchar "═"
310
310
; v = make_uchar "║"
311
311
}
312
+
313
+
314
+
let unicode_bold =
315
+
{ tl = make_uchar "┏"
316
+
; tr = make_uchar "┓"
317
+
; bl = make_uchar "┗"
318
+
; br = make_uchar "┛"
319
+
; h = make_uchar "━"
320
+
; v = make_uchar "┃"
321
+
}
312
322
let unicode_rounded =
313
323
{ tl = make_uchar "╭"
314
324
; tr = make_uchar "╮"
···
317
327
; h = make_uchar "─"
318
328
; v = make_uchar "│"
319
329
}
320
-
;;
330
+
331
+
let dashed =
332
+
{ tl = make_uchar "┌"
333
+
; tr = make_uchar "┐"
334
+
; bl = make_uchar "└"
335
+
; br = make_uchar "┘"
336
+
; h = make_uchar "╌"
337
+
; v = make_uchar "╎"
338
+
}
339
+
340
+
let dashed_bold =
341
+
{ tl = make_uchar "┏"
342
+
; tr = make_uchar "┓"
343
+
; bl = make_uchar "┗"
344
+
; br = make_uchar "┛"
345
+
; h = make_uchar "╍"
346
+
; v = make_uchar "╏"
347
+
}
321
348
322
-
(** Convenience focused styles *)
323
-
let unicode_bold =
349
+
350
+
let quad_dashed =
351
+
{ tl = make_uchar "┌"
352
+
; tr = make_uchar "┐"
353
+
; bl = make_uchar "└"
354
+
; br = make_uchar "┘"
355
+
; h = make_uchar "┈"
356
+
; v = make_uchar "┊"
357
+
}
358
+
359
+
let quad_dashed_bold =
324
360
{ tl = make_uchar "┏"
325
361
; tr = make_uchar "┓"
326
362
; bl = make_uchar "┗"
327
363
; br = make_uchar "┛"
328
-
; h = make_uchar "━"
329
-
; v = make_uchar "┃"
364
+
; h = make_uchar "┉"
365
+
; v = make_uchar "┋"
330
366
}
367
+
331
368
;;
332
369
end
333
370
+58
-152
forks/nottui/lib/nottui/widgets/border_box.ml
+58
-152
forks/nottui/lib/nottui/widgets/border_box.ml
···
4
4
open Nottui_main
5
5
open Lwd_infix
6
6
7
-
(*------ Internal/Private----*)
8
-
module Internal = struct
9
-
let neutral_grav = Gravity.make ~h:`Neutral ~v:`Neutral
10
-
11
-
module W = Nottui_widgets
12
-
13
-
(** Truncate a string to a given length, adding an ellipsis if truncated. *)
14
-
let truncate_string len str =
15
-
if String.length str > len
16
-
then if len <= 3 then "" else String.sub str 0 (len - 3) ^ "..."
17
-
else str
18
-
;;
19
-
20
-
(** top border*)
21
-
let outline_top attr w label =
22
-
let chr x = I.uchar attr (Uchar.of_int x) 1 1 in
23
-
let hbar = I.uchar attr (Uchar.of_int 0x2500) w 1
24
-
and label = if label |> I.width > w - 2 then I.empty else label |> I.hpad 2 0
25
-
and a, b = chr 0x256d, chr 0x256e in
26
-
I.zcat [ label; I.hcat [ a; hbar; b ]; label ]
27
-
;;
28
-
29
-
(** bottom border*)
30
-
let outline_bot attr w label =
31
-
let chr x = I.uchar attr (Uchar.of_int x) 1 1 in
32
-
let hbar = I.uchar attr (Uchar.of_int 0x2500) w 1 in
33
-
let label =
34
-
if label |> I.width > w - 2
35
-
then I.empty
36
-
else label |> I.hpad (w - (label |> I.width |> ( + ) 1)) 0
37
-
in
38
-
let c, d = chr 0x256f, chr 0x2570 in
39
-
I.zcat [ label; I.hcat [ d; hbar; c ] ]
40
-
;;
41
-
42
-
let make_label max_width label_str =
43
-
I.strf " %s " (truncate_string (max_width - 2) label_str)
44
-
;;
45
-
46
-
(** Internal function for rendering a border box with known dimensions and padding.*)
47
-
let border_box_intern
48
-
?(border_attr = A.empty)
49
-
?(label_top = I.empty)
50
-
?(label_bottom = I.empty)
51
-
~w
52
-
~h
53
-
~pad
54
-
~pad_w
55
-
~pad_h
56
-
input
57
-
=
58
-
(*can't go below 1 internal width or things get weird*)
59
-
let h = if pad_h < 1 then Int.max h 1 else h in
60
-
let w = if pad_w < 1 then Int.max w 1 else w in
61
-
(* this is a weird quirk, but we have to be careful of runaway size expansion.
62
-
If we increase the width of the space by making the vbar longer than the input ui element it will be able to expand to fill that space.
63
-
That will then increase the vbar and increase the height etc etc untill the max height is reached*)
64
-
let vbar =
65
-
I.uchar border_attr (Uchar.of_int 0x2502) 1 (h + (pad_h * 2))
66
-
|> Ui.atom
67
-
|> Ui.resize ~h:0
68
-
in
69
-
Ui.vcat
70
-
[ outline_top border_attr w label_top |> Ui.atom |> Ui.resize ~w:0
71
-
; Ui.hcat
72
-
[ vbar
73
-
; I.void pad_w 1 |> Ui.atom
74
-
; Ui.vcat
75
-
[ I.void 1 pad_h |> Ui.atom
76
-
; input |> Ui.resize ~pad
77
-
; I.void 1 pad_h |> Ui.atom
78
-
]
79
-
; I.void pad_w 1 |> Ui.atom
80
-
; vbar
81
-
]
82
-
; outline_bot border_attr w label_bottom |> Ui.atom |> Ui.resize ~w:0
83
-
]
84
-
;;
85
-
end
86
-
87
-
open Internal
88
-
89
7
let with_border_attr
90
-
?(pad = neutral_grav)
8
+
?(pad = Gravity.make ~h:`Neutral ~v:`Neutral)
91
9
?(pad_w = 2)
92
10
?(pad_h = 1)
93
11
?label_top
···
95
13
get_border
96
14
input
97
15
=
98
-
let size = Lwd.var (0, 0) in
99
-
let layout_width = Lwd.var 0 in
100
-
let input =
101
-
let$ input = input in
102
-
(*We need this later to determine the max with*)
103
-
layout_width $= (input |> Ui.layout_width);
104
-
input
105
-
(*This lets us tell the input to be a flexible size*)
106
-
|> Ui.size_sensor (fun ~w ~h -> if Lwd.peek size <> (w, h) then Lwd.set size (w, h))
107
-
in
108
-
(*This is original width and height of the input before padding or anything *)
109
-
let$ o_w, o_h = Lwd.get size
110
-
and$ input = input
111
-
and$ border_attr = get_border in
112
-
let w, h = o_w + (pad_w * 2), o_h in
113
-
let h = h in
114
-
let bbox =
115
-
border_box_intern
116
-
~border_attr
117
-
?label_top:(label_top |> Option.map (make_label (w - 2)))
118
-
?label_bottom:(label_bottom |> Option.map (make_label (w - 2)))
119
-
(* ~label_bottom:(if has_focus then I.strf "focused" else I.strf "unfocused") *)
120
-
~w
121
-
~h
122
-
~pad
123
-
~pad_w
124
-
~pad_h
125
-
input
126
-
in
127
-
(*If we want the input to be shrinkable we make it expandable, set it's width to something small and then set a max width for the whole box*)
128
-
bbox
16
+
Lwd.map2 input get_border ~f:(fun ui attr ->
17
+
ui
18
+
|> Ui.resize ~pad
19
+
|> Ui.border ~pad_w ~pad_h ?label_top ?label_bottom ~attr)
129
20
;;
130
21
131
22
let focusable
132
23
?pad
133
-
?pad_w
134
-
?pad_h
24
+
?(pad_w = 2)
25
+
?(pad_h = 1)
135
26
?label_top
136
27
?label_bottom
137
28
?(border_attr = A.empty)
138
-
?(focus_attr = A.fg A.blue)
29
+
?(focus_attr = (A.fg A.blue))
30
+
?style
31
+
?(focus_style=Ui.Border.unicode_bold)
139
32
?(focus = Focus.make ())
140
33
?(on_key = fun _ -> `Unhandled)
141
34
input
142
35
=
143
-
let input =
144
-
input
145
-
|> Lwd.map2 (focus |> Focus.status) ~f:(fun focus ui ->
146
-
ui |> Ui.keyboard_area ~focus on_key)
147
-
in
148
-
with_border_attr
149
-
?pad
150
-
?pad_w
151
-
?pad_h
152
-
?label_top
153
-
?label_bottom
154
-
(let$ focus = Focus.status focus in
155
-
if Focus.has_focus focus then focus_attr else border_attr)
156
-
input
36
+
let focus_status = Focus.status focus in
37
+
let$ ui = input
38
+
and$ focus_status = Focus.status focus in
39
+
ui
40
+
|> Ui.keyboard_area ~focus:focus_status on_key
41
+
|> Ui.resize ?pad
42
+
|> Ui.border
43
+
~pad_w
44
+
~pad_h
45
+
?label_top
46
+
?label_bottom
47
+
~attr:border_attr
48
+
~focus_attr:(focus_attr)
49
+
?style
50
+
~focus_style
157
51
;;
158
52
159
-
let box ?pad ?pad_w ?pad_h ?label_top ?label_bottom ?(border_attr = A.empty) input =
160
-
with_border_attr
161
-
?pad
162
-
?pad_w
163
-
?pad_h
164
-
?label_top
165
-
?label_bottom
166
-
(border_attr |> Lwd.pure)
167
-
input
53
+
let box
54
+
?pad
55
+
?pad_w
56
+
?pad_h
57
+
?label_top
58
+
?label_bottom
59
+
?(border_attr = A.empty)
60
+
?focus_attr
61
+
?style
62
+
?focus_style
63
+
input
64
+
=
65
+
Lwd.map input ~f:(fun ui ->
66
+
ui
67
+
|> Ui.resize ?pad
68
+
|> Ui.border
69
+
?pad_w
70
+
?pad_h
71
+
?label_top
72
+
?label_bottom
73
+
~attr:border_attr
74
+
?focus_attr
75
+
?style
76
+
?focus_style)
168
77
;;
169
78
170
79
let static
171
-
?(pad = neutral_grav)
80
+
?(pad = Gravity.make ~h:`Neutral ~v:`Neutral)
172
81
?(pad_w = 2)
173
82
?(pad_h = 1)
174
83
?label_top
···
176
85
?(border_attr = A.empty)
177
86
ui
178
87
=
179
-
let Ui.{ w; h; _ } = Ui.layout_spec ui in
180
-
Internal.border_box_intern
181
-
~w
182
-
~h
183
-
~pad
184
-
~pad_w
185
-
~pad_h
186
-
?label_top
187
-
?label_bottom
188
-
~border_attr
189
-
ui
88
+
ui
89
+
|> Ui.resize ~pad
90
+
|> Ui.border
91
+
~pad_w
92
+
~pad_h
93
+
?label_top
94
+
?label_bottom
95
+
~attr:border_attr
190
96
;;
+5
-23
forks/nottui/lib/nottui/widgets/border_box.mli
+5
-23
forks/nottui/lib/nottui/widgets/border_box.mli
···
10
10
-> Nottui_main.ui Lwd.t
11
11
12
12
(** Creates a bordered box around the given [input] widget. This box will change colour when focused
13
-
14
-
15
13
@param pad The padding around the input widget within the border box.
16
14
@param pad_w The horizontal padding around the input widget.
17
15
@param pad_h The vertical padding around the input widget.
···
30
28
-> ?label_bottom:string
31
29
-> ?border_attr:Notty.attr
32
30
-> ?focus_attr:Notty.attr
31
+
-> ?style:Nottui_main.Ui.Border.style
32
+
-> ?focus_style:Nottui_main.Ui.Border.style
33
33
-> ?focus:Nottui_main.Focus.handle
34
34
-> ?on_key:(Nottui_main.Ui.key -> Nottui_main.Ui.may_handle)
35
35
-> Nottui_main.ui Lwd.t
···
54
54
-> ?label_top:string
55
55
-> ?label_bottom:string
56
56
-> ?border_attr:Notty.attr
57
+
-> ?focus_attr:Notty.attr
58
+
-> ?style:Nottui_main.Ui.Border.style
59
+
-> ?focus_style:Nottui_main.Ui.Border.style
57
60
-> Nottui_main.ui Lwd.t
58
61
-> Nottui_main.ui Lwd.t
59
62
60
-
(** Creates a bordered box around the given [input]. The input must have a static sive ans this doesn't adjust the s .
61
-
@param scaling
62
-
Controls how the input widget is sized within the border box. Can be:
63
-
- [`Static] - The input widget is not resized.
64
-
- [`Expand sw] - The input widget is allowed to expand to fill the available space, with a stretch width [sw].
65
-
- [`Shrinkable (min_width, sw)] - The input widget is allowed to shrink to a minimum width of [min_width], and expand with a stretch width [sw].
66
-
@param pad The padding around the input widget within the border box.
67
-
@param pad_w The horizontal padding around the input widget.
68
-
@param pad_h The vertical padding around the input widget.
69
-
@param label An optional label to display within the border box.
70
-
@param input The input widget to be bordered.
71
-
@param border_attr Style for the border, defaults to [A.empty]. *)
72
-
val static
73
-
: ?pad:Nottui_main.gravity
74
-
-> ?pad_w:int
75
-
-> ?pad_h:int
76
-
-> ?label_top:Notty.image
77
-
-> ?label_bottom:Notty.image
78
-
-> ?border_attr:Notty.attr
79
-
-> Nottui_main.ui
80
-
-> Nottui_main.ui