uhhh
idkkkk
This commit is contained in:
@@ -11,14 +11,13 @@
|
||||
"." #'agda2-goal-and-context-and-inferred
|
||||
"," #'agda2-goal-and-context
|
||||
"=" #'agda2-show-constraints
|
||||
"SPC" #'agda2-give
|
||||
"g" #'agda2-give
|
||||
"a" #'agda2-mimer-maybe-all
|
||||
"b" #'agda2-previous-goal
|
||||
"[" #'agda2-previous-goal
|
||||
"c" #'agda2-make-case
|
||||
"d" #'agda2-infer-type-maybe-toplevel
|
||||
"e" #'agda2-show-context
|
||||
"f" #'agda2-next-goal
|
||||
"gG" #'agda2-go-back
|
||||
"]" #'agda2-next-goal
|
||||
"h" #'agda2-helper-function-type
|
||||
"l" #'agda2-load
|
||||
"n" #'agda2-compute-normalised-maybe-toplevel
|
||||
@@ -37,6 +36,17 @@
|
||||
:states '(motion normal)
|
||||
"[ n" #'agda2-previous-goal
|
||||
"] n" #'agda2-next-goal)
|
||||
(setq agda2-fontset-name "JuliaMono"))
|
||||
(setq agda2-fontset-name "JuliaMono")
|
||||
|
||||
(defun syd-agda-lookup-documentation ()
|
||||
(interactive)
|
||||
(call-interactively #'agda2-goal-and-context)
|
||||
agda2-info-buffer)
|
||||
|
||||
;; DEPRECATED: Remove once syd-strategies is working.
|
||||
(syd-add-hook 'agda2-mode-hook
|
||||
(defun syd-agda-set-handlers-h ()
|
||||
(setq-local syd-lookup-documentation-handlers
|
||||
(list #'syd-agda-lookup-documentation)))))
|
||||
|
||||
(provide 'syd-lang-agda)
|
||||
|
||||
@@ -69,7 +69,7 @@ to a pop up buffer."
|
||||
(syd-add-hook '(emacs-lisp-mode-hook lisp-data-mode-hook)
|
||||
#'syd-lisp-mode)
|
||||
|
||||
;; DEPRECATED: Remove once syd-strategies is working.
|
||||
;; DEPRECATED: Remove once syd-strategies is working.
|
||||
(syd-add-hook '(emacs-lisp-mode-hook help-mode-hook lisp-data-mode-hook)
|
||||
(defun syd-emacs-set-handlers-h ()
|
||||
(setq-local syd-lookup-documentation-handlers
|
||||
|
||||
@@ -39,7 +39,9 @@ See `https://github.com/ProofGeneral/PG/issues/427'."
|
||||
(set-popup-rules!
|
||||
`((,(rx bol "*idris2-notes*" eol)
|
||||
:ttl nil)
|
||||
(,(rx bol "*idris2-holes" eol)
|
||||
:ttl nil :quit t :vslot -5 :height 7))))
|
||||
(,(rx bol "*idris2-holes*" eol)
|
||||
:ttl nil :quit t :vslot -5 :height 7)))
|
||||
(dolist (c '(?_ ??))
|
||||
(modify-syntax-entry c "w" idris2-syntax-table)))
|
||||
|
||||
(provide 'syd-lang-idris2)
|
||||
|
||||
Reference in New Issue
Block a user