From 60fa86a4f8dd743367156fa9b80fd4986dc89d65 Mon Sep 17 00:00:00 2001
From: Philipp Joram <mail@phijor.me>
Date: Tue, 14 May 2024 18:59:05 +0300
Subject: [PATCH] Ignore failed writes when loading buffer

Previously, loading buffers of read-only files wasn't possible, as
cornelis would try to write the file before loading (which would fail
and abort the command).

Add `silent` to the command to ignore failed writes.  This should be
a safe fallback.

Fixes #116.
---
 src/Plugin.hs      |  2 +-
 test/Readonly.agda |  6 ++++++
 test/TestSpec.hs   | 12 +++++++++++-
 3 files changed, 18 insertions(+), 2 deletions(-)
 create mode 100644 test/Readonly.agda

diff --git a/src/Plugin.hs b/src/Plugin.hs
index 6c2b907..798d169 100644
--- a/src/Plugin.hs
+++ b/src/Plugin.hs
@@ -81,7 +81,7 @@ load = withAgda $ withCurrentBuffer $ \b -> do
   agda <- getAgda b
   ready <- liftIO $ readIORef $ a_ready agda
   if ready then do
-    vim_command "noautocmd w"
+    vim_command "silent! noautocmd w"
     name <- buffer_get_name $ a_buffer agda
     flip runIOTCM agda $ Cmd_load name []
     buffer_get_number b >>= resetDiff
diff --git a/test/Readonly.agda b/test/Readonly.agda
new file mode 100644
index 0000000..57c2950
--- /dev/null
+++ b/test/Readonly.agda
@@ -0,0 +1,6 @@
+module Readonly where
+
+open import Agda.Builtin.String
+
+description : String
+description = "This is a read-only file. Loading it should work fine."
diff --git a/test/TestSpec.hs b/test/TestSpec.hs
index 660646e..c925f3d 100644
--- a/test/TestSpec.hs
+++ b/test/TestSpec.hs
@@ -8,7 +8,7 @@ import           Control.Monad (void)
 import           Cornelis.Subscripts (decNextDigitSeq, incNextDigitSeq)
 import           Cornelis.Types
 import           Cornelis.Types.Agda (Rewrite (..))
-import           Cornelis.Utils (withBufferStuff)
+import           Cornelis.Utils (withBufferStuff, withLocalEnv)
 import           Cornelis.Vim
 import qualified Data.Text as T
 import qualified Data.Vector as V
@@ -18,6 +18,7 @@ import           Neovim.Test
 import           Plugin
 import           Test.Hspec
 import           Utils
+import           Lib (cornelisInit)
 
 
 broken :: String -> SpecWith a -> SpecWith a
@@ -26,6 +27,15 @@ broken = before_ . pendingWith
 spec :: Spec
 spec = focus $ do
   let timeout = Seconds 60
+
+  it "should load read-only file" $ do
+    withVim timeout $ \w b -> do
+      env <- cornelisInit
+      withLocalEnv env $ do
+        vim_command "view test/Readonly.agda"
+        liftIO $ threadDelay 1e6
+        load
+
   diffSpec "should refine" timeout "test/Hello.agda"
       [ Swap "unit = ?" "unit = one"] $ \w _ -> do
     goto w 11 8