From 0ee89cbb5cad96c458b1f4df1b73e56b3c411006 Mon Sep 17 00:00:00 2001 From: Henrik Lissner Date: Tue, 10 Sep 2024 17:04:20 -0400 Subject: [PATCH] tweak(idris): add popup rules --- modules/lang/idris/config.el | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/modules/lang/idris/config.el b/modules/lang/idris/config.el index 9864a6ab1..8f8d3bc1b 100644 --- a/modules/lang/idris/config.el +++ b/modules/lang/idris/config.el @@ -4,7 +4,8 @@ (add-hook 'idris-mode-hook #'turn-on-idris-simple-indent) (when (modulep! +lsp) (add-hook 'idris-mode-hook #'lsp! 'append)) - (set-repl-handler! 'idris-mode 'idris-pop-to-repl) + (set-popup-rule! "^\\*idris-\\(notes\\|holes\\|info\\)" :select nil :ttl nil) + (set-repl-handler! 'idris-mode #'idris-pop-to-repl) (set-lookup-handlers! 'idris-mode :documentation #'idris-docs-at-point) (map! :localleader