2026-03-20 11:01:04 +01:00
|
|
|
//! Browser panel for theory/instance navigation
|
|
|
|
|
//!
|
|
|
|
|
//! Displays a tree view of all theories and instances.
|
|
|
|
|
|
|
|
|
|
use eframe::egui;
|
|
|
|
|
|
|
|
|
|
use crate::gui::state::{GuiState, SelectedItem};
|
|
|
|
|
|
|
|
|
|
/// Browser panel for navigating theories and instances
|
|
|
|
|
pub struct BrowserPanel {
|
|
|
|
|
/// Search/filter text
|
|
|
|
|
filter: String,
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
impl BrowserPanel {
|
|
|
|
|
pub fn new() -> Self {
|
|
|
|
|
Self {
|
|
|
|
|
filter: String::new(),
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
pub fn show(&mut self, ui: &mut egui::Ui, state: &mut GuiState) {
|
|
|
|
|
ui.heading("Browser");
|
|
|
|
|
ui.separator();
|
|
|
|
|
|
|
|
|
|
// Filter input
|
|
|
|
|
ui.horizontal(|ui| {
|
|
|
|
|
ui.label("Filter:");
|
|
|
|
|
ui.text_edit_singleline(&mut self.filter);
|
|
|
|
|
});
|
|
|
|
|
ui.add_space(4.0);
|
|
|
|
|
|
|
|
|
|
// Scrollable tree view
|
|
|
|
|
egui::ScrollArea::vertical()
|
|
|
|
|
.auto_shrink([false, false])
|
|
|
|
|
.show(ui, |ui| {
|
|
|
|
|
self.show_theories_section(ui, state);
|
|
|
|
|
ui.add_space(8.0);
|
|
|
|
|
self.show_instances_section(ui, state);
|
|
|
|
|
});
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
fn show_theories_section(&mut self, ui: &mut egui::Ui, state: &mut GuiState) {
|
|
|
|
|
let theories = state.repl.list_theories();
|
|
|
|
|
let filtered: Vec<_> = theories
|
|
|
|
|
.iter()
|
|
|
|
|
.filter(|t| {
|
|
|
|
|
self.filter.is_empty()
|
|
|
|
|
|| t.name.to_lowercase().contains(&self.filter.to_lowercase())
|
|
|
|
|
})
|
|
|
|
|
.collect();
|
|
|
|
|
|
|
|
|
|
let header = if self.filter.is_empty() {
|
|
|
|
|
format!("Theories ({})", theories.len())
|
|
|
|
|
} else {
|
|
|
|
|
format!("Theories ({}/{})", filtered.len(), theories.len())
|
|
|
|
|
};
|
|
|
|
|
|
2026-03-20 11:05:58 +01:00
|
|
|
let response = egui::CollapsingHeader::new(header)
|
2026-03-20 11:01:04 +01:00
|
|
|
.default_open(state.theories_expanded)
|
|
|
|
|
.show(ui, |ui| {
|
|
|
|
|
if filtered.is_empty() {
|
|
|
|
|
ui.label("(none)");
|
|
|
|
|
} else {
|
|
|
|
|
for theory in filtered {
|
|
|
|
|
let is_selected = matches!(
|
|
|
|
|
&state.selected_item,
|
|
|
|
|
Some(SelectedItem::Theory(name)) if name == &theory.name
|
|
|
|
|
);
|
|
|
|
|
|
|
|
|
|
let label = format!(
|
|
|
|
|
"{} ({} sorts{}{}{})",
|
|
|
|
|
theory.name,
|
|
|
|
|
theory.num_sorts,
|
|
|
|
|
if theory.num_functions > 0 {
|
|
|
|
|
format!(", {} funcs", theory.num_functions)
|
|
|
|
|
} else {
|
|
|
|
|
String::new()
|
|
|
|
|
},
|
|
|
|
|
if theory.num_relations > 0 {
|
|
|
|
|
format!(", {} rels", theory.num_relations)
|
|
|
|
|
} else {
|
|
|
|
|
String::new()
|
|
|
|
|
},
|
|
|
|
|
if theory.num_axioms > 0 {
|
|
|
|
|
format!(", {} axioms", theory.num_axioms)
|
|
|
|
|
} else {
|
|
|
|
|
String::new()
|
|
|
|
|
},
|
|
|
|
|
);
|
|
|
|
|
|
|
|
|
|
if ui.selectable_label(is_selected, label).clicked() {
|
|
|
|
|
state.selected_item = Some(SelectedItem::Theory(theory.name.clone()));
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
});
|
2026-03-20 11:05:58 +01:00
|
|
|
state.theories_expanded = response.fully_open();
|
2026-03-20 11:01:04 +01:00
|
|
|
}
|
|
|
|
|
|
|
|
|
|
fn show_instances_section(&mut self, ui: &mut egui::Ui, state: &mut GuiState) {
|
|
|
|
|
let instances = state.repl.list_instances();
|
|
|
|
|
let filtered: Vec<_> = instances
|
|
|
|
|
.iter()
|
|
|
|
|
.filter(|i| {
|
|
|
|
|
self.filter.is_empty()
|
|
|
|
|
|| i.name.to_lowercase().contains(&self.filter.to_lowercase())
|
|
|
|
|
|| i.theory_name
|
|
|
|
|
.to_lowercase()
|
|
|
|
|
.contains(&self.filter.to_lowercase())
|
|
|
|
|
})
|
|
|
|
|
.collect();
|
|
|
|
|
|
|
|
|
|
let header = if self.filter.is_empty() {
|
|
|
|
|
format!("Instances ({})", instances.len())
|
|
|
|
|
} else {
|
|
|
|
|
format!("Instances ({}/{})", filtered.len(), instances.len())
|
|
|
|
|
};
|
|
|
|
|
|
2026-03-20 11:05:58 +01:00
|
|
|
let response = egui::CollapsingHeader::new(header)
|
2026-03-20 11:01:04 +01:00
|
|
|
.default_open(state.instances_expanded)
|
|
|
|
|
.show(ui, |ui| {
|
|
|
|
|
if filtered.is_empty() {
|
|
|
|
|
ui.label("(none)");
|
|
|
|
|
} else {
|
|
|
|
|
for instance in filtered {
|
|
|
|
|
let is_selected = matches!(
|
|
|
|
|
&state.selected_item,
|
|
|
|
|
Some(SelectedItem::Instance(name)) if name == &instance.name
|
|
|
|
|
);
|
|
|
|
|
|
|
|
|
|
let label = format!(
|
|
|
|
|
"{} : {} ({} elems)",
|
|
|
|
|
instance.name, instance.theory_name, instance.num_elements
|
|
|
|
|
);
|
|
|
|
|
|
|
|
|
|
let response = ui.selectable_label(is_selected, label);
|
|
|
|
|
|
|
|
|
|
// Left click to select
|
|
|
|
|
if response.clicked() {
|
|
|
|
|
state.selected_item =
|
|
|
|
|
Some(SelectedItem::Instance(instance.name.clone()));
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
// Right-click context menu
|
|
|
|
|
response.context_menu(|ui| {
|
|
|
|
|
if ui.button("Inspect").clicked() {
|
|
|
|
|
state.selected_item =
|
|
|
|
|
Some(SelectedItem::Instance(instance.name.clone()));
|
|
|
|
|
ui.close_menu();
|
|
|
|
|
}
|
|
|
|
|
if ui.button("Run Chase").clicked() {
|
|
|
|
|
// This will be handled by the app
|
|
|
|
|
state.selected_item =
|
|
|
|
|
Some(SelectedItem::Instance(instance.name.clone()));
|
|
|
|
|
state.log_info(format!(
|
|
|
|
|
"Use Chase menu to run chase on '{}'",
|
|
|
|
|
instance.name
|
|
|
|
|
));
|
|
|
|
|
ui.close_menu();
|
|
|
|
|
}
|
|
|
|
|
if ui.button("View Graph").clicked() {
|
|
|
|
|
state.show_graph(&instance.name, None);
|
|
|
|
|
ui.close_menu();
|
|
|
|
|
}
|
|
|
|
|
});
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
});
|
2026-03-20 11:05:58 +01:00
|
|
|
state.instances_expanded = response.fully_open();
|
2026-03-20 11:01:04 +01:00
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
impl Default for BrowserPanel {
|
|
|
|
|
fn default() -> Self {
|
|
|
|
|
Self::new()
|
|
|
|
|
}
|
|
|
|
|
}
|