Agda 2.5.4 → 2.5.4.1
raw patch · 8 files changed
+46/−512 lines, 8 filessetup-changedPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- Agda.cabal +3/−2
- CHANGELOG.md +17/−0
- Setup.hs +12/−14
- dist/build/Agda/Syntax/Parser/Parser.hs +1/−373
- doc/user-manual.pdf binary
- src/data/emacs-mode/agda2-mode-pkg.el +1/−1
- src/data/emacs-mode/agda2-mode.el +11/−78
- stack-8.4.3.yaml +1/−44
Agda.cabal view
@@ -1,5 +1,5 @@ name: Agda-version: 2.5.4+version: 2.5.4.1 cabal-version: >= 1.10 build-type: Custom license: OtherLicense@@ -83,7 +83,7 @@ source-repository this type: git location: https://github.com/agda/agda.git- tag: v2.5.4+ tag: v2.5.4.1 flag cpphs default: True@@ -106,6 +106,7 @@ setup-depends: base >= 4.8.0.0 && < 4.12 , Cabal >= 1.22.5.0 && < 2.3 , filepath >= 1.4.0.0 && < 1.5+ , filemanip >= 0.3.6.2 && < 0.4 , process >= 1.2.3.0 && < 1.7 library
CHANGELOG.md view
@@ -1,3 +1,20 @@+Release notes for Agda version 2.5.4.1+======================================++Installation and infrastructure+-------------------------------++* Generated the interface file for the `Sigma.agda` built-in when+ installing Agda+ [Issue [#3128](https://github.com/agda/agda/issues/3128)].++Emacs mode+----------++* Light highlighting is no longer applied continuously, but only when+ the file is saved [Issue+ [#3119](https://github.com/agda/agda/issues/3119)].+ Release notes for Agda version 2.5.4 ====================================
Setup.hs view
@@ -1,11 +1,11 @@ -import Data.List import Distribution.Simple import Distribution.Simple.LocalBuildInfo import Distribution.Simple.Setup import Distribution.Simple.BuildPaths (exeExtension) import Distribution.PackageDescription import System.FilePath+import System.FilePath.Find import System.Process import System.Exit @@ -13,29 +13,27 @@ hooks = simpleUserHooks { regHook = checkAgdaPrimitiveAndRegister } -builtins :: [String]-builtins =- [ "Bool", "Char", "Coinduction", "Equality", "Float"- , "FromNat", "FromNeg", "FromString", "IO", "Int", "List"- , "Nat", "Reflection", "Size", "Strict", "String"- , "TrustMe", "Unit", "Word" ]+builtins :: FilePath -> IO [FilePath]+builtins = find always (extension ==? ".agda") checkAgdaPrimitive :: PackageDescription -> LocalBuildInfo -> RegisterFlags -> IO () checkAgdaPrimitive pkg info flags | regGenPkgConf flags /= NoFlag = return () -- Gets run twice, only do this the second time checkAgdaPrimitive pkg info flags = do- let dirs = absoluteInstallDirs pkg info NoCopyDest- agda = buildDir info </> "agda" </> "agda" <.> exeExtension- primMod ms = (ms, datadir dirs </> "lib" </> "prim" </> "Agda" </> foldr1 (</>) ms <.> "agda")- prims = primMod ["Primitive"] : [ primMod ["Builtin", m] | m <- builtins ]+ let dirs = absoluteInstallDirs pkg info NoCopyDest+ agda = buildDir info </> "agda" </> "agda" <.> exeExtension+ auxDir = datadir dirs </> "lib" </> "prim" </> "Agda"+ prim = auxDir </> "Primitive" <.> "agda" - checkPrim (ms, file) = do+ checkPrim file = do ok <- rawSystem agda [file, "-v0"] case ok of ExitSuccess -> return ()- ExitFailure _ -> putStrLn $ "WARNING: Failed to typecheck " ++ intercalate "." ("Agda" : ms) ++ "!"+ ExitFailure _ -> putStrLn $ "WARNING: Failed to typecheck " ++ file ++ "!" putStrLn "Generating Agda library interface files..."- mapM_ checkPrim prims+ checkPrim prim+ auxBuiltins <- builtins (auxDir </> "Builtins")+ mapM_ checkPrim auxBuiltins checkAgdaPrimitiveAndRegister :: PackageDescription -> LocalBuildInfo -> UserHooks -> RegisterFlags -> IO () checkAgdaPrimitiveAndRegister pkg info hooks flags = do
dist/build/Agda/Syntax/Parser/Parser.hs view
@@ -7529,379 +7529,7 @@ {-# LINE 10 "<command-line>" #-}-{-# LINE 1 "/tmp/ghc16748_0/ghc_2.h" #-}------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+{-# LINE 1 "/tmp/ghc8142_0/ghc_2.h" #-}
doc/user-manual.pdf view
binary file changed (647010 → 645013 bytes)
src/data/emacs-mode/agda2-mode-pkg.el view
@@ -1,2 +1,2 @@-(define-package "agda2-mode" "2.5.4"+(define-package "agda2-mode" "2.5.4.1" "interactive development for Agda, a dependently typed functional programming language")
src/data/emacs-mode/agda2-mode.el view
@@ -10,7 +10,7 @@ ;;; Code: -(defvar agda2-version "2.5.4"+(defvar agda2-version "2.5.4.1" "The version of the Agda mode. Note that the same version of the Agda executable must be used.") @@ -185,19 +185,6 @@ (if (and (equal agda2-fontset-name "fontset-agda2") window-system) (create-fontset-from-fontset-spec agda2-fontset-spec-of-fontset-agda2 t t)) -(defcustom agda2-highlight-after-inactivity-interval 0.2- "Highlight the buffer when Emacs has been idle for the given time.-After the last modification of the buffer. Only token-based-highlighting is performed. Highlighting is only performed if the-buffer is (marked as being) modified, the Agda process is not-busy, and `agda2-highlight-level' is not `none'."- :group 'agda2-highlight- :type '(choice (const :tag "Turn off this feature" nil)- (restricted-sexp- :tag "Seconds"- :match-alternatives ((lambda (n)- (and (numberp n) (>= n 0)))))))- ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;; Global and buffer-local vars, initialization @@ -395,10 +382,6 @@ "Was `agda2-file-buffer' active when `agda2-output-filter' started? Note that this variable is not buffer-local.") -(defvar agda2-highlight-after-inactivity-timer nil- "Timer used to update token-based highlighting after inactivity.")-(make-variable-buffer-local 'agda2-highlight-after-inactivity-timer)- ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;; agda2-mode @@ -447,7 +430,7 @@ (error (error "Unable to change the font; change agda2-fontset-name or tweak agda2-fontset-spec-of-fontset-agda2")))) ;; Deactivate highlighting if the buffer is edited before ;; typechecking is complete.- (add-hook 'after-change-functions 'agda2-abort-highlighting nil 'local)+ (add-hook 'first-change-hook 'agda2-abort-highlighting nil 'local) ;; If Agda is not running syntax highlighting does not work properly. (unless (eq 'run (agda2-process-status)) (agda2-restart))@@ -759,9 +742,9 @@ (unless agda2-in-progress (setq agda2-highlight-in-progress nil))) -(defun agda2-abort-highlighting (beg end len)+(defun agda2-abort-highlighting nil "Abort any interactive highlighting.-This function should be used in `after-change-functions'."+This function should be used in `first-change-hook'." (when agda2-highlight-in-progress (setq agda2-highlight-in-progress nil) (message "\"%s\" has been modified. Interrupting highlighting."@@ -1228,11 +1211,7 @@ (defun agda2-quit () "Quit and clean up after agda2." (interactive)- (when (timerp agda2-highlight-after-inactivity-timer)- (cancel-timer agda2-highlight-after-inactivity-timer))- (remove-hook 'after-change-functions- 'agda2-highlight-after-inactivity 'local)- (remove-hook 'after-change-functions 'agda2-abort-highlighting 'local)+ (remove-hook 'first-change-hook 'agda2-abort-highlighting 'local) (remove-hook 'after-save-hook 'agda2-highlight-tokens 'local) (agda2-remove-annotations) (agda2-term))@@ -1859,12 +1838,8 @@ ;; things). Syntax table setup for comments is done elsewhere. (set (make-local-variable 'comment-use-syntax) t) - ;; Update token-based highlighting after the buffer has been saved- ;; and after Emacs has been idle for a certain amount of time (and- ;; the buffer has been modified).+ ;; Update token-based highlighting after the buffer has been saved. (add-hook 'after-save-hook 'agda2-highlight-tokens nil 'local)- (add-hook 'after-change-functions 'agda2-highlight-after-inactivity- nil 'local) ;; Support for proper filling of text in comments (requires that ;; Filladapt is activated).@@ -1890,59 +1865,17 @@ (comment-dwim nil)) (pop-mark)))) -(defun agda2-all-extensions (filename)- "Return all of FILENAME's extensions.--FILENAME must not contain any extensions treated specially by-`file-name-extension', such as ~3~."- (let ((ext (concat "." (file-name-extension filename)))- (newname (file-name-sans-extension filename)))- (if (equal newname filename)- ""- (concat (agda2-all-extensions newname) ext))))- (defun agda2-highlight-tokens nil "Compute token-based highlighting information. Unless `agda2-highlight-level' is `none' or the Agda process is-busy with something. This command does not save the buffer."+busy with something. This command might save the buffer." (unless (or agda2-in-progress (equal agda2-highlight-level 'none))- (let ((tmp (make-temp-file "agda2-" nil- (agda2-all-extensions- (file-name-nondirectory- (buffer-file-name))))))- (write-region nil nil tmp nil 'do-not-display-message)- (agda2-go 'do-not-save nil t t- "Cmd_tokenHighlighting"- (agda2-string-quote tmp)- "Remove"))))--(defun agda2-highlight-after-inactivity (beg end len)- "Compute token-based highlighting after Emacs has been idle.-Only if `agda2-highlight-after-inactivity-interval' is a-non-negative number. The number is interpreted as the number of-seconds of continuous inactivity that is required before-highlighting is updated. Furthermore nothing happens unless,-after the given amount of time, the buffer is marked as being-modified, the Agda process is not busy, and-`agda2-highlight-level' is not `none'.--When this procedure is invoked previous, pending invocations are-cancelled.--This procedure is intended to be used in `after-change-functions'."- (when (and (numberp agda2-highlight-after-inactivity-interval)- (>= agda2-highlight-after-inactivity-interval 0))- (when (timerp agda2-highlight-after-inactivity-timer)- (cancel-timer agda2-highlight-after-inactivity-timer))- (setq agda2-highlight-after-inactivity-timer- (run-with-idle-timer agda2-highlight-after-inactivity-interval- nil- `(lambda nil- (with-current-buffer ,(current-buffer)- (when (buffer-modified-p)- (agda2-highlight-tokens))))))))+ (agda2-go 'save nil t t+ "Cmd_tokenHighlighting"+ (agda2-string-quote (buffer-file-name))+ "Keep"))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Go to definition site
stack-8.4.3.yaml view
@@ -1,47 +1,4 @@-resolver: ghc-8.4.3--extra-deps:-- async-2.2.1-- EdisonCore-1.3.2.1-- data-hash-0.2.0.1-- equivalence-0.3.2-- geniplate-mirror-0.7.6-- EdisonAPI-1.3.1-- QuickCheck-2.11.3-- STMonadTrans-0.4.3-- blaze-html-0.9.0.1-- boxes-0.1.5-- edit-distance-0.2.2.1-- gitrev-1.3.1-- hashable-1.2.7.0-- hashtables-1.2.3.0-- ieee754-0.8.0-- murmur-hash-0.1.0.9-- regex-tdfa-1.2.3-- strict-0.3.2-- transformers-compat-0.6.0.6-- unordered-containers-0.2.9.0-- uri-encode-1.5.0.5-- zlib-0.6.2-- base-compat-0.9.3-- blaze-builder-0.4.1.0-- blaze-markup-0.8.2.0-- network-uri-2.6.1.0-- primitive-0.6.3.0-- random-1.1-- regex-base-0.93.2-- split-0.2.3.3-- tf-random-0.5-- utf8-string-1.0.1.1-- vector-0.12.0.1-- cpphs-1.20.8-- old-locale-1.0.0.7-- old-time-1.1.0.3-- polyparse-1.12-- alex-3.2.4-- happy-1.19.9-- text-icu-0.7.0.1-+resolver: lts-12.0 # Local packages, usually specified by relative directory name packages: