WIP

Cargo.toml

@@ -31,15 +31,15 @@ default = []
 gui = ["eframe", "egui_extras", "rfd"]
 
 [dependencies.eframe]
-version = "0.29"
+version = "0.33.3"
 optional = true
 
 [dependencies.egui_extras]
-version = "0.29"
+version = "0.33.3"
 optional = true
 
 [dependencies.rfd]
-version = "0.15"
+version = "0.17.2"
 optional = true
 
 [[bin]]

README2.md

@@ -79,18 +79,19 @@ src/gui/
 - Filter/search functionality
 - Click to select, right-click for context menu
 - Shows counts (sorts, functions, relations, axioms, elements)
+- Fixed-width docked sidebar
 
-**Editor Panel (Center Top)**
+**Editor Panel (Center)**
 - Multi-line code editor
-- Line numbers
 - Run button (or Ctrl+Enter) to execute code
 - Clear button
 
-**Inspector Panel (Center Bottom)**
+**Inspector Panel (Right)**
 - Theory details: parameters, sorts, functions, relations, instance fields, axioms
 - Instance details: elements by sort, function values, relation tuples, nested instances
 - Collapsible sections
 - "View Graph" button for instances
+- Fixed-width docked sidebar in the main workspace view
 
 **Console Panel (Bottom)**
 - Scrollable message log
@@ -103,11 +104,13 @@ src/gui/
   - Type `:inspect <name>` to inspect
   - Type `:chase <instance>` to run chase
   - Or type geolog code directly
+- Fixed-height docked footer
 
-**Adjustable Panels**
+**Layout**
-- Browser panel (left): drag right edge to resize
+- Docked workspace layout for stability
-- Console panel (bottom): drag top edge to resize
+- Browser on the left, editor in the center, inspector on the right
-- Editor/Inspector split: drag the separator bar between them
+- Console fixed at the bottom
+- Chase and graph visualizations replace the central workspace when active
 
 **Chase Visualization**
 - Step/Run All/Stop controls
