Skip to content

Commit

Permalink
Merge pull request #149 from phijor/fix-loading-ro-files
Browse files Browse the repository at this point in the history
Ignore failed writes when loading buffer
  • Loading branch information
isovector authored May 15, 2024
2 parents c97b481 + 60fa86a commit 5fb7f1d
Show file tree
Hide file tree
Showing 3 changed files with 18 additions and 2 deletions.
2 changes: 1 addition & 1 deletion src/Plugin.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 6 additions & 0 deletions test/Readonly.agda
Original file line number Diff line number Diff line change
@@ -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."
12 changes: 11 additions & 1 deletion test/TestSpec.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -18,6 +18,7 @@ import Neovim.Test
import Plugin
import Test.Hspec
import Utils
import Lib (cornelisInit)


broken :: String -> SpecWith a -> SpecWith a
Expand All @@ -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
Expand Down

0 comments on commit 5fb7f1d

Please sign in to comment.