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
88
89
90
91
92
93
94
95
96
97
98
99
100
101

use crossterm::event::KeyEvent;
use ratatui::layout::{Position, Rect};
use tokio::sync::mpsc::UnboundedSender;

use crate::{
    navigation::Direction,
    protocol::{ClientToServerCommand, ServerToClientMessage},
    selection::Selection,
    tcp_client::WorkerInfo,
};

#[derive(Clone)]
pub enum AppMessage {
    KeyPressed {
        key: KeyEvent,
    },
    WorkerConnected {
        port: u16,
        commands: UnboundedSender<ClientToServerCommand>,
    },
    WorkerSent {
        port: u16,
        message: ServerToClientMessage,
    },
    WorkerSentInvalid {
        port: u16,
        error: String,
    },
    WorkerDisconnected {
        port: u16,
    },
    WorkersDiscovered {
        workers: Vec<WorkerInfo>,
    },
    Select {
        selection: Selection,
    },
    ShowError {
        message: String,
    },
}

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum GlobalAction {
    Quit,
    ToggleHelp,
    ToggleLegend,
    ToggleInputPane,
    ToggleOutputPane,
    OpenWorkerSelector,
    ToggleFollowMode,
    NextDisplayMode,
    PreviousDisplayMode,
    GotoSelection,
    CopySelection,
    CycleTimingDisplay,
    CloseOverlay,
}

#[derive(Debug, Clone, Copy)]
pub enum ModeAction {
    Move { direction: Direction },
    FlipOrientation,
    ToggleExpanded,
    TogglePreviousPane,
    ToggleNextPane,
}

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum WorkerSelectorAction {
    HighlightPrevious,
    HighlightNext,
    Connect,
    Rescan,
    Cancel,
}

#[derive(Clone)]
pub struct ClickTarget {
    pub area: Rect,
    pub message: AppMessage,
}

pub fn find_click_target(
    click_targets: &[ClickTarget],
    column: u16,
    row: u16,
) -> Option<AppMessage> {
    click_targets
        .iter()
        .rev()
        .find(|target| target.area.contains(Position::new(column, row)))
        .map(|target| target.message.clone())
}

pub fn selection_click_target(area: Rect, selection: Selection) -> ClickTarget {
    ClickTarget {
        area,
        message: AppMessage::Select { selection },
    }
}