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

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

use crate::{
    interactive::{InteractiveStatefulWidget, KeyEvent},
    theme::Theme,
};

const KEYBINDINGS: &[(&str, &str)] = &[
    ("[/]", "cycle display mode"),
    ("j/k", "navigate up/down"),
    ("g", "goto origin"),
    ("y", "copy to clipboard"),
    ("f", "select file"),
    ("F", "toggle follow mode"),
    ("L", "legend"),
    ("?", "close help"),
    ("q", "quit"),
];

/// State for the help menu widget.
#[derive(Default)]
pub struct HelpMenuState {
    visible: bool,
}

impl HelpMenuState {
    pub const fn toggle(&mut self) {
        self.visible = !self.visible;
    }
}

/// Widget for rendering the help menu overlay.
pub struct HelpMenuWidget;

impl StatefulWidget for HelpMenuWidget {
    type State = HelpMenuState;

    fn render(self, area: Rect, buf: &mut Buffer, state: &mut Self::State) {
        if !state.visible {
            return;
        }

        let key_style = Style::new().fg(Theme::KEYBINDING);

        let lines: Vec<Line> = KEYBINDINGS
            .iter()
            .map(|(key, desc)| {
                Line::from(vec![
                    Span::styled(format!("{key:>6}"), key_style),
                    Span::raw(format!("  {desc}")),
                ])
            })
            .collect();

        let width = 28u16;
        let height = (lines.len() as u16) + 2;
        let x = area.width.saturating_sub(width + 1);
        let y = area.height.saturating_sub(height + 2);
        let popup_area = Rect::new(x, y, width, height);

        Clear.render(popup_area, buf);

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

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

impl InteractiveStatefulWidget for HelpMenuWidget {
    type Input = ();
    type Event = KeyEvent;

    fn update_state(_state: &mut Self::State, _input: Self::Input) {}

    fn handle_event(state: &mut Self::State, event: Self::Event) -> bool {
        if !state.visible {
            return false;
        }

        match event.code {
            KeyCode::Esc | KeyCode::Char('?') => {
                state.visible = false;
                true
            }
            _ => false,
        }
    }
}