From c9ab60459a27c643df8f35e0fa30e379272d4ac3 Mon Sep 17 00:00:00 2001
From: Mekeor Melire <mekeor@posteo.de>
Date: Tue, 10 Dec 2024 20:26:17 +0100
Subject: [PATCH] Wrap lsp-interface invocations into eval-and-compile

This fixes the issue reported and detailedly discussed at:
https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs/topic/lsp-mode.20errors.20due.20to.20list.20!.3D.20hash-table

Also, make code fit into fill-column.
---
 lean4-fringe.el |  7 ++++---
 lean4-info.el   | 11 +++++++----
 2 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/lean4-fringe.el b/lean4-fringe.el
index 6d27aeb..e5ab9e0 100644
--- a/lean4-fringe.el
+++ b/lean4-fringe.el
@@ -26,9 +26,10 @@
 (require 'lsp-mode)
 (require 'lsp-protocol)
 
-(lsp-interface
- (lean:LeanFileProgressProcessingInfo (:range :kind) nil)
- (lean:LeanFileProgressParams (:textDocument :processing) nil))
+(eval-and-compile
+  (lsp-interface
+   (lean:LeanFileProgressProcessingInfo (:range :kind) nil)
+   (lean:LeanFileProgressParams (:textDocument :processing) nil)))
 
 (defvar-local lean4-fringe-delay-timer nil)
 
diff --git a/lean4-info.el b/lean4-info.el
index 61e3668..923cf56 100644
--- a/lean4-info.el
+++ b/lean4-info.el
@@ -72,10 +72,13 @@ The buffer is supposed to be the *Lean Goal* buffer."
    ;; current window of current buffer is selected (i.e., in focus)
    (eq (current-buffer) (window-buffer))))
 
-(lsp-interface
- (lean:PlainGoal (:goals) nil)
- (lean:PlainTermGoal (:goal) nil)
- (lean:Diagnostic (:range :fullRange :message) (:code :relatedInformation :severity :source :tags)))
+(eval-and-compile
+  (lsp-interface
+   (lean:PlainGoal (:goals) nil)
+   (lean:PlainTermGoal (:goal) nil)
+   (lean:Diagnostic
+    (:range :fullRange :message)
+    (:code :relatedInformation :severity :source :tags))))
 
 (defconst lean4-info-buffer-name "*Lean Goal*")