lean-tui 1.1.0

Standalone TUI infoview for Lean 4 theorem prover
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
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143

use ratatui::{
    buffer::Buffer,
    layout::{Constraint, Rect},
    style::Style,
    text::{Line, Span},
    widgets::{Cell, Row, Table, Widget},
};

/// Content for a table cell - either plain text with a style, or styled spans.
pub enum CellContent {
    Plain { text: String, style: Style },
    Styled(Vec<Span<'static>>),
}

impl CellContent {
    pub fn plain(text: impl Into<String>, style: Style) -> Self {
        Self::Plain {
            text: text.into(),
            style,
        }
    }

    pub fn styled(spans: Vec<Span<'static>>) -> Self {
        Self::Styled(spans)
    }

    pub fn width(&self) -> usize {
        match self {
            Self::Plain { text, .. } => text.chars().count(),
            Self::Styled(spans) => spans.iter().map(|s| s.content.chars().count()).sum(),
        }
    }

    fn into_cell(self) -> Cell<'static> {
        match self {
            Self::Plain { text, style } => Cell::from(text).style(style),
            Self::Styled(spans) => Cell::from(Line::from(spans)),
        }
    }
}

/// A single row in an aligned three-column table.
pub struct AlignedRow {
    pub name: String,
    pub name_style: Style,
    pub separator: &'static str,
    pub separator_style: Style,
    pub type_content: CellContent,
}

impl AlignedRow {
    pub fn new(
        name: impl Into<String>,
        name_style: Style,
        separator: &'static str,
        separator_style: Style,
        type_text: impl Into<String>,
        type_style: Style,
    ) -> Self {
        Self {
            name: name.into(),
            name_style,
            separator,
            separator_style,
            type_content: CellContent::plain(type_text, type_style),
        }
    }

    pub fn with_styled_type(
        name: impl Into<String>,
        name_style: Style,
        separator: &'static str,
        separator_style: Style,
        type_spans: Vec<Span<'static>>,
    ) -> Self {
        Self {
            name: name.into(),
            name_style,
            separator,
            separator_style,
            type_content: CellContent::styled(type_spans),
        }
    }

    pub fn name_width(&self) -> usize {
        self.name.chars().count()
    }

    pub fn type_width(&self) -> usize {
        self.type_content.width()
    }

    fn into_row(self) -> Row<'static> {
        Row::new(vec![
            Cell::from(self.name).style(self.name_style),
            Cell::from(self.separator).style(self.separator_style),
            self.type_content.into_cell(),
        ])
    }
}

/// A three-column aligned table widget.
///
/// Renders rows with:
/// - Column 1: Name (fixed width based on max name length)
/// - Column 2: Separator (single character like ":" or "⊢")
/// - Column 3: Type text (fills remaining space)
pub struct AlignedTable {
    rows: Vec<AlignedRow>,
}

impl AlignedTable {
    pub fn new(rows: Vec<AlignedRow>) -> Self {
        Self { rows }
    }

    fn max_name_width(&self) -> u16 {
        self.rows
            .iter()
            .map(AlignedRow::name_width)
            .max()
            .unwrap_or(0) as u16
    }
}

impl Widget for AlignedTable {
    fn render(self, area: Rect, buf: &mut Buffer) {
        let name_width = self.max_name_width().max(1);

        let rows: Vec<Row> = self.rows.into_iter().map(AlignedRow::into_row).collect();

        let table = Table::new(
            rows,
            [
                Constraint::Length(name_width),
                Constraint::Length(1),
                Constraint::Fill(1),
            ],
        );

        Widget::render(table, area, buf);
    }
}