diff --git a/Agda.cabal b/Agda.cabal --- a/Agda.cabal +++ b/Agda.cabal @@ -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 diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 ==================================== diff --git a/Setup.hs b/Setup.hs --- a/Setup.hs +++ b/Setup.hs @@ -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 diff --git a/dist/build/Agda/Syntax/Parser/Parser.hs b/dist/build/Agda/Syntax/Parser/Parser.hs --- a/dist/build/Agda/Syntax/Parser/Parser.hs +++ b/dist/build/Agda/Syntax/Parser/Parser.hs @@ -7529,379 +7529,7 @@ {-# LINE 10 "" #-} -{-# LINE 1 "/tmp/ghc16748_0/ghc_2.h" #-} - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - +{-# LINE 1 "/tmp/ghc8142_0/ghc_2.h" #-} diff --git a/doc/user-manual.pdf b/doc/user-manual.pdf Binary files a/doc/user-manual.pdf and b/doc/user-manual.pdf differ diff --git a/src/data/emacs-mode/agda2-mode-pkg.el b/src/data/emacs-mode/agda2-mode-pkg.el --- a/src/data/emacs-mode/agda2-mode-pkg.el +++ b/src/data/emacs-mode/agda2-mode-pkg.el @@ -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") diff --git a/src/data/emacs-mode/agda2-mode.el b/src/data/emacs-mode/agda2-mode.el --- a/src/data/emacs-mode/agda2-mode.el +++ b/src/data/emacs-mode/agda2-mode.el @@ -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 diff --git a/stack-8.4.3.yaml b/stack-8.4.3.yaml --- a/stack-8.4.3.yaml +++ b/stack-8.4.3.yaml @@ -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: