logicaffeine_web/ui/components/
context_view.rs

1//! Context view panel for Code mode.
2//!
3//! Displays the current proof context including definitions, inductive types,
4//! and their constructors. Organizes entries by category.
5//!
6//! # Props
7//!
8//! - `definitions` - List of term definitions
9//! - `inductives` - List of inductive type definitions
10//!
11//! # Key Types
12//!
13//! - [`ContextEntry`] - A single definition or type in the context
14//! - [`EntryKind`] - Definition, Inductive, or Constructor
15
16use dioxus::prelude::*;
17
18const CONTEXT_VIEW_STYLE: &str = r#"
19.context-view {
20    display: flex;
21    flex-direction: column;
22    height: 100%;
23    background: #12161c;
24    font-family: 'SF Mono', 'Fira Code', monospace;
25}
26
27.context-view-header {
28    padding: 12px 16px;
29    border-bottom: 1px solid rgba(255, 255, 255, 0.08);
30    background: rgba(255, 255, 255, 0.02);
31}
32
33.context-view-title {
34    font-size: 14px;
35    font-weight: 600;
36    color: rgba(255, 255, 255, 0.9);
37}
38
39.context-sections {
40    flex: 1;
41    overflow: auto;
42    padding: 12px;
43}
44
45.context-section {
46    margin-bottom: 20px;
47}
48
49.context-section-header {
50    font-size: 11px;
51    font-weight: 600;
52    text-transform: uppercase;
53    letter-spacing: 0.5px;
54    color: rgba(255, 255, 255, 0.4);
55    margin-bottom: 8px;
56    padding-bottom: 4px;
57    border-bottom: 1px solid rgba(255, 255, 255, 0.06);
58}
59
60.context-item {
61    padding: 8px 10px;
62    margin-bottom: 4px;
63    background: rgba(255, 255, 255, 0.02);
64    border-radius: 4px;
65    font-size: 12px;
66    line-height: 1.5;
67}
68
69.context-item-name {
70    color: #61afef;
71    font-weight: 500;
72}
73
74.context-item-type {
75    color: rgba(255, 255, 255, 0.6);
76    margin-left: 8px;
77}
78
79.context-item-type::before {
80    content: ": ";
81    color: rgba(255, 255, 255, 0.3);
82}
83
84.context-item-body {
85    margin-top: 4px;
86    padding-top: 4px;
87    border-top: 1px dashed rgba(255, 255, 255, 0.06);
88    color: rgba(255, 255, 255, 0.5);
89    font-size: 11px;
90}
91
92.context-empty {
93    display: flex;
94    flex-direction: column;
95    align-items: center;
96    justify-content: center;
97    height: 100%;
98    color: rgba(255, 255, 255, 0.4);
99    text-align: center;
100    padding: 20px;
101    font-size: 13px;
102}
103
104/* Type keywords highlighting */
105.type-keyword {
106    color: #c678dd;
107}
108
109.type-name {
110    color: #e5c07b;
111}
112
113.type-arrow {
114    color: rgba(255, 255, 255, 0.4);
115}
116"#;
117
118/// A definition entry in the context.
119#[derive(Clone, PartialEq)]
120pub struct ContextEntry {
121    pub name: String,
122    pub ty: String,
123    pub body: Option<String>,
124    pub kind: EntryKind,
125}
126
127#[derive(Clone, Copy, PartialEq)]
128pub enum EntryKind {
129    Definition,
130    Inductive,
131    Constructor,
132}
133
134#[component]
135pub fn ContextView(
136    definitions: Vec<ContextEntry>,
137    inductives: Vec<ContextEntry>,
138) -> Element {
139    rsx! {
140        style { "{CONTEXT_VIEW_STYLE}" }
141
142        div { class: "context-view",
143            // Header
144            div { class: "context-view-header",
145                span { class: "context-view-title", "Context" }
146            }
147
148            // Sections
149            div { class: "context-sections",
150                if definitions.is_empty() && inductives.is_empty() {
151                    div { class: "context-empty",
152                        "No definitions in scope"
153                    }
154                } else {
155                    // Inductive types section
156                    if !inductives.is_empty() {
157                        div { class: "context-section",
158                            div { class: "context-section-header", "Inductive Types" }
159                            for entry in inductives.iter() {
160                                ContextItem {
161                                    key: "{entry.name}",
162                                    entry: entry.clone(),
163                                }
164                            }
165                        }
166                    }
167
168                    // Definitions section
169                    if !definitions.is_empty() {
170                        div { class: "context-section",
171                            div { class: "context-section-header", "Definitions" }
172                            for entry in definitions.iter() {
173                                ContextItem {
174                                    key: "{entry.name}",
175                                    entry: entry.clone(),
176                                }
177                            }
178                        }
179                    }
180                }
181            }
182        }
183    }
184}
185
186#[component]
187fn ContextItem(entry: ContextEntry) -> Element {
188    rsx! {
189        div { class: "context-item",
190            div {
191                span { class: "context-item-name", "{entry.name}" }
192                span { class: "context-item-type", "{entry.ty}" }
193            }
194            if let Some(body) = &entry.body {
195                div { class: "context-item-body", ":= {body}" }
196            }
197        }
198    }
199}
logicaffeine_web/ui/components/context_view.rs

logicaffeine_web/ui/components/
context_view.rs
