Skip to content

Commit

Permalink
Updating Emacs Lisp files with changes in Agda 2.6.4; changing versio…
Browse files Browse the repository at this point in the history 
…n number
  • Loading branch information
@viktorcsimma @jespercockx
viktorcsimma authored and jespercockx committed Oct 22, 2023
1 parent 47066e8 commit 95bf6f6
Show file tree
Hide file tree
Showing 4 changed files with 68 additions and 77 deletions.
35 changes: 33 additions & 2 deletions src/data/emacs-mode/agda-input.el
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,11 +53,11 @@ removing all space and newline characters."
;; Functions used to tweak translation pairs

(defun agda-input-compose (f g)
"\x -> concatMap F (G x)"
"λ x -> concatMap F (G x)"
(lambda (x) (agda-input-concat-map f (funcall g x))))

(defun agda-input-or (f g)
"\x -> F x ++ G x"
"λ x -> F x ++ G x"
(lambda (x) (append (funcall f x) (funcall g x))))

(defun agda-input-nonempty ()
Expand Down Expand Up @@ -340,6 +340,37 @@ order for the change to take effect."
("bx" . ("⊠"))
("b." . ("⊡"))

;; APL boxed operators

("box=" . ("⌸"))
("box?" . ("⍰"))
("box'" . ("⍞"))
("box:" . ("⍠"))
("box/" . ("⍁"))
("box\\" . ("⍂"))
("box<" . ("⍃"))
("box>" . ("⍄"))
("boxo" . ("⌻"))
("boxO" . ("⌼"))

("boxcomp" . ("⌻"))
("boxcircle" . ("⌼"))
("boxeq" . ("⌸"))
("boxneq" . ("⍯"))
("boxeqn" . ("⍯"))

("boxl" . ("⍇"))
("boxr" . ("⍈"))
("boxu" . ("⍐"))
("boxd" . ("⍗"))

("boxdi" . ("⌺"))
("boxdiv" . ("⌹"))
("boxwedge" . ("⍓"))
("boxvee" . ("⍌"))
("boxdelta" . ("⍍"))
("boxnabla" . ("⍔"))

;; Various symbols.

("integral" . ,(agda-input-to-string-list "∫∬∭∮∯∰∱∲∳"))
Expand Down
84 changes: 22 additions & 62 deletions src/data/emacs-mode/agda2-highlight.el
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,24 +58,6 @@ If the face does not exist, then it is created first."
:font 'unspecified)
(eval `(set-face-attribute face nil ,@attrs)))

(defvar agda2-highlight-face-attributes-list
'(:family :width :height :weight :slant :foreground :background
:inverse-video :stipple :underline :overline :strike-through
:inherit :box :font)
"The attributes considered by `agda2-highlight-face-attributes'.")

(defun agda2-highlight-face-attributes (face)
"The names and values of all attributes in FACE.
Only the attributes in `agda2-highlight-face-attributes-list' are
considered. The attributes are returned in a flat list of the
form (name1 value1 name2 value2...)."
(apply 'append
(mapcar (lambda (attr)
(let ((val (face-attribute face attr)))
(if (member val '(unspecified nil)) '()
(list attr (if (symbolp val) `',val val)))))
agda2-highlight-face-attributes-list)))

