lean-tui 1.1.1

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

use std::iter::once;

use ratatui::{
    buffer::Buffer,
    layout::Rect,
    style::{Color, Modifier, Style},
    text::{Line, Span},
    widgets::{Block, Clear, Paragraph, Widget},
};

#[derive(Debug, Clone)]
pub struct LegendItem {
    pub icon: String,
    pub color: Color,
    pub description: String,
}

impl LegendItem {
    pub fn new(icon: impl Into<String>, color: Color, description: impl Into<String>) -> Self {
        Self {
            icon: icon.into(),
            color,
            description: description.into(),
        }
    }
}

#[derive(Debug, Clone)]
pub struct LegendSection {
    pub title: String,
    pub title_color: Color,
    pub items: Vec<LegendItem>,
}

impl LegendSection {
    pub fn new(title: impl Into<String>, title_color: Color, items: Vec<LegendItem>) -> Self {
        Self {
            title: title.into(),
            title_color,
            items,
        }
    }
}

fn legend_lines(sections: &[LegendSection]) -> Vec<Line<'static>> {
    sections
        .iter()
        .flat_map(|section| {
            let title = Line::from(Span::styled(
                section.title.clone(),
                Style::new()
                    .fg(section.title_color)
                    .add_modifier(Modifier::BOLD),
            ));
            let items = section.items.iter().map(|item| {
                Line::from(vec![
                    Span::styled(item.icon.clone(), Style::new().fg(item.color)),
                    Span::raw(" "),
                    Span::raw(item.description.clone()),
                ])
            });
            once(title).chain(items)
        })
        .collect()
}

pub struct LegendPopup {
    pub sections: Vec<LegendSection>,
}

impl Widget for LegendPopup {
    fn render(self, area: Rect, buf: &mut Buffer) {
        let lines = legend_lines(&self.sections);
        let width = lines.iter().map(Line::width).max().unwrap_or_default() as u16 + 2;
        let height = (lines.len() as u16) + 2;

        let popup_area = Rect::new(1, area.height.saturating_sub(height + 1), width, height);

        Clear.render(popup_area, buf);

        let block = Block::bordered()
            .title(" Legend ")
            .border_style(Style::new().fg(Color::Reset));

        Paragraph::new(lines).block(block).render(popup_area, buf);
    }
}