@@ -129,22 +132,14 @@ src/gui/
 ```
 ┌─────────────────────────────────────────────────────────────┐
 │  File   Edit   View   Chase   Help                          │
-├────────────┬────────────────────────────────────────────────┤
+├──────────────┬──────────────────────────────┬───────────────┤
-│ ▼ Theories │  ┌─────────────────────────────────────────┐   │
+│ Browser      │ Editor                       │ Inspector     │
-│   Preorder │  │ Editor                                  │   │
+│ ▼ Theories   │ theory Foo {                 │ Chain3        │
-│   Graph    │  │ theory Foo {                            │   │
+│   Preorder   │   X : Sort;                  │ : Preorder    │
-│ ▼ Instances│  │   X : Sort;                             │   │
+│ ▼ Instances  │ }           [Run] [Clear]    │ ▼ Elements    │
-│   Chain3   │  │ }                     [Run] [Clear]     │   │
+│   Chain3     │                              │ ▼ Relations   │
-│            │  ├─────────────────────────────────────────┤   │
+│              │                              │ [View Graph]  │
-│            │  │ ═══════════ [drag to resize] ═══════════│   │
+├──────────────┴──────────────────────────────┴───────────────┤
-│            │  ├─────────────────────────────────────────┤   │
-│            │  │ Inspector: Chain3 : Preorder            │   │
-│            │  │ ▼ Elements (3)                          │   │
-│            │  │   X: bot, mid, top                      │   │
-│            │  │ ▼ Relations                             │   │
-│            │  │   leq: 6 tuples [View Graph]            │   │
-│            │  └─────────────────────────────────────────┘   │
-├────────────┴────────────────────────────────────────────────┤
 │ Console                                              [Clear]│
 │ > Defined theory Preorder (1 sorts, 1 relations, 2 axioms)  │
 │ + Defined instance Chain3 : Preorder (3 elements)          │

src/bin/geolog-gui.rs

@@ -113,6 +113,7 @@ fn parse_args(args: &[String]) -> (Option<PathBuf>, Vec<PathBuf>) {
 fn setup_fonts(ctx: &egui::Context) {
     // Use a slightly larger default font
     let mut style = (*ctx.style()).clone();
+    style.animation_time = 0.0;
     style.text_styles.insert(
         egui::TextStyle::Body,
         egui::FontId::proportional(14.0),
@@ -129,6 +130,11 @@ fn setup_fonts(ctx: &egui::Context) {
     // Set up dark theme with custom colors
     style.visuals = egui::Visuals::dark();
     style.visuals.override_text_color = Some(egui::Color32::from_gray(220));
+    style.visuals.widgets.noninteractive.expansion = 0.0;
+    style.visuals.widgets.inactive.expansion = 0.0;
+    style.visuals.widgets.hovered.expansion = 0.0;
+    style.visuals.widgets.active.expansion = 0.0;
+    style.visuals.widgets.open.expansion = 0.0;
 
     ctx.set_style(style);
 }

src/gui/app.rs

@@ -21,9 +21,6 @@ pub struct GeologApp {
     console: ConsolePanel,
     chase_viz: ChaseVisualization,
     graph_view: GraphView,
-
-    /// Editor/Inspector split ratio (0.0 to 1.0, where 0.5 = equal)
-    editor_split: f32,
 }
 
 impl GeologApp {
@@ -37,7 +34,6 @@ impl GeologApp {
             console: ConsolePanel::new(),
             chase_viz: ChaseVisualization::new(),
             graph_view: GraphView::new(),
-            editor_split: 0.5, // 50% editor, 50% inspector
         }
     }
 
@@ -290,80 +286,7 @@ impl GeologApp {
     fn central_panel(&mut self, ui: &mut egui::Ui) {
         match self.state.central_view {
             CentralView::EditorAndInspector => {
-                // Split vertically: editor on top, inspector on bottom
-                let available_height = ui.available_height();
-                let splitter_height = 8.0;
-                // Ensure heights are never negative
-                let usable_height = (available_height - splitter_height).max(0.0);
-                let editor_height = (usable_height * self.editor_split).max(0.0);
-                let inspector_height = (usable_height * (1.0 - self.editor_split)).max(0.0);
-
-                // Editor section
-                ui.allocate_ui_with_layout(
-                    egui::vec2(ui.available_width(), editor_height),
-                    egui::Layout::top_down(egui::Align::LEFT),
-                    |ui| {
                 self.editor.show(ui, &mut self.state);
-                    },
-                );
-
-                // Draggable splitter
-                let splitter_response = ui.allocate_response(
-                    egui::vec2(ui.available_width(), splitter_height),
-                    egui::Sense::drag(),
-                );
-
-                // Draw splitter bar
-                let splitter_rect = splitter_response.rect;
-                let is_dragging = splitter_response.dragged();
-                let is_hovered = splitter_response.hovered();
-
-                let splitter_color = if is_dragging {
-                    egui::Color32::from_rgb(100, 150, 255)
-                } else if is_hovered {
-                    egui::Color32::from_rgb(80, 80, 100)
-                } else {
-                    egui::Color32::from_rgb(60, 60, 70)
-                };
-
-                ui.painter().rect_filled(splitter_rect, 0.0, splitter_color);
-
-                // Draw grip lines
-                let center_y = splitter_rect.center().y;
-                let grip_width = 30.0;
-                let grip_x = splitter_rect.center().x;
-                for i in -1..=1 {
-                    let y = center_y + (i as f32) * 2.0;
-                    ui.painter().line_segment(
-                        [
-                            egui::pos2(grip_x - grip_width / 2.0, y),
-                            egui::pos2(grip_x + grip_width / 2.0, y),
-                        ],
-                        egui::Stroke::new(1.0, egui::Color32::GRAY),
-                    );
-                }
-
-                // Handle dragging
-                if is_dragging {
-                    let delta = splitter_response.drag_delta().y;
-                    let divisor = (available_height - splitter_height).max(1.0);
-                    let new_split = self.editor_split + delta / divisor;
-                    self.editor_split = new_split.clamp(0.1, 0.9);
-                }
-
-                // Change cursor when hovering
-                if is_hovered || is_dragging {
-                    ui.ctx().set_cursor_icon(egui::CursorIcon::ResizeVertical);
-                }
-
-                // Inspector section
-                ui.allocate_ui_with_layout(
-                    egui::vec2(ui.available_width(), inspector_height),
-                    egui::Layout::top_down(egui::Align::LEFT),
-                    |ui| {
-                        self.inspector.show(ui, &mut self.state);
-                    },
-                );
             }
             CentralView::ChaseVisualization => {
                 self.chase_viz.show(ui, &mut self.state);
@@ -384,18 +307,28 @@ impl eframe::App for GeologApp {
 
         // Left panel: Browser
         egui::SidePanel::left("browser_panel")
-            .default_width(200.0)
+            .default_width(240.0)
-            .min_width(150.0)
+            .min_width(240.0)
-            .resizable(true)
+            .resizable(false)
             .show(ctx, |ui| {
                 self.browser.show(ui, &mut self.state);
             });
 
+        if self.state.central_view == CentralView::EditorAndInspector {
+            egui::SidePanel::right("inspector_panel")
+                .default_width(340.0)
+                .min_width(340.0)
+                .resizable(false)
+                .show(ctx, |ui| {
+                    self.inspector.show(ui, &mut self.state);
+                });
+        }
+
         // Bottom panel: Console
         egui::TopBottomPanel::bottom("console_panel")
-            .default_height(150.0)
+            .default_height(200.0)
-            .min_height(100.0)
+            .min_height(200.0)
-            .resizable(true)
+            .resizable(false)
             .show(ctx, |ui| {
                 self.console.show(ui, &mut self.state);
             });

src/gui/panels/console.rs

@@ -3,6 +3,7 @@
 //! Shows a scrollable log of messages with color coding and a REPL input.
 
 use eframe::egui;
+use egui_extras::{Size, StripBuilder};
 
 use crate::gui::state::{GuiState, MessageKind};
 use crate::repl::{MetaCommand, ListTarget, ExecuteResult};
@@ -30,31 +31,44 @@ impl ConsolePanel {
     }
 
     pub fn show(&mut self, ui: &mut egui::Ui, state: &mut GuiState) {
-        // Header with title and buttons
+        StripBuilder::new(ui)
+            .size(Size::exact(28.0))
+            .size(Size::remainder().at_least(80.0))
+            .size(Size::exact(28.0))
+            .vertical(|mut strip| {
+                strip.cell(|ui| {
                     ui.horizontal(|ui| {
                         ui.heading("Console");
 
                         ui.with_layout(egui::Layout::right_to_left(egui::Align::Center), |ui| {
-                if ui.button("Clear").clicked() {
+                            if ui
+                                .add_sized([64.0, 22.0], egui::Button::new("Clear"))
+                                .clicked()
+                            {
                                 state.clear_console();
                             }
 
-                ui.checkbox(&mut self.auto_scroll, "Auto-scroll");
+                            ui.add_sized(
+                                [112.0, 22.0],
+                                egui::Checkbox::new(&mut self.auto_scroll, "Auto-scroll"),
+                            );
 
-                ui.label(format!("{} messages", state.console_messages.len()));
+                            ui.add_sized(
+                                [96.0, 22.0],
+                                egui::Label::new(format!("{} messages", state.console_messages.len())),
+                            );
+                        });
                     });
                 });
 
-        ui.separator();
+                strip.cell(|ui| {
-
+                    egui::Frame::default()
-        // Scrollable message area (takes most of the space)
+                        .inner_margin(egui::Margin::same(4))
-        let available_height = (ui.available_height() - 30.0).max(50.0); // Reserve space for input
+                        .show(ui, |ui| {
-        let scroll_area = egui::ScrollArea::vertical()
+                            egui::ScrollArea::vertical()
                                 .auto_shrink([false, false])
-            .max_height(available_height)
+                                .stick_to_bottom(self.auto_scroll)
-            .stick_to_bottom(self.auto_scroll);
+                                .show(ui, |ui| {
-
-        scroll_area.show(ui, |ui| {
                                     if state.console_messages.is_empty() {
                                         ui.label("Type commands below (e.g., :help, :list, or geolog code)");
                                     } else {
@@ -74,10 +88,13 @@ impl ConsolePanel {
                                             };
 
                                             ui.horizontal(|ui| {
-                        ui.label(
+                                                ui.add_sized(
+                                                    [12.0, 18.0],
+                                                    egui::Label::new(
                                                         egui::RichText::new(prefix)
                                                             .color(color)
                                                             .monospace(),
+                                                    ),
                                                 );
                                                 ui.label(
                                                     egui::RichText::new(&message.text)
@@ -88,30 +105,35 @@ impl ConsolePanel {
                                         }
                                     }
                                 });
+                        });
+                });
 
-        // REPL input at the bottom
+                strip.cell(|ui| {
-        ui.separator();
                     ui.horizontal(|ui| {
-            ui.label(
+                        ui.add_sized(
+                            [68.0, 22.0],
+                            egui::Label::new(
                                 egui::RichText::new("geolog>")
                                     .monospace()
                                     .color(egui::Color32::from_rgb(100, 150, 255)),
+                            ),
                         );
 
-            let response = ui.add(
+                        let run_width = 56.0;
+                        let spacing = ui.spacing().item_spacing.x;
+                        let input_width = (ui.available_width() - run_width - spacing).max(120.0);
+                        let response = ui.add_sized(
+                            [input_width, 22.0],
                             egui::TextEdit::singleline(&mut self.input)
                                 .font(egui::FontId::monospace(13.0))
-                    .desired_width((ui.available_width() - 60.0).max(50.0))
                                 .hint_text(":help for commands"),
                         );
 
-            // Handle Enter key
                         if response.lost_focus() && ui.input(|i| i.key_pressed(egui::Key::Enter)) {
                             self.execute_input(state);
                             response.request_focus();
                         }
 
-            // Handle Up/Down for history
                         if response.has_focus() {
                             if ui.input(|i| i.key_pressed(egui::Key::ArrowUp)) {
                                 self.history_up();
@@ -121,10 +143,15 @@ impl ConsolePanel {
                             }
                         }
 
-            if ui.button("Run").clicked() {
+                        if ui
+                            .add_sized([run_width, 22.0], egui::Button::new("Run"))
+                            .clicked()
+                        {
                             self.execute_input(state);
                         }
                     });
+                });
+            });
     }
 
     fn execute_input(&mut self, state: &mut GuiState) {

src/gui/panels/editor.rs

@@ -7,16 +7,11 @@ use eframe::egui;
 use crate::gui::state::GuiState;
 
 /// Code editor panel
-pub struct EditorPanel {
+pub struct EditorPanel {}
-    /// Whether to show line numbers
-    show_line_numbers: bool,
-}
 
 impl EditorPanel {
     pub fn new() -> Self {
-        Self {
+        Self {}
-            show_line_numbers: true,
-        }
     }
 
     pub fn show(&mut self, ui: &mut egui::Ui, state: &mut GuiState) {
@@ -59,39 +54,8 @@ impl EditorPanel {
         // Use a monospace font for code
         let font_id = egui::FontId::monospace(14.0);
 
-        // Calculate line numbers if needed
+        // Main editor area - simplified layout without line numbers column
-        let line_count = state.editor_content.lines().count().max(1);
+        // to avoid layout instability from horizontal split calculations
-        let line_number_width = if self.show_line_numbers {
-            let digits = (line_count as f32).log10().floor() as usize + 1;
-            digits.max(2) as f32 * 10.0 + 8.0
-        } else {
-            0.0
-        };
-
-        ui.horizontal(|ui| {
-            // Line numbers column
-            if self.show_line_numbers {
-                ui.allocate_ui_with_layout(
-                    egui::vec2(line_number_width, ui.available_height().max(0.0)),
-                    egui::Layout::top_down(egui::Align::RIGHT),
-                    |ui| {
-                        ui.style_mut().visuals.override_text_color =
-                            Some(egui::Color32::GRAY);
-
-                        for i in 1..=line_count {
-                            ui.label(
-                                egui::RichText::new(format!("{}", i))
-                                    .font(font_id.clone())
-                                    .color(egui::Color32::GRAY),
-                            );
-                        }
-                    },
-                );
-
-                ui.separator();
-            }
-
-            // Main editor area
         let text_edit = egui::TextEdit::multiline(&mut state.editor_content)
             .font(font_id)
             .code_editor()
@@ -110,7 +74,6 @@ impl EditorPanel {
                 }
             }
         }
-        });
     }
 }
 

src/gui/state.rs

@@ -5,6 +5,7 @@
 use std::collections::HashSet;
 use std::path::PathBuf;
 
+use crate::core::Structure;
 use crate::repl::{InstanceDetail, ReplState, TheoryDetail};
 
 /// What item is currently selected in the browser
@@ -57,6 +58,7 @@ pub enum ChaseMode {
 pub struct ChaseVisualizationState {
     pub mode: ChaseMode,
     pub instance_name: String,
+    pub initial_structure: Structure,
     pub events: Vec<ChaseEventRecord>,
     pub current_event: usize,
     pub current_iteration: usize,
@@ -65,10 +67,11 @@ pub struct ChaseVisualizationState {
 }
 
 impl ChaseVisualizationState {
-    pub fn new(instance_name: String) -> Self {
+    pub fn new(instance_name: String, initial_structure: Structure) -> Self {
         Self {
             mode: ChaseMode::Idle,
             instance_name,
+            initial_structure,
             events: Vec::new(),
             current_event: 0,
             current_iteration: 0,
@@ -308,7 +311,15 @@ impl GuiState {
 
     /// Start a chase visualization for an instance
     pub fn start_chase(&mut self, instance_name: &str) {
-        self.chase_state = Some(ChaseVisualizationState::new(instance_name.to_string()));
+        let Some(entry) = self.repl.instances.get(instance_name) else {
+            self.log_error(format!("Instance '{}' not found", instance_name));
+            return;
+        };
+
+        self.chase_state = Some(ChaseVisualizationState::new(
+            instance_name.to_string(),
+            entry.structure.clone(),
+        ));
         self.central_view = CentralView::ChaseVisualization;
     }
 

src/gui/visualizations/chase.rs

@@ -3,6 +3,7 @@
 //! Provides step-through debugging and visualization of the chase algorithm.
 
 use eframe::egui;
+use std::collections::HashSet;
 
 use crate::core::RelationStorage;
 use crate::gui::state::{ChaseEventRecord, ChaseMode, ChaseVisualizationState, CentralView, GuiState, SelectedItem};
@@ -67,9 +68,9 @@ impl ChaseVisualization {
 
     fn show_chase_panel(&mut self, ui: &mut egui::Ui, state: &mut GuiState) {
         // Read mode and instance_name before mutable operations
-        let (mode, instance_name) = {
+        let mode = {
             let chase_state = state.chase_state.as_ref().unwrap();
-            (chase_state.mode, chase_state.instance_name.clone())
+            chase_state.mode
         };
 
         // Control buttons
@@ -130,7 +131,7 @@ impl ChaseVisualization {
             }
         }
         if reset_clicked {
-            state.chase_state = Some(ChaseVisualizationState::new(instance_name));
+            self.reset_chase(state);
         }
         if close_clicked {
             state.chase_state = None;
@@ -283,14 +284,40 @@ impl ChaseVisualization {
         }
     }
 
+    fn reset_chase(&mut self, state: &mut GuiState) {
+        let Some(chase_state) = &state.chase_state else {
+            return;
+        };
+
+        let instance_name = chase_state.instance_name.clone();
+        let initial_structure = chase_state.initial_structure.clone();
+        let breakpoints = chase_state.breakpoints.clone();
+
+        let Some(entry) = state.repl.instances.get_mut(&instance_name) else {
+            state.log_error(format!("Instance '{}' not found", instance_name));
+            return;
+        };
+
+        entry.structure = initial_structure.clone();
+
+        let mut new_state = ChaseVisualizationState::new(instance_name, initial_structure);
+        new_state.breakpoints = breakpoints;
+        state.chase_state = Some(new_state);
+        self.new_breakpoint.clear();
+        state.log_info("Chase visualization reset");
+    }
+
     /// Execute a single step of the chase
     fn step_chase(&mut self, state: &mut GuiState) {
         let instance_name = match &state.chase_state {
             Some(s) => s.instance_name.clone(),
             None => return,
         };
-
+        let breakpoints = state
-        let current_iteration = state.chase_state.as_ref().map(|s| s.current_iteration).unwrap_or(0);
+            .chase_state
+            .as_ref()
+            .map(|s| s.breakpoints.clone())
+            .unwrap_or_default();
 
         // Get theory name first (immutable borrow)
         let theory_name = match state.repl.instances.get(&instance_name) {
@@ -313,13 +340,7 @@ impl ChaseVisualization {
         let entry = state.repl.instances.get_mut(&instance_name).unwrap();
 
         // Create a GUI observer that records events
-        let mut observer = GuiChaseObserver {
+        let mut observer = GuiChaseObserver::new(&entry.slid_to_name, Some(1), breakpoints);
-            events: Vec::new(),
-            slid_to_name: &entry.slid_to_name,
-            iteration: current_iteration,
-            step_mode: true,
-            steps_remaining: 1,
-        };
 
         // Run chase with observer (just one step)
         let sig = &theory.theory.signature;
@@ -332,33 +353,43 @@ impl ChaseVisualization {
             &mut entry.structure,
             &mut state.repl.store.universe,
             sig,
-            1, // Just one iteration
+            100,
             &mut observer,
         );
 
-        // Record events
+        let GuiChaseObserver {
-        let events = observer.events;
+            events,
+            iteration: current_iteration,
+            breakpoint_hit: paused_on_breakpoint,
+            completed_iterations,
+            ..
+        } = observer;
         if let Some(chase_state) = &mut state.chase_state {
             chase_state.mode = ChaseMode::Stepping;
-            for event in events {
+            chase_state.events.extend(events);
-                chase_state.events.push(event);
+            if !chase_state.events.is_empty() {
+                chase_state.current_event = chase_state.events.len() - 1;
             }
-            chase_state.current_event = chase_state.events.len().saturating_sub(1);
+            chase_state.current_iteration = chase_state.current_iteration.max(current_iteration);
-            chase_state.current_iteration += 1;
 
-            if let Ok(iterations) = result {
+            if let Some(iterations) = completed_iterations {
-                if iterations == 0 {
                 chase_state.mode = ChaseMode::Completed;
-                    chase_state.total_iterations = Some(chase_state.current_iteration);
+                chase_state.current_iteration = iterations;
-                }
+                chase_state.total_iterations = Some(iterations);
             }
         }
 
-        // Log completion separately
+        match result {
-        if let Ok(iterations) = result {
+            Ok(_) => {
-            if iterations == 0 {
+                if let Some(bp) = paused_on_breakpoint {
-                let total = state.chase_state.as_ref().map(|s| s.current_iteration).unwrap_or(0);
+                    state.log_info(format!("Paused at breakpoint '{}'", bp));
-                state.log_success(format!("Chase completed after {} iterations", total));
+                }
+                if let Some(iterations) = completed_iterations {
+                    state.log_success(format!("Chase completed after {} iterations", iterations));
+                }
+            }
+            Err(e) => {
+                state.log_error(format!("Chase error: {}", e));
             }
         }
     }
@@ -387,35 +418,71 @@ impl ChaseVisualization {
             }
         };
 
+        let breakpoints = state
+            .chase_state
+            .as_ref()
+            .map(|s| s.breakpoints.clone())
+            .unwrap_or_default();
+
         // Now get mutable access to entry
         let entry = state.repl.instances.get_mut(&instance_name).unwrap();
 
         // Run chase to fixpoint
         let sig = &theory.theory.signature;
         let axioms = &theory.theory.axioms;
+        let axiom_names = &theory.theory.axiom_names;
 
         let start = std::time::Instant::now();
-        let result = crate::query::chase::chase_fixpoint(
+        let mut observer = GuiChaseObserver::new(&entry.slid_to_name, None, breakpoints);
+        let result = crate::query::chase::chase_fixpoint_with_observer(
             axioms,
+            axiom_names,
             &mut entry.structure,
             &mut state.repl.store.universe,
             sig,
             100,
+            &mut observer,
         );
 
+        let GuiChaseObserver {
+            events,
+            iteration: current_iteration,
+            breakpoint_hit,
+            completed_iterations,
+            ..
+        } = observer;
+
         match result {
-            Ok(iterations) => {
+            Ok(_) => {
                 let elapsed = start.elapsed();
                 if let Some(chase_state) = &mut state.chase_state {
-                    chase_state.mode = ChaseMode::Completed;
+                    chase_state.events.extend(events);
-                    chase_state.total_iterations = Some(iterations);
+                    if !chase_state.events.is_empty() {
+                        chase_state.current_event = chase_state.events.len() - 1;
                     }
+                    chase_state.current_iteration =
+                        chase_state.current_iteration.max(current_iteration);
+
+                    if let Some(iterations) = completed_iterations {
+                        chase_state.mode = ChaseMode::Completed;
+                        chase_state.current_iteration = iterations;
+                        chase_state.total_iterations = Some(iterations);
+                    } else {
+                        chase_state.mode = ChaseMode::Stepping;
+                        chase_state.total_iterations = None;
+                    }
+                }
+
+                if let Some(bp) = breakpoint_hit {
+                    state.log_info(format!("Paused at breakpoint '{}'", bp));
+                } else if let Some(iterations) = completed_iterations {
                     state.log_success(format!(
                         "Chase completed in {} iterations ({:.2}ms)",
                         iterations,
                         elapsed.as_secs_f64() * 1000.0
                     ));
                 }
+            }
             Err(e) => {
                 state.log_error(format!("Chase error: {}", e));
             }
@@ -434,8 +501,30 @@ struct GuiChaseObserver<'a> {
     events: Vec<ChaseEventRecord>,
     slid_to_name: &'a std::collections::HashMap<crate::id::Slid, String>,
     iteration: usize,
-    step_mode: bool,
+    step_budget: Option<usize>,
-    steps_remaining: usize,
+    breakpoints: HashSet<String>,
+    pending_breakpoint_hit: Option<String>,
+    breakpoint_hit: Option<String>,
+    completed_iterations: Option<usize>,
+}
+
+impl<'a> GuiChaseObserver<'a> {
+    fn new(
+        slid_to_name: &'a std::collections::HashMap<crate::id::Slid, String>,
+        step_budget: Option<usize>,
+        breakpoints: HashSet<String>,
+    ) -> Self {
+        Self {
+            events: Vec::new(),
+            slid_to_name,
+            iteration: 0,
+            step_budget,
+            breakpoints,
+            pending_breakpoint_hit: None,
+            breakpoint_hit: None,
+            completed_iterations: None,
+        }
+    }
 }
 
 impl<'a> ChaseObserver for GuiChaseObserver<'a> {
@@ -471,27 +560,176 @@ impl<'a> ChaseObserver for GuiChaseObserver<'a> {
                     binding: binding_vec,
                     changed: false, // Will be updated in AxiomFired
                 });
-
+                self.pending_breakpoint_hit = axiom_name
-                if self.step_mode {
+                    .filter(|name| self.breakpoints.iter().any(|bp| name.contains(bp)))
-                    self.steps_remaining = self.steps_remaining.saturating_sub(1);
+                    .map(str::to_string);
-                    if self.steps_remaining == 0 {
-                        ChaseControl::Stop
-                    } else {
                 ChaseControl::Continue
             }
-                } else {
+            ChaseEvent::AxiomFired {
-                    ChaseControl::Continue
+                axiom_name,
-                }
+                changed,
-            }
+                ..
-            ChaseEvent::AxiomFired { changed, .. } => {
+            } => {
                 // Update the last event with the changed status
                 if let Some(last) = self.events.last_mut() {
                     last.changed = changed;
                 }
+
+                let mut should_stop = false;
+
+                if let Some(remaining) = &mut self.step_budget {
+                    *remaining = remaining.saturating_sub(1);
+                    if *remaining == 0 {
+                        should_stop = true;
+                    }
+                }
+
+                if let Some(bp) = self.pending_breakpoint_hit.take() {
+                    self.breakpoint_hit = Some(bp);
+                    should_stop = true;
+                } else if self.breakpoint_hit.is_none() {
+                    self.breakpoint_hit = axiom_name
+                        .filter(|name| self.breakpoints.iter().any(|bp| name.contains(bp)))
+                        .map(str::to_string);
+                    should_stop |= self.breakpoint_hit.is_some();
+                }
+
+                if should_stop {
+                    ChaseControl::Stop
+                } else {
                     ChaseControl::Continue
                 }
+            }
             ChaseEvent::IterationEnd { .. } => ChaseControl::Continue,
-            ChaseEvent::ChaseComplete { .. } => ChaseControl::Continue,
+            ChaseEvent::ChaseComplete { iterations } => {
+                self.completed_iterations = Some(iterations);
+                ChaseControl::Continue
+            }
         }
     }
 }
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::core::{Context, DerivedSort, ElaboratedTheory, Formula, Sequent, Signature, Structure, Term, Theory};
+    use crate::repl::InstanceEntry;
+    use std::rc::Rc;
+
+    fn build_test_state() -> GuiState {
+        let mut state = GuiState::new();
+        let mut sig = Signature::default();
+        sig.add_sort("X".to_string());
+        sig.add_relation(
+            "leq".to_string(),
+            DerivedSort::Product(vec![
+                ("x".to_string(), DerivedSort::Base(0)),
+                ("y".to_string(), DerivedSort::Base(0)),
+            ]),
+        );
+
+        let theory = Theory {
+            name: "Preorder".to_string(),
+            signature: sig,
+            axioms: vec![Sequent {
+                context: Context {
+                    vars: vec![("x".to_string(), DerivedSort::Base(0))],
+                },
+                premise: Formula::True,
+                conclusion: Formula::Rel(
+                    0,
+                    Term::Record(vec![
+                        ("x".to_string(), Term::Var("x".to_string(), DerivedSort::Base(0))),
+                        ("y".to_string(), Term::Var("x".to_string(), DerivedSort::Base(0))),
+                    ]),
+                ),
+            }],
+            axiom_names: vec!["ax/refl".to_string()],
+        };
+
+        state.repl.theories.insert(
+            "Preorder".to_string(),
+            Rc::new(ElaboratedTheory {
+                params: vec![],
+                theory,
+            }),
+        );
+
+        let mut structure = Structure::new(1);
+        let (a, _) = structure.add_element(&mut state.repl.store.universe, 0);
+        let (b, _) = structure.add_element(&mut state.repl.store.universe, 0);
+        structure.init_relations(&[2]);
+
+        let mut entry = InstanceEntry::new(
+            structure,
+            "Preorder".to_string(),
+            "Preorder".to_string(),
+        );
+        entry.register_element("a".to_string(), a);
+        entry.register_element("b".to_string(), b);
+        state.repl.instances.insert("Chain".to_string(), entry);
+        state.start_chase("Chain");
+        state
+    }
+
+    #[test]
+    fn gui_step_executes_exactly_one_firing() {
+        let mut state = build_test_state();
+        let mut viz = ChaseVisualization::new();
+
+        viz.step_chase(&mut state);
+
+        let entry = state.repl.instances.get("Chain").unwrap();
+        assert_eq!(entry.structure.relations[0].len(), 1);
+
+        let chase_state = state.chase_state.as_ref().unwrap();
+        assert_eq!(chase_state.events.len(), 1);
+        assert_eq!(chase_state.current_iteration, 1);
+        assert_eq!(chase_state.mode, ChaseMode::Stepping);
+        assert!(chase_state.events[0].changed);
+    }
+
+    #[test]
+    fn gui_run_all_pauses_after_breakpoint_and_records_event() {
+        let mut state = build_test_state();
+        let mut viz = ChaseVisualization::new();
+        state
+            .chase_state
+            .as_mut()
+            .unwrap()
+            .breakpoints
+            .insert("refl".to_string());
+
+        viz.run_chase_to_completion(&mut state);
+
+        let entry = state.repl.instances.get("Chain").unwrap();
+        assert_eq!(entry.structure.relations[0].len(), 1);
+
+        let chase_state = state.chase_state.as_ref().unwrap();
+        assert_eq!(chase_state.events.len(), 1);
+        assert_eq!(chase_state.current_iteration, 1);
+        assert_eq!(chase_state.mode, ChaseMode::Stepping);
+    }
+
+    #[test]
+    fn gui_reset_restores_initial_structure() {
+        let mut state = build_test_state();
+        let mut viz = ChaseVisualization::new();
+
+        viz.step_chase(&mut state);
+        assert_eq!(
+            state.repl.instances.get("Chain").unwrap().structure.relations[0].len(),
+            1
+        );
+
+        viz.reset_chase(&mut state);
+
+        let entry = state.repl.instances.get("Chain").unwrap();
+        assert_eq!(entry.structure.relations[0].len(), 0);
+
+        let chase_state = state.chase_state.as_ref().unwrap();
+        assert!(chase_state.events.is_empty());
+        assert_eq!(chase_state.current_iteration, 0);
+        assert_eq!(chase_state.mode, ChaseMode::Idle);
+    }
+}

src/gui/visualizations/graph.rs

@@ -359,10 +359,45 @@ impl GraphView {
         );
 
         let rect = response.rect;
+        let pointer_delta = ui.input(|i| i.pointer.delta());
+        let pointer_pos = ui.input(|i| i.pointer.hover_pos());
+        let initial_zoom = self.zoom;
+        let initial_pan = self.pan;
+
+        let center = rect.center();
+        let hit_test_transform = |pos: egui::Pos2| -> egui::Pos2 {
+            egui::Pos2::new(
+                center.x + pos.x * initial_zoom + initial_pan.x,
+                center.y + pos.y * initial_zoom + initial_pan.y,
+            )
+        };
+
+        let node_radius = 20.0 * initial_zoom;
+        let hovered_node = if response.hovered() {
+            pointer_pos.and_then(|pointer| {
+                self.nodes.iter().find_map(|node| {
+                    let pos = self
+                        .node_positions
+                        .get(&node.id)
+                        .copied()
+                        .unwrap_or(node.position);
+                    let screen_pos = hit_test_transform(pos);
+                    let node_rect =
+                        egui::Rect::from_center_size(screen_pos, egui::Vec2::splat(node_radius * 2.0));
+                    node_rect.contains(pointer).then_some(node.id)
+                })
+            })
+        } else {
+            None
+        };
+
+        if response.drag_started() && hovered_node.is_some() {
+            self.dragged_node = hovered_node;
+        }
 
         // Handle panning
         if response.dragged() && self.dragged_node.is_none() {
-            self.pan += response.drag_delta();
+            self.pan += pointer_delta;
         }
 
         // Handle zooming with scroll
@@ -381,8 +416,6 @@ impl GraphView {
             }
         }
 
-        // Transform helper - centers (0,0) world coordinates in the view
-        let center = rect.center();
         let transform = |pos: egui::Pos2| -> egui::Pos2 {
             egui::Pos2::new(
                 center.x + pos.x * self.zoom + self.pan.x,
@@ -436,31 +469,14 @@ impl GraphView {
         }
 
         // Draw nodes
-        let node_radius = 20.0 * self.zoom;
-
         for node in &self.nodes {
             let pos = self.node_positions.get(&node.id).copied().unwrap_or(node.position);
             let screen_pos = transform(pos);
-
+            let is_hovered = hovered_node == Some(node.id);
-            // Check if node is being hovered or dragged
-            let node_rect = egui::Rect::from_center_size(
-                screen_pos,
-                egui::Vec2::splat(node_radius * 2.0),
-            );
-
-            let is_hovered = response.hovered()
-                && ui.input(|i| i.pointer.hover_pos())
-                    .map(|p| node_rect.contains(p))
-                    .unwrap_or(false);
-
-            // Handle node dragging
-            if is_hovered && response.drag_started() {
-                self.dragged_node = Some(node.id);
-            }
 
             if self.dragged_node == Some(node.id) {
                 if response.dragged() {
-                    let delta = response.drag_delta() / self.zoom;
+                    let delta = pointer_delta / self.zoom;
                     if let Some(pos) = self.node_positions.get_mut(&node.id) {
                         *pos += delta;
                     }