-
-
Notifications
You must be signed in to change notification settings - Fork 16
Description
GitHub TUI has some elements inside a border like this one:
github-tui/lib/tui/widget/widget.ml
Lines 29 to 34 in deb91b8
| let code_tab ~is_selected = | |
| tab_doc ~is_selected | |
| [ "╭───────╮"; | |
| "│ Code¹ │"; | |
| "└───────┴"; | |
| ] [@@ocamlformat "disable"] |
Sometimes those elements are selected and I would love to have a bold border for them.
Unfortunately, the bold ANSI sequence doesn't make borders bold! I need to use different characters like ┏━┓ instead of ┌─┐.
This issue is to discuss possible options to implement this inside GitHub TUI.
Option 1: Traverse the sequence of graphemes
Recent migration to ansifmt enabled to introspect easily the current applied formatting. A simple solution would be to check if the current chunk is bold and if yes, convert to a list of graphemes and replace border characters with new ones and convert back here:
github-tui/lib/pretty/chunk.ml
Line 6 in deb91b8
| let fmt { styles; string } = Ansifmt.Styling.wrap ~contents:string styles |
It may seem costly to traverse every single chunk but since TUI is not exactly huge, maybe it'll be fine. But it's the simplest non-invasive solution.