cornelis 0.2.0.0 → 0.2.0.1

raw patch · 6 files changed

+72/−3 lines, 6 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

ChangeLog.md +4/−0
cornelis.cabal +4/−1
src/Plugin.hs +1/−1
test/Hello.agda +46/−0
test/Readonly.agda +6/−0
test/TestSpec.hs +11/−1

ChangeLog.md view

@@ -1,5 +1,9 @@ # Changelog for cornelis +## v0.2.0.1 - 2024-05-17++Updated metadata for Hackage.+ ## v0.2.0.0 - 2024-04-17  The first official release, after years in the oven.

cornelis.cabal view

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           cornelis-version:        0.2.0.0+version:        0.2.0.1 description:    Please see the README on GitHub at <https://github.com/isovector/cornelis#readme> homepage:       https://github.com/isovector/cornelis#readme bug-reports:    https://github.com/isovector/cornelis/issues@@ -18,6 +18,9 @@ extra-source-files:     README.md     ChangeLog.md+data-files:+    test/Hello.agda+    test/Readonly.agda  source-repository head   type: git

src/Plugin.hs view

@@ -81,7 +81,7 @@   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/Hello.agda view

@@ -0,0 +1,46 @@+module Hello where+open import Agda.Builtin.Nat+data Bool : Set where+  true : Bool+  false : Bool++data Unit : Set where+  one : Unit++unit : Unit+unit = ?++test : Bool → Bool+test x = ?++unicodeTest₁ : Bool → Bool+unicodeTest₁ x = ?++slap : Bool → Bool+slap = λ { x → ? }++module _ where+  testIndent : Bool → Bool+  testIndent b = ?++isEven∘ : Nat → Set+isEven∘ zero = Nat+isEven∘ (suc n) = {! isEven∘ !}++copattern : Bool → Bool+copattern = ?++foo? : Bool → Bool → Set+foo? ?f = {! !}++give : Bool+give = {! true !}++elaborate : Nat+elaborate = {! 3 !}++sub₀and-super⁹ : Nat+sub₀and-super⁹ = 15++infer : Bool → Bool → Bool+infer x = {! x !}

+ test/Readonly.agda view

@@ -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 view

@@ -8,7 +8,7 @@ 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           Plugin import           Test.Hspec import           Utils+import           Lib (cornelisInit)   broken :: String -> SpecWith a -> SpecWith a@@ -26,6 +27,15 @@ 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