Merge pull request #149 from phijor/fix-loading-ro-files

Ignore failed writes when loading buffer

Author: isovector

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

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."

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