(defun agda2-highlight-set-faces (variable group)
"Set all Agda faces according to the value of GROUP.
Also sets the default value of VARIABLE to GROUP."
Expand Down Expand Up @@ -146,71 +128,49 @@ Also sets the default value of VARIABLE to GROUP."
:background "light blue")))
((equal group 'default-faces)
(list (cons 'agda2-highlight-keyword-face
(agda2-highlight-face-attributes
font-lock-keyword-face))
(list :inherit font-lock-keyword-face))
(cons 'agda2-highlight-string-face
(agda2-highlight-face-attributes
font-lock-string-face))
(list :inherit font-lock-string-face))
(cons 'agda2-highlight-number-face
(agda2-highlight-face-attributes
font-lock-constant-face))
(list :inherit font-lock-constant-face))
(cons 'agda2-highlight-symbol-face
(agda2-highlight-face-attributes
font-lock-keyword-face))
(list :inherit font-lock-keyword-face))
(cons 'agda2-highlight-primitive-type-face
(agda2-highlight-face-attributes
font-lock-keyword-face))
(list :inherit font-lock-keyword-face))
(cons 'agda2-highlight-bound-variable-face
(agda2-highlight-face-attributes
font-lock-variable-name-face))
(list :inherit font-lock-variable-name-face))
(cons 'agda2-highlight-generalizable-variable-face
(agda2-highlight-face-attributes
font-lock-variable-name-face))
(list :inherit font-lock-variable-name-face))
(cons 'agda2-highlight-inductive-constructor-face
(agda2-highlight-face-attributes
font-lock-type-face))
(list :inherit font-lock-type-face))
(cons 'agda2-highlight-coinductive-constructor-face
(agda2-highlight-face-attributes
font-lock-type-face))
(list :inherit font-lock-type-face))
(cons 'agda2-highlight-datatype-face
(agda2-highlight-face-attributes
font-lock-type-face))
(list :inherit font-lock-type-face))
(cons 'agda2-highlight-field-face
(agda2-highlight-face-attributes
font-lock-variable-name-face))
(list :inherit font-lock-variable-name-face))
(cons 'agda2-highlight-function-face
(agda2-highlight-face-attributes
font-lock-function-name-face))
(list :inherit font-lock-function-name-face))
(cons 'agda2-highlight-module-face
(agda2-highlight-face-attributes
font-lock-type-face))
(list :inherit font-lock-type-face))
(cons 'agda2-highlight-postulate-face
(agda2-highlight-face-attributes
font-lock-type-face))
(list :inherit font-lock-type-face))
(cons 'agda2-highlight-primitive-face
(agda2-highlight-face-attributes
font-lock-constant-face))
(list :inherit font-lock-constant-face))
(cons 'agda2-highlight-macro-face
(agda2-highlight-face-attributes
font-lock-function-name-face))
(list :inherit font-lock-function-name-face))
(cons 'agda2-highlight-record-face
(agda2-highlight-face-attributes
font-lock-variable-name-face))
(list :inherit font-lock-variable-name-face))
(cons 'agda2-highlight-dotted-face
(agda2-highlight-face-attributes
font-lock-variable-name-face))
(list :inherit font-lock-variable-name-face))
(cons 'agda2-highlight-operator-face
(agda2-highlight-face-attributes
font-lock-function-name-face))
(list :inherit font-lock-function-name-face))
(cons 'agda2-highlight-error-face
(agda2-highlight-face-attributes
font-lock-warning-face))
(list :inherit font-lock-warning-face))
(cons 'agda2-highlight-typechecks-face
(agda2-highlight-face-attributes
font-lock-type-face))
(list :inherit font-lock-type-face))
(cons 'agda2-highlight-typechecking-face
(agda2-highlight-face-attributes
font-lock-preprocessor-face)))))))
(list :inherit font-lock-preprocessor-face)))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Faces
Expand Down
4 changes: 2 additions & 2 deletions src/data/emacs-mode/agda2-mode-pkg.el
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
(define-package "agda2-mode" "2.6.3"
(define-package "agda2-mode" "2.6.4"
"interactive development for Agda, a dependently typed functional programming language"
'((emacs "24.3") (annotation "1.0") (eri "1.0")))
'((emacs "24.3"))) ;; dep defs for `annotation.el` and `eri.el` are not required if they are packaged together
22 changes: 11 additions & 11 deletions src/data/emacs-mode/agda2-mode.el
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@

;;; Code:

(defvar agda2-version "2.6.3"
(defvar agda2-version "2.6.4"
"The version of the Agda mode.
Note that the same version of the Agda executable must be used.")

Expand Down Expand Up @@ -93,7 +93,7 @@ Or possibly (let* VARBIND (labels FUNCBIND BODY...))."
:group 'agda2)

(defcustom agda2-program-args
'("--disable-backend") ; so that it doesn't complain about mixing backend with frontend
'("--disable-backend") ; so that it doesn't complain about mixing backend with frontend
"Command-line arguments given to the Agda executable (one per string).
Note: Do not give several arguments in the same string.
Expand All @@ -103,7 +103,7 @@ argument, and does not need to be listed here."
:type '(repeat string)
:group 'agda2)

(defvar agda2-backends '("AGDA2HS")
(defvar agda2-backends '("AGDA2HS" "GHC" "GHCNoMain" "JS" "LaTeX" "QuickLaTeX")
"Compilation backends.")

(defcustom agda2-backend
Expand Down Expand Up @@ -265,13 +265,13 @@ constituents.")
"Table of commands, used to build keymaps and menus.
Each element has the form (CMD &optional KEYS WHERE DESC) where
CMD is a command; KEYS is its key binding (if any); WHERE is a
list which should contain 'local if the command should exist in
the goal menu and 'global if the command should exist in the main
list which should contain \\='local if the command should exist in
the goal menu and \\='global if the command should exist in the main
menu; and DESC is the description of the command used in the
menus.")

(defvar agda2-mode-map
(let ((map (make-sparse-keymap "Agda mode")))
(let ((map (make-sparse-keymap "Agda2Hs mode")))
(define-key map [menu-bar Agda]
(cons "Agda2Hs" (make-sparse-keymap "Agda2Hs")))
(define-key map [down-mouse-3] 'agda2-popup-menu-3)
Expand Down Expand Up @@ -534,7 +534,7 @@ process."
Sends the list of strings ARGS to the Agda2 interpreter, waits
for output and executes the responses, if any.
If SAVE is 'save, then the buffer is saved first.
If SAVE is \\='save, then the buffer is saved first.
If HIGHLIGHT is non-nil, then the buffer's syntax highlighting
may be updated. This is also the case if the Agda process is
Expand Down Expand Up @@ -763,13 +763,13 @@ The user input is computed as follows:
contains whitespace, then the input is taken from the
minibuffer. In this case WANT is used as the prompt string.
* Otherwise (including if WANT is 'goal) the goal contents are
* Otherwise (including if WANT is \\='goal) the goal contents are
used.
If the user input is not taken from the goal, then an empty goal
range is given.
If SAVE is 'save, then the buffer is saved just before the
If SAVE is \\='save, then the buffer is saved just before the
command is sent to Agda (if it is sent)."
(cl-multiple-value-bind (o g) (agda2-goal-at (point))
(unless g (error "For this command, please place the cursor in a goal"))
Expand Down Expand Up @@ -896,8 +896,8 @@ of new goals."
(agda2-goal-cmd "Cmd_autoOne" 'save 'goal))

(defun agda2-autoAll ()
(interactive)
"Solves all goals by simple proof search."
(interactive)
(agda2-go nil nil 'busy t "Cmd_autoAll")
)

Expand Down Expand Up @@ -1953,7 +1953,7 @@ the argument is a positive number, otherwise turn it off."

(defun agda2-get-agda-program-versions ()
"Get \"version strings\" of executables starting with
'agda-mode' in current path."
\\='agda2hs-mode\\=' in current path."
(delete-dups
(mapcar (lambda (path)
;; strip 'agda2hs-mode' prefix
Expand Down

0 comments on commit 95bf6f6

Please sign in to comment.