From dc69e8a45624aac530a20d6c48b7f3f91a400d33 Mon Sep 17 00:00:00 2001 From: CJ van den Berg Date: Mon, 4 Aug 2025 10:55:33 +0200 Subject: [PATCH] feat: make hover_time configurable --- src/config.zig | 1 + src/tui/editor.zig | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/config.zig b/src/config.zig index 7436e84..f2a65e6 100644 --- a/src/config.zig +++ b/src/config.zig @@ -17,6 +17,7 @@ whitespace_mode: []const u8 = "none", inline_diagnostics: bool = true, animation_min_lag: usize = 0, //milliseconds animation_max_lag: usize = 50, //milliseconds +hover_time_ms: usize = 500, //milliseconds enable_format_on_save: bool = false, restore_last_cursor_position: bool = true, follow_cursor_on_buffer_switch: bool = false, //scroll cursor into view on buffer switch diff --git a/src/tui/editor.zig b/src/tui/editor.zig index 9fa8948..f6943c7 100644 --- a/src/tui/editor.zig +++ b/src/tui/editor.zig @@ -6159,7 +6159,7 @@ pub const EditorWidget = struct { } if (event == .init) { self.hover_mouse_event = false; - const delay_us: u64 = std.time.us_per_ms * 500; + const delay_us: u64 = std.time.us_per_ms * tui.config().hover_time_ms; self.hover_timer = tp.self_pid().delay_send_cancellable(self.editor.allocator, "editor.hover_timer", delay_us, .{"HOVER"}) catch null; } }