(h: Highlight)
| 646 | } |
| 647 | |
| 648 | function removeNewlines(h: Highlight): void { |
| 649 | h.lines = h.lines.map(line => |
| 650 | line.flatMap(([style, text]) => |
| 651 | text |
| 652 | .split('\n') |
| 653 | .filter(p => p.length > 0) |
| 654 | .map((p): Block => [style, p]), |
| 655 | ), |
| 656 | ) |
| 657 | } |
| 658 | |
| 659 | function charWidth(ch: string): number { |
| 660 | return stringWidth(ch) |