Still show last compiled goal-state while `Processing file...`

[valeratrades]

When I'm writing a proof, I would love to be able to have a consistent point of reference of existing hypothesis in the scope. Currently on every justification step I have to stop, wait for the file to process, and then in 90% of cases look for a hypothesis that was already available to find its name and exact statement.

It would be so much faster to have an option (or have it be default) of seeing the previously compiled state with a small indicator of Processing file... at the bottom or to the side, which would allow to write proofs without needless interrupts.

[Julian]

I agree 100% with this FWIW, it's been on my docket to do.

[geezee]

I was able to sort of achieve this on my local installation. I'm not sure how to reflect that on the latest commit though since my local copy is at 98405ac (Jul 2024).

Anyways, to help the conversation going this is the diff:

diff --git a/lua/lean/infoview.lua b/lua/lean/infoview.lua
index a44d2ed..b40ef37 100644
--- a/lua/lean/infoview.lua
+++ b/lua/lean/infoview.lua
@@ -22,7 +22,8 @@ local options = {
   autoopen = true,
   autopause = false,
   indicators = 'auto',
-  show_processing = true,
+  show_processing = false,
+  keep_goal_while_processing = true, -- has an effect when show_processing = false
   show_no_info_message = false,
   use_widgets = true,
 
@@ -1000,6 +1001,9 @@ function Pin:__mk_data_elem(tick)
         name = 'processing-msg',
       }
     end
+    if options.keep_goal_while_processing then
+      return
+    end
     return Element:new()
   end

The downside to my solution is that the first time a file is opened the infoview is completely blank and doesn't show the "Processing File..." message.