summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndresSicardRamirez <>2018-07-19 14:10:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2018-07-19 14:10:00 (GMT)
commite579926b3d1142f4920960ea34905b3d53af1db5 (patch)
treea6f789c3864a2ccf2c8edd84dd049f1ab213d81f
parentc58679c07afc91634e6bd224921dd16c06449e1e (diff)
version 2.5.4.12.5.4.1
-rw-r--r--Agda.cabal5
-rw-r--r--CHANGELOG.md17
-rw-r--r--Setup.hs26
-rw-r--r--dist/build/Agda/Syntax/Parser/Parser.hs374
-rw-r--r--doc/user-manual.pdfbin647010 -> 645013 bytes
-rw-r--r--src/data/emacs-mode/agda2-mode-pkg.el2
-rw-r--r--src/data/emacs-mode/agda2-mode.el89
-rw-r--r--stack-8.4.3.yaml45
8 files changed, 46 insertions, 512 deletions
diff --git a/Agda.cabal b/Agda.cabal
index 49c722a..1869093 100644
--- 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 head
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 @@ custom-setup
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
index 01d381a..40a8e3b 100644
--- 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
index 8345eb6..29fa95a 100644
--- 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 @@ main = defaultMainWithHooks hooks
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
index 945066b..1edb9a0 100644
--- a/dist/build/Agda/Syntax/Parser/Parser.hs
+++ b/dist/build/Agda/Syntax/Parser/Parser.hs
@@ -7529,379 +7529,7 @@ parseDisplayPragma r pos s =
{-# LINE 10 "<command-line>" #-}
-{-# 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
index 46b773d..d1962e0 100644
--- a/doc/user-manual.pdf
+++ b/doc/user-manual.pdf
Binary files differ
diff --git a/src/data/emacs-mode/agda2-mode-pkg.el b/src/data/emacs-mode/agda2-mode-pkg.el
index 90714e4..6a13520 100644
--- 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
index 1e4709a..69aebaf 100644
--- 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 @@ to this variable to take effect."
(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 @@ Note that this variable is not buffer-local.")
"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 @@ agda2-include-dirs is not bound." :warning))
(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 @@ reloaded from `agda2-highlighting-file', unless
(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 @@ is inserted, and point is placed before this text."
(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 @@ a file is loaded."
;; 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 @@ From the beginning of the current line to the end of the buffer."
(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
index 04bbb9f..126917d 100644
--- 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: