Add an AGENTS.md file to project

AGENTS.md

@@ -0,0 +1,146 @@
+# AGENTS.md
+
+This file provides guidance to coding agents collaborating on this repository.
+
+## Mission
+
+Geolog is a Rust codebase for geometric logic:
+
+- a parser and pretty-printer for the Geolog language,
+- an elaboration layer that turns syntax into core structures,
+- a REPL and workspace/persistence layer,
+- a chase/query/solver runtime,
+- and an optional egui GUI behind the `gui` Cargo feature.
+
+Priorities, in order:
+
+1. Semantic correctness of theories, instances, queries, and chase behavior.
+2. Clear boundaries between parsing, elaboration, core structures, REPL/workspace, and GUI code.
+3. Focused, maintainable changes with good regression coverage.
+4. Performance only after correctness and testability are preserved.
+
+## Core Rules
+
+- Use English for code, comments, docs, tests, and commit-facing text.
+- Prefer small, targeted changes over broad rewrites.
+- Fix root causes rather than layering on ad hoc workarounds.
+- Keep modules decoupled: parsing in parser/lexer, semantics in `core`/`elaborate`, runtime behavior in `repl`/`query`/`solver`, presentation in `gui`.
+- Do not introduce unnecessary global mutable state.
+- Preserve feature gating: GUI code must remain behind the `gui` feature.
+- Avoid adding dependencies unless clearly justified.
+- Add comments only when they clarify non-obvious invariants, algorithms, or semantic constraints.
+
+Quick examples:
+
+- Good: add a targeted regression test for a chase bug in an existing GUI or unit test module.
+- Good: fix a REPL/workspace bug in `src/repl.rs` or `src/store/` without refactoring unrelated parser code.
+- Bad: rewrite the AST/core boundary during a small GUI task.
+- Bad: mix GUI presentation logic into core semantic modules.
+
+## Repository Layout
+
+- `src/lib.rs`: crate entrypoint and module exports.
+- `src/ast.rs`, `src/lexer.rs`, `src/parser.rs`, `src/pretty.rs`: syntax pipeline and round-tripping.
+- `src/core.rs`: core semantic data structures such as signatures, theories, and structures.
+- `src/elaborate/`: elaboration from AST into core representations.
+- `src/repl.rs`: REPL state, command handling, and top-level execution flow.
+- `src/store/`: persistence/workspace and storage-related logic.
+- `src/query/`: chase, query compilation, optimization, backend execution.
+- `src/solver/`: solver and tactic logic.
+- `src/tensor/`: tensor-based checking/evaluation support.
+- `src/gui/`: egui GUI state, panels, and visualizations.
+- `src/bin/geolog.rs`: CLI/REPL binary.
+- `src/bin/geolog-gui.rs`: GUI binary (requires `--features gui`).
+- `examples/geolog/`: sample Geolog programs.
+- `tests/`: integration, regression, unit-style cross-module, and property tests.
+- `docs/`: architecture and syntax documentation.
+- `proofs/`: Lean proofs and formal artifacts.
+- `fuzz/`: fuzzing targets.
+
+## Architecture Constraints
+
+- Keep the syntax pipeline clean: text → lexer → parser → AST.
+- Keep elaboration separate from parsing and separate from UI code.
+- `core` types should remain usable without the GUI.
+- GUI code should orchestrate and present existing behavior, not reimplement semantic logic.
+- Workspace/persistence behavior belongs in `repl`/`store`, not inside GUI widgets.
+- Query/chase behavior changes must preserve observable semantics and existing tests.
+- If a change affects persistence or serialization, consider compatibility with existing workspace behavior.
+
+## GUI Rules
+
+- The GUI is optional and must compile cleanly only when the `gui` feature is enabled.
+- Prefer fixing GUI bugs in `src/gui/state.rs`, `src/gui/panels/`, or `src/gui/visualizations/` before touching core logic.
+- Keep GUI state transitions explicit and centralized when possible.
+- Avoid hard-coding theme assumptions; UI should remain readable in the intended visual style.
+- File dialog, editor, browser, inspector, console, and visualization behavior should stay consistent with REPL/workspace state.
+
+## Testing Layout Rules
+
+- Prefer unit tests near the code they exercise when there is already a local test module.
+- Put broader cross-module coverage in `tests/`.
+- Keep regression tests close to the bug they reproduce when that is the clearest fit.
+- Do not add a new testing framework if existing `cargo test`, property tests, or fuzz targets are sufficient.
+- If you move behavior across modules, move or rewrite the relevant tests with it.
+
+## Workflow
+
+Before coding:
+
+1. Identify whether the task is parser, elaboration, runtime, persistence, solver/query, or GUI work.
+2. Read the touched module and nearby tests first.
+3. Check whether the change should live in `core`/`repl`/`store` rather than the GUI.
+
+Implement and validate:
+
+1. Make the smallest change that solves the problem.
+2. Add or update tests when behavior changes or a bug is fixed.
+3. Run the narrowest relevant command while iterating.
+4. Run broader validation once the change is stable.
+5. Update docs if user-facing behavior or workflow changed.
+
+## Validation Commands
+
+Use the narrowest relevant command first:
+
+- General compile check: `cargo check`
+- Full test suite: `cargo test`
+- GUI compile check: `cargo check --features gui --bin geolog-gui`
+- GUI-related tests: `cargo test --features gui`
+- Single test/module during iteration: `cargo test <name>`
+
+Formatting:
+
+- Prefer formatting only touched Rust files when the repository is not already fully formatted.
+- Avoid reformatting unrelated files as part of a focused bugfix.
+
+## Testing Expectations
+
+- No semantic bugfix is complete without appropriate validation.
+- Parser/elaboration changes should preserve round-trip and error-reporting behavior where relevant.
+- Query/chase/solver changes need explicit coverage because regressions can be subtle.
+- GUI bugfixes should get a focused test when practical, especially for state transitions or regressions.
+- Keep tests deterministic and focused on observable behavior.
+
+## Documentation Expectations
+
+- Update `README.md` when user workflow, CLI behavior, or GUI usage changes.
+- Update `docs/ARCHITECTURE.md` or `docs/SYNTAX.md` when architectural or language behavior changes materially.
+- If you find stale docs directly related to your change, fix them in the same patch.
+
+## Review Guidelines
+
+Review output should be concise and focus on real defects.
+
+- `P0`: broken build, broken tests, data loss, or incorrect core semantics.
+- `P1`: likely semantic regression, unsafe state transition, missing validation on risky changes.
+
+Use this review format:
+
+1. `Severity` (`P0`/`P1`)
+2. `File:line`
+3. `Issue`
+4. `Why it matters`
+5. `Minimal fix direction`
+
+Do not include style-only feedback or broad praise.

README2.md

@@ -37,6 +37,10 @@ Usage in REPL:
 
 A full-featured graphical interface built with egui.
 
+Current design note:
+- The GUI uses a rigid docked layout rather than draggable in-window splitters.
+- This was done to reduce hover/drag-induced layout jitter and keep the workspace visually stable.
+
 #### Building the GUI
 
 ```bash

src/bin/geolog-gui.rs

@@ -114,22 +114,18 @@ 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),
-    );
-    style.text_styles.insert(
-        egui::TextStyle::Heading,
-        egui::FontId::proportional(18.0),
-    );
-    style.text_styles.insert(
-        egui::TextStyle::Monospace,
-        egui::FontId::monospace(13.0),
-    );
+    style
+        .text_styles
+        .insert(egui::TextStyle::Body, egui::FontId::proportional(14.0));
+    style
+        .text_styles
+        .insert(egui::TextStyle::Heading, egui::FontId::proportional(18.0));
+    style
+        .text_styles
+        .insert(egui::TextStyle::Monospace, egui::FontId::monospace(13.0));
 
-    // Set up dark theme with custom colors
-    style.visuals = egui::Visuals::dark();
-    style.visuals.override_text_color = Some(egui::Color32::from_gray(220));
+    // Force a light theme for the GUI.
+    style.visuals = egui::Visuals::light();
     style.visuals.widgets.noninteractive.expansion = 0.0;
     style.visuals.widgets.inactive.expansion = 0.0;
     style.visuals.widgets.hovered.expansion = 0.0;

src/gui/app.rs

@@ -46,21 +46,21 @@ impl GeologApp {
 
     /// Render the menu bar
     fn menu_bar(&mut self, ui: &mut egui::Ui) {
-        egui::menu::bar(ui, |ui| {
+        egui::MenuBar::new().ui(ui, |ui| {
             ui.menu_button("File", |ui| {
                 if ui.button("Open...").clicked() {
                     self.handle_open_file();
-                    ui.close_menu();
+                    ui.close();
                 }
                 if ui.button("Save").clicked() {
                     self.handle_save_file();
-                    ui.close_menu();
+                    ui.close();
                 }
                 ui.separator();
                 if ui.button("Reset State").clicked() {
-                    self.state.repl.reset();
+                    self.state.reset_runtime_state();
                     self.state.log_info("State reset");
-                    ui.close_menu();
+                    ui.close();
                 }
                 ui.separator();
                 if ui.button("Quit").clicked() {
@@ -71,11 +71,11 @@ impl GeologApp {
             ui.menu_button("Edit", |ui| {
                 if ui.button("Clear Editor").clicked() {
                     self.state.editor_content.clear();
-                    ui.close_menu();
+                    ui.close();
                 }
                 if ui.button("Clear Console").clicked() {
                     self.state.clear_console();
-                    ui.close_menu();
+                    ui.close();
                 }
             });
 
@@ -88,7 +88,7 @@ impl GeologApp {
                     .clicked()
                 {
                     self.state.central_view = CentralView::EditorAndInspector;
-                    ui.close_menu();
+                    ui.close();
                 }
                 if ui
                     .selectable_label(
@@ -98,7 +98,7 @@ impl GeologApp {
                     .clicked()
                 {
                     self.state.central_view = CentralView::ChaseVisualization;
-                    ui.close_menu();
+                    ui.close();
                 }
                 if ui
                     .selectable_label(
@@ -108,7 +108,7 @@ impl GeologApp {
                     .clicked()
                 {
                     self.state.central_view = CentralView::GraphVisualization;
-                    ui.close_menu();
+                    ui.close();
                 }
             });
 
@@ -119,11 +119,11 @@ impl GeologApp {
                     let name = name.clone();
                     if ui.button(format!("Run Chase on {}", name)).clicked() {
                         self.handle_run_chase(&name);
-                        ui.close_menu();
+                        ui.close();
                     }
                     if ui.button(format!("Debug Chase on {}", name)).clicked() {
                         self.state.start_chase(&name);
-                        ui.close_menu();
+                        ui.close();
                     }
                 } else {
                     ui.label("(Select an instance first)");
@@ -132,15 +132,13 @@ impl GeologApp {
 
             ui.menu_button("Help", |ui| {
                 if ui.button("About").clicked() {
-                    self.state.log_info(format!(
-                        "Geolog GUI v{}",
-                        env!("CARGO_PKG_VERSION")
-                    ));
-                    ui.close_menu();
+                    self.state
+                        .log_info(format!("Geolog GUI v{}", env!("CARGO_PKG_VERSION")));
+                    ui.close();
                 }
                 if ui.button("Syntax Help").clicked() {
                     self.show_syntax_help();
-                    ui.close_menu();
+                    ui.close();
                 }
             });
         });
@@ -148,7 +146,7 @@ impl GeologApp {
 
     /// Handle opening a file
     fn handle_open_file(&mut self) {
-        if let Some(path) = rfd::FileDialog::new()
+        if let Some(path) = Self::new_file_dialog()
             .add_filter("Geolog", &["geolog"])
             .add_filter("All Files", &["*"])
             .pick_file()
@@ -170,7 +168,7 @@ impl GeologApp {
             }
         } else {
             // Save As
-            if let Some(path) = rfd::FileDialog::new()
+            if let Some(path) = Self::new_file_dialog()
                 .add_filter("Geolog", &["geolog"])
                 .save_file()
             {
@@ -187,6 +185,14 @@ impl GeologApp {
         }
     }
 
+    fn new_file_dialog() -> rfd::FileDialog {
+        let dialog = rfd::FileDialog::new();
+        match std::env::current_dir() {
+            Ok(dir) => dialog.set_directory(dir),
+            Err(_) => dialog,
+        }
+    }
+
     /// Run chase on an instance
     fn handle_run_chase(&mut self, instance_name: &str) {
         use crate::core::RelationStorage;
@@ -242,8 +248,7 @@ impl GeologApp {
             Ok(iterations) => {
                 let elapsed = start.elapsed();
                 // Get structure info before releasing borrow
-                let total_tuples: usize =
-                    entry.structure.relations.iter().map(|r| r.len()).sum();
+                let total_tuples: usize = entry.structure.relations.iter().map(|r| r.len()).sum();
                 let num_elements = entry.structure.len();
 
                 self.state.log_success(format!(
@@ -255,8 +260,7 @@ impl GeologApp {
                 // Show structure summary
                 self.state.log_info(format!(
                     "Structure: {} elements, {} relation tuples",
-                    num_elements,
-                    total_tuples
+                    num_elements, total_tuples
                 ));
             }
             Err(e) => {

src/gui/panels/browser.rs

@@ -147,7 +147,7 @@ impl BrowserPanel {
                             if ui.button("Inspect").clicked() {
                                 state.selected_item =
                                     Some(SelectedItem::Instance(instance.name.clone()));
-                                ui.close_menu();
+                                ui.close();
                             }
                             if ui.button("Run Chase").clicked() {
                                 // This will be handled by the app
@@ -157,11 +157,11 @@ impl BrowserPanel {
                                     "Use Chase menu to run chase on '{}'",
                                     instance.name
                                 ));
-                                ui.close_menu();
+                                ui.close();
                             }
                             if ui.button("View Graph").clicked() {
                                 state.show_graph(&instance.name, None);
-                                ui.close_menu();
+                                ui.close();
                             }
                         });
                     }

src/gui/panels/console.rs

@@ -6,7 +6,7 @@ use eframe::egui;
 use egui_extras::{Size, StripBuilder};
 
 use crate::gui::state::{GuiState, MessageKind};
-use crate::repl::{MetaCommand, ListTarget, ExecuteResult};
+use crate::repl::{ExecuteResult, ListTarget, MetaCommand};
 
 /// Console panel for output messages and REPL input
 pub struct ConsolePanel {
@@ -73,12 +73,7 @@ impl ConsolePanel {
                                         ui.label("Type commands below (e.g., :help, :list, or geolog code)");
                                     } else {
                                         for message in &state.console_messages {
-                                            let color = match message.kind {
-                                                MessageKind::Info => egui::Color32::LIGHT_GRAY,
-                                                MessageKind::Success => egui::Color32::from_rgb(100, 200, 100),
-                                                MessageKind::Error => egui::Color32::from_rgb(255, 100, 100),
-                                                MessageKind::Warning => egui::Color32::from_rgb(255, 200, 100),
-                                            };
+                                            let color = message_color(ui, message.kind);
 
                                             let prefix = match message.kind {
                                                 MessageKind::Info => ">",
@@ -115,7 +110,7 @@ impl ConsolePanel {
                             egui::Label::new(
                                 egui::RichText::new("geolog>")
                                     .monospace()
-                                    .color(egui::Color32::from_rgb(100, 150, 255)),
+                                    .color(ui.visuals().hyperlink_color),
                             ),
                         );
 
@@ -231,8 +226,7 @@ impl ConsolePanel {
 
     fn handle_meta_command(&mut self, state: &mut GuiState, cmd: MetaCommand) {
         match cmd {
-            MetaCommand::Help(topic) => {
-                match topic.as_deref() {
+            MetaCommand::Help(topic) => match topic.as_deref() {
                 None => {
                     state.log_info("Commands:");
                     state.log_info("  :help          Show this help");
@@ -247,8 +241,7 @@ impl ConsolePanel {
                 Some(t) => {
                     state.log_info(format!("Help topic: {}", t));
                 }
-                }
-            }
+            },
             MetaCommand::List(target) => {
                 match target {
                     ListTarget::Theories | ListTarget::All => {
@@ -286,7 +279,7 @@ impl ConsolePanel {
                 }
             }
             MetaCommand::Inspect(name) => {
-                use crate::repl::{InspectResult, format_theory_detail, format_instance_detail};
+                use crate::repl::{format_instance_detail, format_theory_detail, InspectResult};
                 match state.repl.inspect(&name) {
                     Some(InspectResult::Theory(detail)) => {
                         for line in format_theory_detail(&detail).lines() {
@@ -307,15 +300,16 @@ impl ConsolePanel {
                 state.clear_console();
             }
             MetaCommand::Reset => {
-                state.repl.reset();
-                state.selected_item = None;
+                state.reset_runtime_state();
                 state.log_success("State reset.");
             }
-            MetaCommand::Chase { instance, max_iterations } => {
+            MetaCommand::Chase {
+                instance,
+                max_iterations,
+            } => {
                 self.run_chase(state, &instance, max_iterations);
             }
-            MetaCommand::Source(path) => {
-                match std::fs::read_to_string(&path) {
+            MetaCommand::Source(path) => match std::fs::read_to_string(&path) {
                 Ok(content) => {
                     state.editor_content = content;
                     state.current_file = Some(path.clone());
@@ -325,8 +319,7 @@ impl ConsolePanel {
                 Err(e) => {
                     state.log_error(format!("Failed to load: {}", e));
                 }
-                }
-            }
+            },
             _ => {
                 state.log_warning("Command not yet implemented in GUI");
             }
@@ -361,7 +354,11 @@ impl ConsolePanel {
             return;
         }
 
-        state.log_info(format!("Running chase on '{}' ({} axioms)...", instance_name, axioms.len()));
+        state.log_info(format!(
+            "Running chase on '{}' ({} axioms)...",
+            instance_name,
+            axioms.len()
+        ));
 
         let entry = state.repl.instances.get_mut(instance_name).unwrap();
         let max_iter = max_iterations.unwrap_or(100);
@@ -389,8 +386,7 @@ impl ConsolePanel {
                 ));
                 state.log_info(format!(
                     "Structure: {} elements, {} relation tuples",
-                    num_elements,
-                    total_tuples
+                    num_elements, total_tuples
                 ));
             }
             Err(e) => {
@@ -432,6 +428,15 @@ impl ConsolePanel {
     }
 }
 
+fn message_color(ui: &egui::Ui, kind: MessageKind) -> egui::Color32 {
+    match kind {
+        MessageKind::Info => ui.visuals().text_color(),
+        MessageKind::Success => egui::Color32::from_rgb(25, 110, 55),
+        MessageKind::Error => egui::Color32::from_rgb(170, 30, 45),
+        MessageKind::Warning => egui::Color32::from_rgb(145, 95, 15),
+    }
+}
+
 impl Default for ConsolePanel {
     fn default() -> Self {
         Self::new()

src/gui/state.rs

@@ -179,6 +179,16 @@ impl GuiState {
         }
     }
 
+    /// Reset the loaded theories/instances and clear any stale GUI selections.
+    pub fn reset_runtime_state(&mut self) {
+        self.repl.reset();
+        self.selected_item = None;
+        self.chase_state = None;
+        self.graph_instance = None;
+        self.graph_relation = None;
+        self.central_view = CentralView::EditorAndInspector;
+    }
+
     /// Add an info message to the console
     pub fn log_info(&mut self, text: impl Into<String>) {
         self.console_messages.push(ConsoleMessage {
@@ -330,3 +340,30 @@ impl GuiState {
         self.central_view = CentralView::GraphVisualization;
     }
 }
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn reset_runtime_state_clears_gui_navigation_state() {
+        let mut state = GuiState::new();
+        state.selected_item = Some(SelectedItem::Theory("Demo".into()));
+        state.chase_state = Some(ChaseVisualizationState::new("I".into(), Structure::new(0)));
+        state.graph_instance = Some("I".into());
+        state.graph_relation = Some("R".into());
+        state.central_view = CentralView::GraphVisualization;
+        state.editor_content = "theory Demo {}".into();
+        state.current_file = Some(PathBuf::from("demo.geolog"));
+
+        state.reset_runtime_state();
+
+        assert!(state.selected_item.is_none());
+        assert!(state.chase_state.is_none());
+        assert!(state.graph_instance.is_none());
+        assert!(state.graph_relation.is_none());
+        assert_eq!(state.central_view, CentralView::EditorAndInspector);
+        assert_eq!(state.editor_content, "theory Demo {}");
+        assert_eq!(state.current_file, Some(PathBuf::from("demo.geolog")));
+    }
+}

src/gui/visualizations/chase.rs

@@ -6,7 +6,9 @@ use eframe::egui;
 use std::collections::HashSet;
 
 use crate::core::RelationStorage;
-use crate::gui::state::{ChaseEventRecord, ChaseMode, ChaseVisualizationState, CentralView, GuiState, SelectedItem};
+use crate::gui::state::{
+    CentralView, ChaseEventRecord, ChaseMode, ChaseVisualizationState, GuiState, SelectedItem,
+};
 use crate::query::chase::{ChaseControl, ChaseEvent, ChaseObserver};
 
 /// Chase visualization panel
@@ -50,7 +52,10 @@ impl ChaseVisualization {
             ui.label("No instances defined. Create an instance first.");
         } else {
             for instance in instances {
-                if ui.button(format!("{} : {}", instance.name, instance.theory_name)).clicked() {
+                if ui
+                    .button(format!("{} : {}", instance.name, instance.theory_name))
+                    .clicked()
+                {
                     state.start_chase(&instance.name);
                 }
             }
@@ -60,7 +65,10 @@ impl ChaseVisualization {
         if let Some(SelectedItem::Instance(name)) = &state.selected_item {
             ui.add_space(16.0);
             let name = name.clone();
-            if ui.button(format!("Start Chase on selected: {}", name)).clicked() {
+            if ui
+                .button(format!("Start Chase on selected: {}", name))
+                .clicked()
+            {
                 state.start_chase(&name);
             }
         }
@@ -186,11 +194,11 @@ impl ChaseVisualization {
                             );
 
                             let color = if is_current {
-                                egui::Color32::YELLOW
+                                ui.visuals().hyperlink_color
                             } else if event.changed {
-                                egui::Color32::from_rgb(100, 200, 100)
+                                egui::Color32::from_rgb(25, 110, 55)
                             } else {
-                                egui::Color32::LIGHT_GRAY
+                                ui.visuals().weak_text_color()
                             };
 
                             ui.label(egui::RichText::new(text).color(color).monospace());
@@ -612,7 +620,10 @@ impl<'a> ChaseObserver for GuiChaseObserver<'a> {
 #[cfg(test)]
 mod tests {
     use super::*;
-    use crate::core::{Context, DerivedSort, ElaboratedTheory, Formula, Sequent, Signature, Structure, Term, Theory};
+    use crate::core::{
+        Context, DerivedSort, ElaboratedTheory, Formula, Sequent, Signature, Structure, Term,
+        Theory,
+    };
     use crate::repl::InstanceEntry;
     use std::rc::Rc;
 
@@ -639,8 +650,14 @@ mod tests {
                 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))),
+                        (
+                            "x".to_string(),
+                            Term::Var("x".to_string(), DerivedSort::Base(0)),
+                        ),
+                        (
+                            "y".to_string(),
+                            Term::Var("x".to_string(), DerivedSort::Base(0)),
+                        ),
                     ]),
                 ),
             }],
@@ -660,11 +677,8 @@ mod tests {
         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(),
-        );
+        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);
@@ -718,7 +732,14 @@ mod tests {
 
         viz.step_chase(&mut state);
         assert_eq!(
-            state.repl.instances.get("Chain").unwrap().structure.relations[0].len(),
+            state
+                .repl
+                .instances
+                .get("Chain")
+                .unwrap()
+                .structure
+                .relations[0]
+                .len(),
             1
         );
 

src/gui/visualizations/graph.rs

@@ -83,7 +83,8 @@ impl GraphView {
         ui.separator();
 
         // Check if we need to rebuild the graph
-        if state.graph_instance != self.last_instance || state.graph_relation != self.last_relation {
+        if state.graph_instance != self.last_instance || state.graph_relation != self.last_relation
+        {
             self.rebuild_graph(state);
         }
 
@@ -109,21 +110,23 @@ impl GraphView {
 
                         ui.label("Relation:");
                         egui::ComboBox::from_label("")
-                            .selected_text(
-                                self.selected_relation
-                                    .as_deref()
-                                    .unwrap_or("(all)"),
-                            )
+                            .selected_text(self.selected_relation.as_deref().unwrap_or("(all)"))
                             .show_ui(ui, |ui| {
-                                if ui.selectable_label(self.selected_relation.is_none(), "(all)").clicked() {
+                                if ui
+                                    .selectable_label(self.selected_relation.is_none(), "(all)")
+                                    .clicked()
+                                {
                                     self.selected_relation = None;
                                     self.needs_layout = true;
                                 }
                                 for rel in relations {
-                                    if ui.selectable_label(
+                                    if ui
+                                        .selectable_label(
                                             self.selected_relation.as_deref() == Some(rel),
                                             rel,
-                                    ).clicked() {
+                                        )
+                                        .clicked()
+                                    {
                                         self.selected_relation = Some(rel.to_string());
                                         self.needs_layout = true;
                                     }
@@ -183,7 +186,10 @@ impl GraphView {
             ui.label("No instances defined.");
         } else {
             for instance in instances {
-                if ui.button(format!("{} : {}", instance.name, instance.theory_name)).clicked() {
+                if ui
+                    .button(format!("{} : {}", instance.name, instance.theory_name))
+                    .clicked()
+                {
                     state.graph_instance = Some(instance.name.clone());
                     self.needs_layout = true;
                 }
@@ -230,7 +236,10 @@ impl GraphView {
                 .unwrap_or_else(|| format!("#{}", slid_idx));
 
             let sort_name = sig.sorts.get(sort_id).cloned().unwrap_or_default();
-            let color = sort_colors.get(sort_id).copied().unwrap_or(egui::Color32::GRAY);
+            let color = sort_colors
+                .get(sort_id)
+                .copied()
+                .unwrap_or(egui::Color32::GRAY);
 
             self.nodes.push(GraphNode {
                 id: slid,
@@ -326,7 +335,11 @@ impl GraphView {
         let mut max_y = f32::MIN;
 
         for node in &self.nodes {
-            let pos = self.node_positions.get(&node.id).copied().unwrap_or(node.position);
+            let pos = self
+                .node_positions
+                .get(&node.id)
+                .copied()
+                .unwrap_or(node.position);
             min_x = min_x.min(pos.x);
             min_y = min_y.min(pos.y);
             max_x = max_x.max(pos.x);
@@ -346,17 +359,15 @@ impl GraphView {
         // Reset pan to center the content (since our world origin is already at center)
         let world_center_x = (min_x + max_x) / 2.0;
         let world_center_y = (min_y + max_y) / 2.0;
-        self.pan = egui::Vec2::new(
-            -world_center_x * self.zoom,
-            -world_center_y * self.zoom,
-        );
+        self.pan = egui::Vec2::new(-world_center_x * self.zoom, -world_center_y * self.zoom);
     }
 
     fn draw_graph(&mut self, ui: &mut egui::Ui) {
-        let (response, painter) = ui.allocate_painter(
-            ui.available_size(),
-            egui::Sense::click_and_drag(),
-        );
+        let (response, painter) =
+            ui.allocate_painter(ui.available_size(), egui::Sense::click_and_drag());
+        let edge_color = ui.visuals().weak_text_color();
+        let border_color = ui.visuals().text_color();
+        let hint_color = ui.visuals().weak_text_color();
 
         let rect = response.rect;
         let pointer_delta = ui.input(|i| i.pointer.delta());
@@ -382,8 +393,10 @@ impl GraphView {
                         .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));
+                    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)
                 })
             })
@@ -439,14 +452,12 @@ impl GraphView {
                     painter.circle_stroke(
                         loop_center,
                         10.0 * self.zoom,
-                        egui::Stroke::new(1.5, egui::Color32::LIGHT_GRAY),
+                        egui::Stroke::new(1.5, edge_color),
                     );
                 } else {
                     // Regular edge
-                    painter.line_segment(
-                        [from_screen, to_screen],
-                        egui::Stroke::new(1.5, egui::Color32::LIGHT_GRAY),
-                    );
+                    painter
+                        .line_segment([from_screen, to_screen], egui::Stroke::new(1.5, edge_color));
 
                     // Draw arrowhead
                     let dir = (to_screen - from_screen).normalized();
@@ -461,7 +472,7 @@ impl GraphView {
 
                     painter.add(egui::Shape::convex_polygon(
                         vec![p1, p2, p3],
-                        egui::Color32::LIGHT_GRAY,
+                        edge_color,
                         egui::Stroke::NONE,
                     ));
                 }
@@ -470,7 +481,11 @@ impl GraphView {
 
         // Draw nodes
         for node in &self.nodes {
-            let pos = self.node_positions.get(&node.id).copied().unwrap_or(node.position);
+            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);
 
@@ -497,7 +512,7 @@ impl GraphView {
             painter.circle_stroke(
                 screen_pos,
                 node_radius,
-                egui::Stroke::new(2.0, egui::Color32::WHITE),
+                egui::Stroke::new(2.0, border_color),
             );
 
             // Draw node label
@@ -507,7 +522,7 @@ impl GraphView {
                 egui::Align2::CENTER_CENTER,
                 &node.name,
                 egui::FontId::proportional(font_size),
-                egui::Color32::WHITE,
+                text_color_for_fill(fill_color),
             );
 
             // Draw sort label below
@@ -517,7 +532,7 @@ impl GraphView {
                     egui::Align2::CENTER_TOP,
                     &node.sort,
                     egui::FontId::proportional(10.0 * self.zoom),
-                    egui::Color32::LIGHT_GRAY,
+                    hint_color,
                 );
             }
         }
@@ -529,7 +544,7 @@ impl GraphView {
                 egui::Align2::CENTER_CENTER,
                 "No elements to display",
                 egui::FontId::proportional(16.0),
-                egui::Color32::GRAY,
+                hint_color,
             );
         }
     }
@@ -554,6 +569,16 @@ fn generate_sort_colors(count: usize) -> Vec<egui::Color32> {
     colors
 }
 
+fn text_color_for_fill(fill: egui::Color32) -> egui::Color32 {
+    let luminance =
+        (0.2126 * fill.r() as f32 + 0.7152 * fill.g() as f32 + 0.0722 * fill.b() as f32) / 255.0;
+    if luminance > 0.6 {
+        egui::Color32::BLACK
+    } else {
+        egui::Color32::WHITE
+    }
+}
+
 /// Convert HSV to RGB
 fn hsv_to_rgb(h: f32, s: f32, v: f32) -> (u8, u8, u8) {
     let c = v * s;