diff --git a/agda2hs.cabal b/agda2hs.cabal index ecfde649..2ac496ed 100644 --- a/agda2hs.cabal +++ b/agda2hs.cabal @@ -15,8 +15,6 @@ description: The tool is implemented as an Agda backend, which means that `agda2hs` is a fully functional Agda compiler. -data-dir: src/data -data-files: emacs-mode/*.el extra-doc-files: CHANGELOG.md README.md @@ -83,16 +81,3 @@ executable agda2hs TupleSections ScopedTypeVariables ghc-options: -Werror - -executable agda2hs-mode - import: smuggler-options - hs-source-dirs: src/agda2hs-mode - main-is: Main.hs - other-modules: Paths_agda2hs - build-depends: base >= 4.10 && < 4.20, - directory >= 1.2.6.2 && < 1.4, - filepath >= 1.4.1.0 && < 1.5, - process >= 1.6.3.0 && < 1.7, - default-language: Haskell2010 - default-extensions: ScopedTypeVariables - ghc-options: -Werror diff --git a/docs/source/features.md b/docs/source/features.md index 71d8e0c9..23dc035a 100644 --- a/docs/source/features.md +++ b/docs/source/features.md @@ -1056,25 +1056,14 @@ If `implicit` is `false`, Prelude gets imported explicitly, and only those ident # Emacs mode -Since there is a full Agda typechecker in the `agda2hs` binary, using a "normal" -Agda installation beside agda2hs can cause a problem: they will check every dependency -again each time you switch from one to another. This problem becomes especially -inconvenient when working with the Emacs mode. +Since there is a full Agda typechecker in the `agda2hs` binary, +you can readily use the Emacs mode of a pre-existing Agda installation (make sure it is the same version as the one `agda2hs` depends on) by changing the binary that `agda-mode` uses (Lisp variable `agda2-program-name`) to (the path to) `agda2hs` binary. -That's why agda2hs comes with a full Agda mode, which uses the Agda typechecker -built into the binary. Installation is roughly the same as with Agda, except that -you use `agda2hs-mode` instead of `agda-mode`. - -With `C-c C-x C-c`, you can even call the `agda2hs` backend from inside Emacs; -but all the usual backends are available, too. +With `C-c C-x C-c`, you will now be able call the `agda2hs` backend from inside Emacs; all the other built-in backends still remain available. ## Known issues -- Switching versions doesn't work yet. -- Documentation and help string are simply taken from the vanilla Agda version. - Now, the output can only be written next to the `.agda` files; there is no option to collect these under a separate directory. - The `--config` option is not yet supported in Emacs mode. -- There might be problems when both the vanilla Agda mode and agda2hs-mode are installed. - For now, it is recommended to install only the agda2hs version. diff --git a/src/agda2hs-mode/Main.hs b/src/agda2hs-mode/Main.hs deleted file mode 100644 index 5364cd7a..00000000 --- a/src/agda2hs-mode/Main.hs +++ /dev/null @@ -1,296 +0,0 @@ --- | A program which either tries to add setup code for Agda's Emacs --- mode to the users .emacs file, or provides information to Emacs --- about where the Emacs mode is installed. --- It uses the Agda compiler bundled with agda2hs. --- Based on Agda's src/agda-mode/Main.hs file. - -module Main (main) where - -import Control.Exception as E -import Control.Monad -import Data.Char -import Data.List (intercalate, isInfixOf) -import Data.Maybe -import Data.Version -import Numeric -import System.Directory -import System.Environment -import System.Exit -import System.FilePath -import System.IO --- import System.IO.Error (isDoesNotExistError) -import System.Process - -import Paths_agda2hs (getDataDir, version) - --- | The program. - -main :: IO () -main = do - prog <- getProgName - args <- getArgs - case args of - [arg] | arg == locateFlag -> printEmacsModeFile - | arg == setupFlag -> do - dotEmacs <- findDotEmacs - setupDotEmacs (Files { thisProgram = prog - , dotEmacs = dotEmacs - }) - | arg == compileFlag -> - compileElispFiles - _ -> do inform usage - exitFailure - --- Command line options. - -setupFlag = "setup" -locateFlag = "locate" -compileFlag = "compile" - --- | Usage information. - -usage :: String -usage = unlines - [ "This program is part of agda2hs version " ++ ver ++ "." - , "It performs actions related to the Emacs mode of the Agda compiler" - , "bundled with agda2hs." - , "" - , "The program can be run in three modes, depending on which option" - , "it is invoked with:" - , "" - , setupFlag - , "" - , " The program tries to add setup code for Agda's Emacs mode to the" - , " current user's .emacs file. It is assumed that the .emacs file" - , " uses the character encoding specified by the locale." - , "" - , locateFlag - , "" - , " The path to the Emacs mode's main file is printed on standard" - , " output (using the UTF-8 character encoding and no trailing" - , " newline)." - , "" - , compileFlag - , "" - , " The program tries to compile Agda's Emacs mode's source files." - , "" - , " WARNING: If you reinstall the Agda mode without recompiling the Emacs" - , " Lisp files, then Emacs may continue using the old, compiled files." - ] - --- | The current version of Agda. - -ver :: String -ver = intercalate "." $ map show $ - versionBranch version - ------------------------------------------------------------------------- --- Locating the Agda mode - --- | Prints out the path to the Agda mode's main file (using UTF-8 and --- without any trailing newline). - -printEmacsModeFile :: IO () -printEmacsModeFile = do - dataDir <- getDataDir - let path = dataDir "emacs-mode" "agda2.el" - hSetEncoding stdout utf8 - putStr path - ------------------------------------------------------------------------- --- Setting up the .emacs file - -data Files = Files { dotEmacs :: FilePath - -- ^ The .emacs file. - , thisProgram :: FilePath - -- ^ The name of the current program. - } - --- | Tries to set up the Agda mode in the given .emacs file. - -setupDotEmacs :: Files -> IO () -setupDotEmacs files = do - informLn $ "The .emacs file used: " ++ dotEmacs files - - already <- alreadyInstalled files - if already then - informLn "It seems as if setup has already been performed." - else do - - appendFile (dotEmacs files) (setupString files) - inform $ unlines $ - [ "Setup done. Try to (re)start Emacs and open an Agda file." - , "The following text was appended to the .emacs file:" - ] ++ lines (setupString files) - --- | Tries to find the user's .emacs file by querying Emacs. - -findDotEmacs :: IO FilePath -findDotEmacs = askEmacs "(expand-file-name user-init-file)" - --- | Has the Agda mode already been set up? - -alreadyInstalled :: Files -> IO Bool -alreadyInstalled files = do - exists <- doesFileExist (dotEmacs files) - if not exists then return False else - withFile (dotEmacs files) ReadMode $ (evaluate . (identifier files `isInfixOf`)) <=< hGetContents - -- Uses evaluate to ensure that the file is not closed - -- prematurely. - --- | If this string occurs in the .emacs file, then it is assumed that --- setup has already been performed. - -identifier :: Files -> String -identifier files = - takeFileName (thisProgram files) ++ " " ++ locateFlag - --- | The string appended to the end of the .emacs file. - -setupString :: Files -> String -setupString files = unlines - [ "" - , "(setenv \"PATH\" (concat (getenv \"PATH\") \":~/.cabal/bin\"))" - , "(setq exec-path (append exec-path '(\"~/.cabal/bin\")))" - -- ^ We append ~/.cabal/bin to PATH, since it's the default installation path when using `cabal new-install`. - , "" - , "(load-file (let ((coding-system-for-read 'utf-8))" - , " (shell-command-to-string \"" - ++ identifier files ++ "\")))" - ] - ------------------------------------------------------------------------- --- Querying Emacs - --- | Evaluates the given Elisp command using Emacs. The output of the --- command (whatever was written into the current buffer) is returned. --- --- Note: The input is not checked. The input is assumed to come from a --- trusted source. - -askEmacs :: String -> IO String -askEmacs query = do - tempDir <- getTemporaryDirectory - bracket (openTempFile tempDir "askEmacs") - (removeFile . fst) $ \(file, h) -> do - hClose h - exit <- rawSystemWithDiagnostics "emacs" - [ "--batch" - -- Andreas, 2022-10-15, issue #5901, suggested by Spencer Baugh (catern): - -- Use Emacs batch mode so that it can run without a terminal. - , "--user", "" - -- The flag --user is necessary with --batch so that user-init-file is defined. - -- The empty user is the default user. - -- (Option --batch includes --no-init-file, this is reverted by supplying --user.) - -- Andreas, 2022-05-25, issue #5901 reloaded: - -- Loading the init file without loading the site fails for some users: - -- , "--quick" - -- -- Option --quick includes --no-site-file. - , "--eval" - , apply [ "with-temp-file", escape file, apply [ "insert", query ] ] - -- Short cutting the temp file via just [ "princ", query ] - -- does not work if the loading of the user-init-file prints extra stuff. - -- Going via the temp file we can let this stuff go to stdout without - -- affecting the output we care about. - ] - unless (exit == ExitSuccess) $ do - informLn "Unable to query Emacs." - exitFailure - withFile file ReadMode $ \h -> do - result <- hGetContents h - evaluate (length result) - -- Uses evaluate to ensure that the file is not closed - -- prematurely. - return result - --- | Like 'rawSystem' but handles 'IOException' by printing diagnostics --- (@PATH@) before 'exitFailure'. - -rawSystemWithDiagnostics - :: FilePath -- ^ Command to run. - -> [String] -- ^ Arguments to command. - -> IO ExitCode -rawSystemWithDiagnostics cmd args = - rawSystem cmd args - `E.catch` \ (e :: IOException) -> do - informLn $ unwords [ "FAILED:", showCommandForUser cmd args ] - informLn $ unwords [ "Exception:", show e ] - -- The PATH might be useful in other exceptions, like "permission denied". - -- when (isDoesNotExistError e) $ do - path <- fromMaybe "(not found)" <$> findExecutable cmd - informLn $ unwords [ "Executable", cmd, "at:", path ] - informLn "PATH:" - mapM_ (informLn . (" - " ++)) =<< getSearchPath - exitFailure - --- | Escapes the string so that Emacs can parse it as an Elisp string. - -escape :: FilePath -> FilePath -escape s = "\"" ++ concatMap esc s ++ "\"" - where - esc c | c `elem` ['\\', '"'] = '\\' : [c] - | isAscii c && isPrint c = [c] - | otherwise = "\\x" ++ showHex (fromEnum c) "\\ " - ------------------------------------------------------------------------- --- Compiling Emacs Lisp files - --- | The Agda mode's Emacs Lisp files, given in the order in which --- they should be compiled. - -emacsLispFiles :: [FilePath] -emacsLispFiles = - [ "agda2-abbrevs.el" - , "annotation.el" - , "agda2-queue.el" - , "eri.el" - , "agda2.el" - , "agda-input.el" - , "agda2-highlight.el" - , "agda2-mode.el" - ] - --- | Tries to compile the Agda mode's Emacs Lisp files. - -compileElispFiles :: IO () -compileElispFiles = do - dataDir <- ( "emacs-mode") <$> getDataDir - let elFiles = map (dataDir ) emacsLispFiles - elFiles <- filterM doesFileExist elFiles - results <- mapM (compile dataDir) elFiles - case catMaybes results of - [] -> return () - fs -> do - informLn "Unable to compile the following Emacs Lisp files:" - mapM_ (informLn . (" " ++)) fs - exitFailure - where - compile dataDir f = do - exit <- rawSystemWithDiagnostics "emacs" $ - [ "--quick" -- 'quick' implies 'no-site-file' - , "--directory", dataDir - , "--batch" -- 'batch' implies 'no-init-file' but not 'no-site-file'. - , "--eval" - , "(progn \ - \(setq byte-compile-error-on-warn t) \ - \(byte-compile-disable-warning 'cl-functions) \ - \(batch-byte-compile))" - , f - ] - return $ if exit == ExitSuccess then Nothing else Just f - ------------------------------------------------------------------------- --- Helper functions - --- These functions inform the user about something by printing on --- stderr. - -inform = hPutStr stderr -informLn = hPutStrLn stderr - -parens :: String -> String -parens s = concat [ "(", s, ")" ] - --- LISP application -apply :: [String] -> String -apply = parens . unwords diff --git a/src/data/emacs-mode/agda-input.el b/src/data/emacs-mode/agda-input.el deleted file mode 100644 index 9cb09a04..00000000 --- a/src/data/emacs-mode/agda-input.el +++ /dev/null @@ -1,1445 +0,0 @@ -;;; -*- lexical-binding: t; -*- -;;; agda-input.el --- The Agda input method - -;; SPDX-License-Identifier: MIT License -;;; Commentary: - -;; A highly customisable input method which can inherit from other -;; Quail input methods. By default the input method is geared towards -;; the input of mathematical and other symbols in Agda programs. -;; -;; Use M-x customize-group agda-input to customise this input method. -;; Note that the functions defined under "Functions used to tweak -;; translation pairs" below can be used to tweak both the key -;; translations inherited from other input methods as well as the -;; ones added specifically for this one. -;; -;; Use agda-input-show-translations to see all the characters which -;; can be typed using this input method (except for those -;; corresponding to ASCII characters). - -;;; Code: - -(require 'quail) -(require 'cl-lib) -;; Quail is quite stateful, so be careful when editing this code. Note -;; that with-temp-buffer is used below whenever buffer-local state is -;; modified. - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Utility functions - -(defun agda-input-concat-map (f xs) - "Concat (map F XS)." - (apply 'append (mapcar f xs))) - -(defun agda-input-to-string-list (s) - "Convert a string S to a list of one-character strings, after -removing all space and newline characters." - (agda-input-concat-map - (lambda (c) (if (member c (string-to-list " \n")) - nil - (list (string c)))) - (string-to-list s))) - -(defun agda-input-character-range (from to) - "A string consisting of the characters from FROM to TO." - (let (seq) - (dotimes (i (1+ (- to from))) - (setq seq (cons (+ from i) seq))) - (concat (nreverse seq)))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Functions used to tweak translation pairs - -(defun agda-input-compose (f g) - "λ 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" - (lambda (x) (append (funcall f x) (funcall g x)))) - -(defun agda-input-nonempty () - "Only keep pairs with a non-empty first component." - (lambda (x) (if (> (length (car x)) 0) (list x)))) - -(defun agda-input-prepend (prefix) - "Prepend PREFIX to all key sequences." - (lambda (x) `((,(concat prefix (car x)) . ,(cdr x))))) - -(defun agda-input-prefix (prefix) - "Only keep pairs whose key sequence starts with PREFIX." - (lambda (x) - (if (equal (substring (car x) 0 (length prefix)) prefix) - (list x)))) - -(defun agda-input-suffix (suffix) - "Only keep pairs whose key sequence ends with SUFFIX." - (lambda (x) - (if (equal (substring (car x) - (- (length (car x)) (length suffix))) - suffix) - (list x)))) - -(defun agda-input-drop (ss) - "Drop pairs matching one of the given key sequences. -SS should be a list of strings." - (lambda (x) (unless (member (car x) ss) (list x)))) - -(defun agda-input-drop-beginning (n) - "Drop N characters from the beginning of each key sequence." - (lambda (x) `((,(substring (car x) n) . ,(cdr x))))) - -(defun agda-input-drop-end (n) - "Drop N characters from the end of each key sequence." - (lambda (x) - `((,(substring (car x) 0 (- (length (car x)) n)) . - ,(cdr x))))) - -(defun agda-input-drop-prefix (prefix) - "Only keep pairs whose key sequence starts with PREFIX. -This prefix is dropped." - (agda-input-compose - (agda-input-drop-beginning (length prefix)) - (agda-input-prefix prefix))) - -(defun agda-input-drop-suffix (suffix) - "Only keep pairs whose key sequence ends with SUFFIX. -This suffix is dropped." - (agda-input-compose - (agda-input-drop-end (length suffix)) - (agda-input-suffix suffix))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Customization - -;; The :set keyword is set to 'agda-input-incorporate-changed-setting -;; so that the input method gets updated immediately when users -;; customize it. However, the setup functions cannot be run before all -;; variables have been defined. Hence the :initialize keyword is set to -;; 'custom-initialize-default to ensure that the setup is not performed -;; until agda-input-setup is called at the end of this file. - -(defgroup agda-input nil - "The Agda input method. -After tweaking these settings you may want to inspect the resulting -translations using `agda-input-show-translations'." - :group 'agda2 - :group 'leim) - -(defcustom agda-input-tweak-all - '(agda-input-compose - (agda-input-prepend "\\") - (agda-input-nonempty)) - "An expression yielding a function which can be used to tweak -all translations before they are included in the input method. -The resulting function (if non-nil) is applied to every -\(KEY-SEQUENCE . TRANSLATION) pair and should return a list of such -pairs. (Note that the translations can be anything accepted by -`quail-defrule'.) - -If you change this setting manually (without using the -customization buffer) you need to call `agda-input-setup' in -order for the change to take effect." - :group 'agda-input - :set 'agda-input-incorporate-changed-setting - :initialize 'custom-initialize-default - :type 'sexp) - -(defcustom agda-input-inherit - `(("TeX" . (agda-input-compose - (agda-input-drop '("geq" "leq" "bullet" "qed" "par")) - (agda-input-or - (agda-input-drop-prefix "\\") - (agda-input-or - (agda-input-compose - (agda-input-drop '("^l" "^o" "^r" "^v")) - (agda-input-prefix "^")) - (agda-input-prefix "_"))))) - ) - "A list of Quail input methods whose translations should be -inherited by the Agda input method (with the exception of -translations corresponding to ASCII characters). - -The list consists of pairs (qp . tweak), where qp is the name of -a Quail package, and tweak is an expression of the same kind as -`agda-input-tweak-all' which is used to tweak the translation -pairs of the input method. - -The inherited translation pairs are added last, after -`agda-input-user-translations' and `agda-input-translations'. - -If you change this setting manually (without using the -customization buffer) you need to call `agda-input-setup' in -order for the change to take effect." - :group 'agda-input - :set 'agda-input-incorporate-changed-setting - :initialize 'custom-initialize-default - :type '(repeat (cons (string :tag "Quail package") - (sexp :tag "Tweaking function")))) - -(defcustom agda-input-translations - (let ((max-lisp-eval-depth 2800)) `( - - ;; Equality and similar symbols. - - ("eq" . ,(agda-input-to-string-list "=∼∽≈≋∻∾∿≀≃⋍≂≅ ≌≊≡≣≐≑≒≓≔≕≖≗≘≙≚≛≜≝≞≟≍≎≏≬⋕＝")) - ("eqn" . ,(agda-input-to-string-list "≠≁ ≉ ≄ ≇≆ ≢ ≭ ")) - - ("=n" . ("≠")) - ("~" . ,(agda-input-to-string-list "∼～")) - ("~n" . ("≁")) - ("~~" . ("≈")) ("~~n" . ("≉")) - ("~~~" . ("≋")) - (":~" . ("∻")) - ("~-" . ("≃")) ("~-n" . ("≄")) - ("-~" . ("≂")) - ("~=" . ("≅")) ("~=n" . ("≇")) - ("~~-" . ("≊")) - ("==" . ("≡")) ("==n" . ("≢")) - ("===" . ("≣")) - ("=" . ("＝")) - (".=" . ("≐")) (".=." . ("≑")) - (":=" . ("≔")) ("=:" . ("≕")) - ("=o" . ("≗")) - ("(=" . ("≘")) - ("and=" . ("≙")) ("or=" . ("≚")) - ("*=" . ("≛")) - ("t=" . ("≜")) - ("def=" . ("≝")) - ("m=" . ("≞")) - ("?=" . ("≟")) - - ;; Inequality and similar symbols. - - ("leq" . ,(agda-input-to-string-list "<≪⋘≤≦≲ ≶≺≼≾⊂⊆ ⋐⊏⊑ ⊰⊲⊴⋖⋚⋜⋞＜")) - ("leqn" . ,(agda-input-to-string-list "≮ ≰≨≴⋦≸⊀ ⋨⊄⊈⊊ ⋢⋤ ⋪⋬ ⋠")) - ("geq" . ,(agda-input-to-string-list ">≫⋙≥≧≳ ≷≻≽≿⊃⊇ ⋑⊐⊒ ⊱⊳⊵⋗⋛⋝⋟＞")) - ("geqn" . ,(agda-input-to-string-list "≯ ≱≩≵⋧≹⊁ ⋩⊅⊉⊋ ⋣⋥ ⋫⋭ ⋡")) - - ("<=" . ("≤")) (">=" . ("≥")) - ("<=n" . ("≰")) (">=n" . ("≱")) - ("len" . ("≰")) ("gen" . ("≱")) - ("n" . ("≯")) - ("<~" . ("≲")) (">~" . ("≳")) - ("<~n" . ("⋦")) (">~n" . ("⋧")) - ("<~nn" . ("≴")) (">~nn" . ("≵")) - - ("sub" . ("⊂")) ("sup" . ("⊃")) - ("subn" . ("⊄")) ("supn" . ("⊅")) - ("sub=" . ("⊆")) ("sup=" . ("⊇")) - ("sub=n" . ("⊈")) ("sup=n" . ("⊉")) - - ("squb" . ("⊏")) ("squp" . ("⊐")) - ("squb=" . ("⊑")) ("squp=" . ("⊒")) - ("squb=n" . ("⋢")) ("squp=n" . ("⋣")) - - ;; Set membership etc. - - ("member" . ,(agda-input-to-string-list "∈∉∊∋∌∍⋲⋳⋴⋵⋶⋷⋸⋹⋺⋻⋼⋽⋾⋿")) - - ("inn" . ("∉")) - ("nin" . ("∌")) - - ;; Intersections, unions etc. - - ("intersection" . ,(agda-input-to-string-list "∩⋂∧⋀⋏⨇⊓⨅⋒∏ ⊼ ⨉")) - ("union" . ,(agda-input-to-string-list "∪⋃∨⋁⋎⨈⊔⨆⋓∐⨿⊽⊻⊍⨃⊎⨄⊌∑⅀")) - - ("and" . ("∧")) ("or" . ("∨")) - ("And" . ("⋀")) ("Or" . ("⋁")) - ("i" . ("∩")) ("un" . ("∪")) ("u+" . ("⊎")) ("u." . ("⊍")) - ("I" . ("⋂")) ("Un" . ("⋃")) ("U+" . ("⨄")) ("U." . ("⨃")) - ("glb" . ("⊓")) ("lub" . ("⊔")) - ("Glb" . ("⨅")) ("Lub" . ("⨆")) - - ;; Entailment etc. - - ("entails" . ,(agda-input-to-string-list "⊢⊣⊤⊥⊦⊧⊨⊩⊪⊫⊬⊭⊮⊯")) - - ("|-" . ("⊢")) ("|-n" . ("⊬")) - ("-|" . ("⊣")) - ("|=" . ("⊨")) ("|=n" . ("⊭")) - ("||-" . ("⊩")) ("||-n" . ("⊮")) - ("||=" . ("⊫")) ("||=n" . ("⊯")) - ("|||-" . ("⊪")) - - ;; Divisibility, parallelity. - - ("|" . ("∣")) ("|n" . ("∤")) - ("||" . ("∥")) ("||n" . ("∦")) - - ;; Some symbols from logic and set theory. - - ("all" . ("∀")) - ("ex" . ("∃")) - ("exn" . ("∄")) - ("0" . ("∅")) - ("C" . ("∁")) - - ;; Corners, ceilings and floors. - - ("c" . ,(agda-input-to-string-list "⌜⌝⌞⌟⌈⌉⌊⌋")) - ("cu" . ,(agda-input-to-string-list "⌜⌝ ⌈⌉ ")) - ("cl" . ,(agda-input-to-string-list " ⌞⌟ ⌊⌋")) - - ("cul" . ("⌜")) ("cuL" . ("⌈")) - ("cur" . ("⌝")) ("cuR" . ("⌉")) - ("cll" . ("⌞")) ("clL" . ("⌊")) - ("clr" . ("⌟")) ("clR" . ("⌋")) - - ;; Various operators/symbols. - - ("qed" . ("∎")) - ("x" . ("×")) - ("o" . ("∘")) - ("comp" . ("∘")) - ("." . ,(agda-input-to-string-list "∙．")) - ("*" . ("⋆")) - (".+" . ("∔")) - (".-" . ("∸")) - (":" . ,(agda-input-to-string-list "∶⦂ː꞉˸፥፦：﹕︓")) - ("," . ,(agda-input-to-string-list "ʻ،⸲⸴⹁⹉、︐︑﹐﹑，､")) - (";" . ,(agda-input-to-string-list "⨾⨟⁏፤꛶；︔﹔⍮⸵;")) - ("::" . ("∷")) - ("::-" . ("∺")) - ("-:" . ("∹")) - ("+ " . ("⊹")) - ("+" . ("＋")) - ("sqrt" . ("√")) - ("surd3" . ("∛")) - ("surd4" . ("∜")) - ("increment" . ("∆")) - ("inf" . ("∞")) - ("&" . ("⅋")) - ("z;" . ,(agda-input-to-string-list "⨟⨾")) - ("z:" . ("⦂")) - - ;; Circled operators. - - ("o+" . ("⊕")) - ("o--" . ("⊖")) - ("ox" . ("⊗")) - ("o/" . ("⊘")) - ("o." . ("⊙")) - ("oo" . ("⊚")) - ("o*" . ("⊛")) - ("o=" . ("⊜")) - ("o-" . ("⊝")) - - ("O+" . ("⨁")) - ("Ox" . ("⨂")) - ("O." . ("⨀")) - ("O*" . ("⍟")) - - ;; Boxed operators. - - ("b+" . ("⊞")) - ("b-" . ("⊟")) - ("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 "∫∬∭∮∯∰∱∲∳")) - ("angle" . ,(agda-input-to-string-list "∟∡∢⊾⊿")) - ("join" . ,(agda-input-to-string-list "⋈⋉⋊⋋⋌⨝⟕⟖⟗")) - - ;; Arrows. - - ("l" . ,(agda-input-to-string-list "←⇐⇚⭅⇇⇆↤⇦↞↼↽⇠⇺↜⇽⟵⟸↚⇍⇷ ↹ ↢↩↫⇋⇜⇤⟻⟽⤆↶↺⟲ ")) - ("r" . ,(agda-input-to-string-list "→⇒⇛⭆⇉⇄↦⇨↠⇀⇁⇢⇻↝⇾⟶⟹↛⇏⇸⇶ ↴ ↣↪↬⇌⇝⇥⟼⟾⤇↷↻⟳⇰⇴⟴⟿ ➵➸➙➔➛➜➝➞➟➠➡➢➣➤➧➨➩➪➫➬➭➮➯➱➲➳➺➻➼➽➾⊸")) - ("u" . ,(agda-input-to-string-list "↑⇑⤊⟰⇈⇅↥⇧↟↿↾⇡⇞ ↰↱➦ ⇪⇫⇬⇭⇮⇯ ")) - ("d" . ,(agda-input-to-string-list "↓⇓⤋⟱⇊⇵↧⇩↡⇃⇂⇣⇟ ↵↲↳➥ ↯ ")) - ("ud" . ,(agda-input-to-string-list "↕⇕ ↨⇳ ")) - ("lr" . ,(agda-input-to-string-list "↔⇔ ⇼↭⇿⟷⟺↮⇎⇹ ")) - ("ul" . ,(agda-input-to-string-list "↖⇖ ⇱↸ ")) - ("ur" . ,(agda-input-to-string-list "↗⇗ ➶➹➚ ")) - ("dr" . ,(agda-input-to-string-list "↘⇘ ⇲ ➴➷➘ ")) - ("dl" . ,(agda-input-to-string-list "↙⇙ ")) - - ("l-" . ("←")) ("<-" . ("←")) ("l=" . ("⇐")) ("<=" . ("⇐")) - ("r-" . ("→")) ("->" . ("→")) ("r=" . ("⇒")) ("=>" . ("⇒")) - ("u-" . ("↑")) ("u=" . ("⇑")) - ("d-" . ("↓")) ("d=" . ("⇓")) - ("ud-" . ("↕")) ("ud=" . ("⇕")) - ("lr-" . ("↔")) ("<->" . ("↔")) ("lr=" . ("⇔")) ("<=>" . ("⇔")) - ("ul-" . ("↖")) ("ul=" . ("⇖")) - ("ur-" . ("↗")) ("ur=" . ("⇗")) - ("dr-" . ("↘")) ("dr=" . ("⇘")) - ("dl-" . ("↙")) ("dl=" . ("⇙")) - - ("l==" . ("⇚")) ("l-2" . ("⇇")) ("l-r-" . ("⇆")) - ("r==" . ("⇛")) ("r-2" . ("⇉")) ("r-3" . ("⇶")) ("r-l-" . ("⇄")) - ("u==" . ("⟰")) ("u-2" . ("⇈")) ("u-d-" . ("⇅")) - ("d==" . ("⟱")) ("d-2" . ("⇊")) ("d-u-" . ("⇵")) - - ("l--" . ("⟵")) ("<--" . ("⟵")) ("l~" . ("↜" "⇜")) - ("r--" . ("⟶")) ("-->" . ("⟶")) ("r~" . ("↝" "⇝" "⟿")) - ("lr--" . ("⟷")) ("<-->" . ("⟷")) ("lr~" . ("↭")) - - ("l-n" . ("↚")) ("<-n" . ("↚")) ("l=n" . ("⇍")) - ("r-n" . ("↛")) ("->n" . ("↛")) ("r=n" . ("⇏")) ("=>n" . ("⇏")) - ("lr-n" . ("↮")) ("<->n" . ("↮")) ("lr=n" . ("⇎")) ("<=>n" . ("⇎")) - - ("l-|" . ("↤")) ("ll-" . ("↞")) - ("r-|" . ("↦")) ("rr-" . ("↠")) - ("u-|" . ("↥")) ("uu-" . ("↟")) - ("d-|" . ("↧")) ("dd-" . ("↡")) - ("ud-|" . ("↨")) - - ("l->" . ("↢")) - ("r->" . ("↣")) - - ("r-o" . ("⊸")) ("-o" . ("⊸")) - - ("dz" . ("↯")) - - ;; Ellipsis. - - ("..." . ,(agda-input-to-string-list "⋯⋮⋰⋱")) - - ;; Box-drawing characters. - - ("---" . ,(agda-input-to-string-list "─│┌┐└┘├┤┬┼┴╴╵╶╷╭╮╯╰╱╲╳")) - ("--=" . ,(agda-input-to-string-list "═║╔╗╚╝╠╣╦╬╩ ╒╕╘╛╞╡╤╪╧ ╓╖╙╜╟╢╥╫╨")) - ("--_" . ,(agda-input-to-string-list "━┃┏┓┗┛┣┫┳╋┻╸╹╺╻ - ┍┯┑┕┷┙┝┿┥┎┰┒┖┸┚┠╂┨┞╀┦┟╁┧┢╈┪┡╇┩ - ┮┭┶┵┾┽┲┱┺┹╊╉╆╅╄╃ ╿╽╼╾")) - ("--." . ,(agda-input-to-string-list "╌╎┄┆┈┊ - ╍╏┅┇┉┋")) - - ;; Triangles. - - ;; Big/small, black/white. - - ("t" . ,(agda-input-to-string-list "◂◃◄◅▸▹►▻▴▵▾▿◢◿◣◺◤◸◥◹")) - ("T" . ,(agda-input-to-string-list "◀◁▶▷▲△▼▽◬◭◮")) - - ("tb" . ,(agda-input-to-string-list "◂▸▴▾◄►◢◣◤◥")) - ("tw" . ,(agda-input-to-string-list "◃▹▵▿◅▻◿◺◸◹")) - - ("Tb" . ,(agda-input-to-string-list "◀▶▲▼")) - ("Tw" . ,(agda-input-to-string-list "◁▷△▽")) - - ;; Squares. - - ("sq" . ,(agda-input-to-string-list "■□◼◻◾◽▣▢▤▥▦▧▨▩◧◨◩◪◫◰◱◲◳")) - ("sqb" . ,(agda-input-to-string-list "■◼◾")) - ("sqw" . ,(agda-input-to-string-list "□◻◽")) - ("sq." . ("▣")) - ("sqo" . ("▢")) - - ;; Rectangles. - - ("re" . ,(agda-input-to-string-list "▬▭▮▯")) - ("reb" . ,(agda-input-to-string-list "▬▮")) - ("rew" . ,(agda-input-to-string-list "▭▯")) - - ;; Parallelograms. - - ("pa" . ,(agda-input-to-string-list "▰▱")) - ("pab" . ("▰")) - ("paw" . ("▱")) - - ;; Diamonds. - - ("di" . ,(agda-input-to-string-list "◆◇◈")) - ("dib" . ("◆")) - ("diw" . ("◇")) - ("di." . ("◈")) - - ;; Circles. - - ("ci" . ,(agda-input-to-string-list "●○◎◌◯◍◐◑◒◓◔◕◖◗◠◡◴◵◶◷⚆⚇⚈⚉")) - ("cib" . ("●")) - ("ciw" . ("○")) - ("ci." . ("◎")) - ("ci.." . ("◌")) - ("ciO" . ("◯")) - - ;; Stars. - - ("st" . ,(agda-input-to-string-list "⋆✦✧✶✴✹ ★☆✪✫✯✰✵✷✸")) - ("st4" . ,(agda-input-to-string-list "✦✧")) - ("st6" . ("✶")) - ("st8" . ("✴")) - ("st12" . ("✹")) - - ;; Blackboard bold letters. - - ("bA" . ("𝔸")) - ("bB" . ("𝔹")) - ("bC" . ("ℂ")) - ("bD" . ("𝔻")) - ("bE" . ("𝔼")) - ("bF" . ("𝔽")) - ("bG" . ("𝔾")) - ("bH" . ("ℍ")) - ("bI" . ("𝕀")) - ("bJ" . ("𝕁")) - ("bK" . ("𝕂")) - ("bL" . ("𝕃")) - ("bM" . ("𝕄")) - ("bN" . ("ℕ")) - ("bO" . ("𝕆")) - ("bP" . ("ℙ")) - ("bQ" . ("ℚ")) - ("bR" . ("ℝ")) - ("bS" . ("𝕊")) - ("bT" . ("𝕋")) - ("bU" . ("𝕌")) - ("bV" . ("𝕍")) - ("bW" . ("𝕎")) - ("bX" . ("𝕏")) - ("bY" . ("𝕐")) - ("bZ" . ("ℤ")) - ("bGG" . ("ℾ")) - ("bGP" . ("ℿ")) - ("bGS" . ("⅀")) - ("ba" . ("𝕒")) - ("bb" . ("𝕓")) - ("bc" . ("𝕔")) - ("bd" . ("𝕕")) - ("be" . ("𝕖")) - ("bf" . ("𝕗")) - ("bg" . ("𝕘")) - ("bh" . ("𝕙")) - ("bi" . ("𝕚")) - ("bj" . ("𝕛")) - ("bk" . ("𝕜")) - ("bl" . ("𝕝")) - ("bm" . ("𝕞")) - ("bn" . ("𝕟")) - ("bo" . ("𝕠")) - ("bp" . ("𝕡")) - ("bq" . ("𝕢")) - ("br" . ("𝕣")) - ("bs" . ("𝕤")) - ("bt" . ("𝕥")) - ("bu" . ("𝕦")) - ("bv" . ("𝕧")) - ("bw" . ("𝕨")) - ("bx" . ("𝕩")) - ("by" . ("𝕪")) - ("bz" . ("𝕫")) - ("bGg" . ("ℽ")) - ("bGp" . ("ℼ")) - - ;; Blackboard bold numbers. - - ("b0" . ("𝟘")) - ("b1" . ("𝟙")) - ("b2" . ("𝟚")) - ("b3" . ("𝟛")) - ("b4" . ("𝟜")) - ("b5" . ("𝟝")) - ("b6" . ("𝟞")) - ("b7" . ("𝟟")) - ("b8" . ("𝟠")) - ("b9" . ("𝟡")) - - ;; Mathematical bold letters. - - ("BA" . ("𝐀")) - ("BB" . ("𝐁")) - ("BC" . ("𝐂")) - ("BD" . ("𝐃")) - ("BE" . ("𝐄")) - ("BF" . ("𝐅")) - ("BG" . ("𝐆")) - ("BH" . ("𝐇")) - ("BI" . ("𝐈")) - ("BJ" . ("𝐉")) - ("BK" . ("𝐊")) - ("BL" . ("𝐋")) - ("BM" . ("𝐌")) - ("BN" . ("𝐍")) - ("BO" . ("𝐎")) - ("BP" . ("𝐏")) - ("BQ" . ("𝐐")) - ("BR" . ("𝐑")) - ("BS" . ("𝐒")) - ("BT" . ("𝐓")) - ("BU" . ("𝐔")) - ("BV" . ("𝐕")) - ("BW" . ("𝐖")) - ("BX" . ("𝐗")) - ("BY" . ("𝐘")) - ("BZ" . ("𝐙")) - ("Ba" . ("𝐚")) - ("Bb" . ("𝐛")) - ("Bc" . ("𝐜")) - ("Bd" . ("𝐝")) - ("Be" . ("𝐞")) - ("Bf" . ("𝐟")) - ("Bg" . ("𝐠")) - ("Bh" . ("𝐡")) - ("Bi" . ("𝐢")) - ("Bj" . ("𝐣")) - ("Bk" . ("𝐤")) - ("Bl" . ("𝐥")) - ("Bm" . ("𝐦")) - ("Bn" . ("𝐧")) - ("Bo" . ("𝐨")) - ("Bp" . ("𝐩")) - ("Bq" . ("𝐪")) - ("Br" . ("𝐫")) - ("Bs" . ("𝐬")) - ("Bt" . ("𝐭")) - ("Bu" . ("𝐮")) - ("Bv" . ("𝐯")) - ("Bw" . ("𝐰")) - ("Bx" . ("𝐱")) - ("By" . ("𝐲")) - ("Bz" . ("𝐳")) - - ;; Mathematical bold Greek letters. - - ("BGA" . ("𝚨")) - ("BGB" . ("𝚩")) - ("BGC" . ("𝚾")) - ("BGD" . ("𝚫")) - ("BGE" . ("𝚬")) - ("BGG" . ("𝚪")) - ("BGH" . ("𝚮")) - ("BGI" . ("𝚰")) - ("BGK" . ("𝚱")) - ("BGL" . ("𝚲")) - ("BGM" . ("𝚳")) - ("BGN" . ("𝚴")) - ("BGO" . ("𝛀")) - ("BOmicron" . ("𝚶")) - ("BGF" . ("𝚽")) - ("BPi" . ("𝚷")) - ("BGP" . ("𝚿")) - ("BGR" . ("𝚸")) - ("BGS" . ("𝚺")) - ("BGT" . ("𝚻")) - ("BGTH" . ("𝚯")) - ("BGU" . ("𝚼")) - ("BGX" . ("𝚵")) - ("BGZ" . ("𝚭")) - ("BGa" . ("𝛂")) - ("BGb" . ("𝛃")) - ("BGc" . ("𝛘")) - ("BGd" . ("𝛅")) - ("BGe" . ("𝛆")) - ("BGg" . ("𝛄")) - ("BGh" . ("𝛈")) - ("BGi" . ("𝛊")) - ("BGk" . ("𝛋")) - ("BGl" . ("𝛌")) - ("BGm" . ("𝛍")) - ("BGn" . ("𝛎")) - ("BGo" . ("𝛚")) - ("Bomicron" . ("𝛐")) - ("BGf" . ("𝛗")) - ("Bpi" . ("𝛑")) - ("BGp" . ("𝛙")) - ("BGr" . ("𝛒")) - ("BGs" . ("𝛔")) - ("BGt" . ("𝛕")) - ("BGth" . ("𝛉")) - ("BGu" . ("𝛖")) - ("BGx" . ("𝛏")) - ("BGz" . ("𝛇")) - - ;; Mathematical bold digits. - - ("B0" . ("𝟎")) - ("B1" . ("𝟏")) - ("B2" . ("𝟐")) - ("B3" . ("𝟑")) - ("B4" . ("𝟒")) - ("B5" . ("𝟓")) - ("B6" . ("𝟔")) - ("B7" . ("𝟕")) - ("B8" . ("𝟖")) - ("B9" . ("𝟗")) - - ;; Fullwidth letters - - ("FA" . ("Ａ")) - ("FB" . ("Ｂ")) - ("FC" . ("Ｃ")) - ("FD" . ("Ｄ")) - ("FE" . ("Ｅ")) - ("FF" . ("Ｆ")) - ("FG" . ("Ｇ")) - ("FH" . ("Ｈ")) - ("FI" . ("Ｉ")) - ("FJ" . ("Ｊ")) - ("FK" . ("Ｋ")) - ("FL" . ("Ｌ")) - ("FM" . ("Ｍ")) - ("FN" . ("Ｎ")) - ("FO" . ("Ｏ")) - ("FP" . ("Ｐ")) - ("FQ" . ("Ｑ")) - ("FR" . ("Ｒ")) - ("FS" . ("Ｓ")) - ("FT" . ("Ｔ")) - ("FU" . ("Ｕ")) - ("FV" . ("Ｖ")) - ("FW" . ("Ｗ")) - ("FX" . ("Ｘ")) - ("FY" . ("Ｙ")) - ("FZ" . ("Ｚ")) - ("Fa" . ("ａ")) - ("Fb" . ("ｂ")) - ("Fc" . ("ｃ")) - ("Fd" . ("ｄ")) - ("Fe" . ("ｅ")) - ("Ff" . ("ｆ")) - ("Fg" . ("ｇ")) - ("Fh" . ("ｈ")) - ("Fi" . ("ｉ")) - ("Fj" . ("ｊ")) - ("Fk" . ("ｋ")) - ("Fl" . ("ｌ")) - ("Fm" . ("ｍ")) - ("Fn" . ("ｎ")) - ("Fo" . ("ｏ")) - ("Fp" . ("ｐ")) - ("Fq" . ("ｑ")) - ("Fr" . ("ｒ")) - ("Fs" . ("ｓ")) - ("Ft" . ("ｔ")) - ("Fu" . ("ｕ")) - ("Fv" . ("ｖ")) - ("Fw" . ("ｗ")) - ("Fx" . ("ｘ")) - ("Fy" . ("ｙ")) - ("Fz" . ("ｚ")) - - ;; Fullwidth digits - - ("F0" . ("０")) - ("F1" . ("１")) - ("F2" . ("２")) - ("F3" . ("３")) - ("F4" . ("４")) - ("F5" . ("５")) - ("F6" . ("６")) - ("F7" . ("７")) - ("F8" . ("８")) - ("F9" . ("９")) - - ;; Parentheses. - - ("(" . ,(agda-input-to-string-list "([{⁅⁽₍〈⎴⟅⟦⟨⟪⦃〈《「『【〔〖〚︵︷︹︻︽︿﹁﹃﹙﹛﹝（［｛｢❪❬❰❲❴⟮⦅⦗⧼⸨❮⦇⦉")) - (")" . ,(agda-input-to-string-list ")]}⁆⁾₎〉⎵⟆⟧⟩⟫⦄〉》」』】〕〗〛︶︸︺︼︾﹀﹂﹄﹚﹜﹞）］｝｣❫❭❱❳❵⟯⦆⦘⧽⸩❯⦈⦊")) - - ("[[" . ("⟦")) - ("]]" . ("⟧")) - ("<" . ,(agda-input-to-string-list "⟨<≪⋘≺⊂⋐⊏⊰⊲⋖＜")) - (">" . ,(agda-input-to-string-list "⟩>≫⋙≻⊃⋑⊐⊱⊳⋗＞")) - ("<<" . ("⟪")) - (">>" . ("⟫")) - ("{{" . ("⦃")) - ("}}" . ("⦄")) - - ("(b" . ("⟅")) - (")b" . ("⟆")) - - ("lbag" . ("⟅")) - ("rbag" . ("⟆")) - - ("<|" . ("⦉")) ;; Angle bar brackets - ("|>" . ("⦊")) - - ("(|" . ("⦇")) ;; Idiom brackets - ("|)" . ("⦈")) - - ("((" . ,(agda-input-to-string-list "⦅｟")) ;; Banana brackets - ("))" . ,(agda-input-to-string-list "⦆｠")) - - ;; Primes. - - ("'" . ,(agda-input-to-string-list "′″‴⁗＇")) - ("`" . ,(agda-input-to-string-list "‵‶‷｀")) - - ;; Fractions. - - ("frac" . ,(agda-input-to-string-list "¼½¾⅓⅔⅕⅖⅗⅘⅙⅚⅛⅜⅝⅞⅟")) - - ;; Bullets. - - ("bu" . ,(agda-input-to-string-list "•◦‣⁌⁍")) - ("bub" . ("•")) - ("buw" . ("◦")) - ("but" . ("‣")) - - ;; Musical symbols. - - ("note" . ,(agda-input-to-string-list "♩♪♫♬")) - ("b" . ("♭")) - ("#" . ("♯")) - - ;; Other punctuation and symbols. - - ("\\" . ("\\")) - ("en" . ("–")) - ("em" . ("—")) - ("!" . ("！")) - ("!!" . ("‼")) - ("?" . ("？")) - ("??" . ("⁇")) - ("?!" . ("‽" "⁈")) - ("!?" . ("⁉")) - ("die" . ,(agda-input-to-string-list "⚀⚁⚂⚃⚄⚅")) - ("asterisk" . ,(agda-input-to-string-list "⁎⁑⁂✢✣✤✥✱✲✳✺✻✼✽❃❉❊❋＊")) - ("8<" . ("✂" "✄")) - ("tie" . ("⁀")) - ("undertie" . ("‿")) - ("apl" . ,(agda-input-to-string-list "⌶⌷⌸⌹⌺⌻⌼⌽⌾⌿⍀⍁⍂⍃⍄⍅⍆⍇⍈ - ⍉⍊⍋⍌⍍⍎⍏⍐⍑⍒⍓⍔⍕⍖⍗⍘⍙⍚⍛ - ⍜⍝⍞⍟⍠⍡⍢⍣⍤⍥⍦⍧⍨⍩⍪⍫⍬⍭⍮ - ⍯⍰⍱⍲⍳⍴⍵⍶⍷⍸⍹⍺⎕")) - ("#" . ("＃")) - ("%" . ("％")) - ("&" . ("＆")) - ("*" . ("＊")) - ("/" . ,(agda-input-to-string-list "／＼")) - ("@" . ("＠")) - ("__" . ("＿")) - ("\"" . ("＂")) - - ;; Some combining characters. - ;; - ;; The following combining characters also have (other) - ;; translations: - ;; ̀ ́ ̂ ̃ ̄ ̆ ̇ ̈ ̋ ̌ ̣ ̧ ̱ - - ("^--" . ,(agda-input-to-string-list"̅̿")) - ("_--" . ,(agda-input-to-string-list"̲̳")) - ("^~" . ,(agda-input-to-string-list"̃͌")) - ("_~" . ( "̰")) - ("^." . ,(agda-input-to-string-list"̇̈⃛⃜")) - ("_." . ,(agda-input-to-string-list"̣̤")) - ("^l" . ,(agda-input-to-string-list"⃖⃐⃔")) - ("^l-" . ( "⃖")) - ("^r" . ,(agda-input-to-string-list"⃗⃑⃕")) - ("^r-" . ( "⃗")) - ("^lr" . ( "⃡")) - ("_lr" . ( "͍")) - ("^^" . ,(agda-input-to-string-list"̂̑͆")) - ("_^" . ,(agda-input-to-string-list"̭̯̪")) - ("^v" . ,(agda-input-to-string-list"̌̆")) - ("_v" . ,(agda-input-to-string-list"̬̮̺")) - - ;; Shorter forms of many greek letters plus ƛ. - - ("Ga" . ("α")) ("GA" . ("Α")) - ("Gb" . ("β")) ("GB" . ("Β")) - ("Gg" . ("γ")) ("GG" . ("Γ")) - ("Gd" . ("δ")) ("GD" . ("Δ")) - ("Ge" . ("ε")) ("GE" . ("Ε")) - ("Gz" . ("ζ")) ("GZ" . ("Ζ")) - ("Gh" . ("η")) ("GH" . ("Η")) - ("Gth" . ("θ")) ("GTH" . ("Θ")) - ("Gi" . ("ι")) ("GI" . ("Ι")) - ("Gk" . ("κ")) ("GK" . ("Κ")) - ("Gl" . ("λ")) ("GL" . ("Λ")) ("Gl-" . ("ƛ")) - ("Gm" . ("μ")) ("GM" . ("Μ")) - ("Gn" . ("ν")) ("GN" . ("Ν")) - ("Gx" . ("ξ")) ("GX" . ("Ξ")) - ;; \omicron \Omicron - ;; \pi \Pi - ("Gr" . ("ρ")) ("GR" . ("Ρ")) - ("Gs" . ("σ")) ("GS" . ("Σ")) - ("Gt" . ("τ")) ("GT" . ("Τ")) - ("Gu" . ("υ")) ("GU" . ("Υ")) - ("Gf" . ("φ")) ("GF" . ("Φ")) - ("Gc" . ("χ")) ("GC" . ("Χ")) - ("Gp" . ("ψ")) ("GP" . ("Ψ")) - ("Go" . ("ω")) ("GO" . ("Ω")) - - ;; Mathematical characters - - ("MiA" . ("𝐴")) - ("MiB" . ("𝐵")) - ("MiC" . ("𝐶")) - ("MiD" . ("𝐷")) - ("MiE" . ("𝐸")) - ("MiF" . ("𝐹")) - ("MiG" . ("𝐺")) - ("MiH" . ("𝐻")) - ("MiI" . ("𝐼")) - ("MiJ" . ("𝐽")) - ("MiK" . ("𝐾")) - ("MiL" . ("𝐿")) - ("MiM" . ("𝑀")) - ("MiN" . ("𝑁")) - ("MiO" . ("𝑂")) - ("MiP" . ("𝑃")) - ("MiQ" . ("𝑄")) - ("MiR" . ("𝑅")) - ("MiS" . ("𝑆")) - ("MiT" . ("𝑇")) - ("MiU" . ("𝑈")) - ("MiV" . ("𝑉")) - ("MiW" . ("𝑊")) - ("MiX" . ("𝑋")) - ("MiY" . ("𝑌")) - ("MiZ" . ("𝑍")) - ("Mia" . ("𝑎")) - ("Mib" . ("𝑏")) - ("Mic" . ("𝑐")) - ("Mid" . ("𝑑")) - ("Mie" . ("𝑒")) - ("Mif" . ("𝑓")) - ("Mig" . ("𝑔")) - ("Mih" . ("ℎ")) - ("Mii" . ("𝑖")) - ("Mij" . ("𝑗")) - ("Mik" . ("𝑘")) - ("Mil" . ("𝑙")) - ("Mim" . ("𝑚")) - ("Min" . ("𝑛")) - ("Mio" . ("𝑜")) - ("Mip" . ("𝑝")) - ("Miq" . ("𝑞")) - ("Mir" . ("𝑟")) - ("Mis" . ("𝑠")) - ("Mit" . ("𝑡")) - ("Miu" . ("𝑢")) - ("Miv" . ("𝑣")) - ("Miw" . ("𝑤")) - ("Mix" . ("𝑥")) - ("Miy" . ("𝑦")) - ("Miz" . ("𝑧")) - ("MIA" . ("𝑨")) - ("MIB" . ("𝑩")) - ("MIC" . ("𝑪")) - ("MID" . ("𝑫")) - ("MIE" . ("𝑬")) - ("MIF" . ("𝑭")) - ("MIG" . ("𝑮")) - ("MIH" . ("𝑯")) - ("MII" . ("𝑰")) - ("MIJ" . ("𝑱")) - ("MIK" . ("𝑲")) - ("MIL" . ("𝑳")) - ("MIM" . ("𝑴")) - ("MIN" . ("𝑵")) - ("MIO" . ("𝑶")) - ("MIP" . ("𝑷")) - ("MIQ" . ("𝑸")) - ("MIR" . ("𝑹")) - ("MIS" . ("𝑺")) - ("MIT" . ("𝑻")) - ("MIU" . ("𝑼")) - ("MIV" . ("𝑽")) - ("MIW" . ("𝑾")) - ("MIX" . ("𝑿")) - ("MIY" . ("𝒀")) - ("MIZ" . ("𝒁")) - ("MIa" . ("𝒂")) - ("MIb" . ("𝒃")) - ("MIc" . ("𝒄")) - ("MId" . ("𝒅")) - ("MIe" . ("𝒆")) - ("MIf" . ("𝒇")) - ("MIg" . ("𝒈")) - ("MIh" . ("𝒉")) - ("MIi" . ("𝒊")) - ("MIj" . ("𝒋")) - ("MIk" . ("𝒌")) - ("MIl" . ("𝒍")) - ("MIm" . ("𝒎")) - ("MIn" . ("𝒏")) - ("MIo" . ("𝒐")) - ("MIp" . ("𝒑")) - ("MIq" . ("𝒒")) - ("MIr" . ("𝒓")) - ("MIs" . ("𝒔")) - ("MIt" . ("𝒕")) - ("MIu" . ("𝒖")) - ("MIv" . ("𝒗")) - ("MIw" . ("𝒘")) - ("MIx" . ("𝒙")) - ("MIy" . ("𝒚")) - ("MIz" . ("𝒛")) - ("McA" . ("𝒜")) - ("McB" . ("ℬ")) - ("McC" . ("𝒞")) - ("McD" . ("𝒟")) - ("McE" . ("ℰ")) - ("McF" . ("ℱ")) - ("McG" . ("𝒢")) - ("McH" . ("ℋ")) - ("McI" . ("ℐ")) - ("McJ" . ("𝒥")) - ("McK" . ("𝒦")) - ("McL" . ("ℒ")) - ("McM" . ("ℳ")) - ("McN" . ("𝒩")) - ("McO" . ("𝒪")) - ("McP" . ("𝒫")) - ("McQ" . ("𝒬")) - ("McR" . ("ℛ")) - ("McS" . ("𝒮")) - ("McT" . ("𝒯")) - ("McU" . ("𝒰")) - ("McV" . ("𝒱")) - ("McW" . ("𝒲")) - ("McX" . ("𝒳")) - ("McY" . ("𝒴")) - ("McZ" . ("𝒵")) - ("Mca" . ("𝒶")) - ("Mcb" . ("𝒷")) - ("Mcc" . ("𝒸")) - ("Mcd" . ("𝒹")) - ("Mce" . ("ℯ")) - ("Mcf" . ("𝒻")) - ("Mcg" . ("ℊ")) - ("Mch" . ("𝒽")) - ("Mci" . ("𝒾")) - ("Mcj" . ("𝒿")) - ("Mck" . ("𝓀")) - ("Mcl" . ("𝓁")) - ("Mcm" . ("𝓂")) - ("Mcn" . ("𝓃")) - ("Mco" . ("ℴ")) - ("Mcp" . ("𝓅")) - ("Mcq" . ("𝓆")) - ("Mcr" . ("𝓇")) - ("Mcs" . ("𝓈")) - ("Mct" . ("𝓉")) - ("Mcu" . ("𝓊")) - ("Mcv" . ("𝓋")) - ("Mcw" . ("𝓌")) - ("Mcx" . ("𝓍")) - ("Mcy" . ("𝓎")) - ("Mcz" . ("𝓏")) - ("MCA" . ("𝓐")) - ("MCB" . ("𝓑")) - ("MCC" . ("𝓒")) - ("MCD" . ("𝓓")) - ("MCE" . ("𝓔")) - ("MCF" . ("𝓕")) - ("MCG" . ("𝓖")) - ("MCH" . ("𝓗")) - ("MCI" . ("𝓘")) - ("MCJ" . ("𝓙")) - ("MCK" . ("𝓚")) - ("MCL" . ("𝓛")) - ("MCM" . ("𝓜")) - ("MCN" . ("𝓝")) - ("MCO" . ("𝓞")) - ("MCP" . ("𝓟")) - ("MCQ" . ("𝓠")) - ("MCR" . ("𝓡")) - ("MCS" . ("𝓢")) - ("MCT" . ("𝓣")) - ("MCU" . ("𝓤")) - ("MCV" . ("𝓥")) - ("MCW" . ("𝓦")) - ("MCX" . ("𝓧")) - ("MCY" . ("𝓨")) - ("MCZ" . ("𝓩")) - ("MCa" . ("𝓪")) - ("MCb" . ("𝓫")) - ("MCc" . ("𝓬")) - ("MCd" . ("𝓭")) - ("MCe" . ("𝓮")) - ("MCf" . ("𝓯")) - ("MCg" . ("𝓰")) - ("MCh" . ("𝓱")) - ("MCi" . ("𝓲")) - ("MCj" . ("𝓳")) - ("MCk" . ("𝓴")) - ("MCl" . ("𝓵")) - ("MCm" . ("𝓶")) - ("MCn" . ("𝓷")) - ("MCo" . ("𝓸")) - ("MCp" . ("𝓹")) - ("MCq" . ("𝓺")) - ("MCr" . ("𝓻")) - ("MCs" . ("𝓼")) - ("MCt" . ("𝓽")) - ("MCu" . ("𝓾")) - ("MCv" . ("𝓿")) - ("MCw" . ("𝔀")) - ("MCx" . ("𝔁")) - ("MCy" . ("𝔂")) - ("MCz" . ("𝔃")) - ("MfA" . ("𝔄")) - ("MfB" . ("𝔅")) - ("MfC" . ("ℭ")) - ("MfD" . ("𝔇")) - ("MfE" . ("𝔈")) - ("MfF" . ("𝔉")) - ("MfG" . ("𝔊")) - ("MfH" . ("ℌ")) - ("MfI" . ("ℑ")) - ("MfJ" . ("𝔍")) - ("MfK" . ("𝔎")) - ("MfL" . ("𝔏")) - ("MfM" . ("𝔐")) - ("MfN" . ("𝔑")) - ("MfO" . ("𝔒")) - ("MfP" . ("𝔓")) - ("MfQ" . ("𝔔")) - ("MfR" . ("ℜ")) - ("MfS" . ("𝔖")) - ("MfT" . ("𝔗")) - ("MfU" . ("𝔘")) - ("MfV" . ("𝔙")) - ("MfW" . ("𝔚")) - ("MfX" . ("𝔛")) - ("MfY" . ("𝔜")) - ("MfZ" . ("ℨ")) - ("Mfa" . ("𝔞")) - ("Mfb" . ("𝔟")) - ("Mfc" . ("𝔠")) - ("Mfd" . ("𝔡")) - ("Mfe" . ("𝔢")) - ("Mff" . ("𝔣")) - ("Mfg" . ("𝔤")) - ("Mfh" . ("𝔥")) - ("Mfi" . ("𝔦")) - ("Mfj" . ("𝔧")) - ("Mfk" . ("𝔨")) - ("Mfl" . ("𝔩")) - ("Mfm" . ("𝔪")) - ("Mfn" . ("𝔫")) - ("Mfo" . ("𝔬")) - ("Mfp" . ("𝔭")) - ("Mfq" . ("𝔮")) - ("Mfr" . ("𝔯")) - ("Mfs" . ("𝔰")) - ("Mft" . ("𝔱")) - ("Mfu" . ("𝔲")) - ("Mfv" . ("𝔳")) - ("Mfw" . ("𝔴")) - ("Mfx" . ("𝔵")) - ("Mfy" . ("𝔶")) - ("Mfz" . ("𝔷")) - - ;; (Sub / Super) scripts - ;; - ;; Unicode 12.1 omits several latin characters from sub/superscript. - ;; https://www.quora.com/Why-is-there-no-character-for-superscript-q-in-Unicode - ;; - ;; Perhaps they will be added in future versions, however there are no - ;; proposals for it currently in the pipeline: - ;; https://www.unicode.org/alloc/Pipeline.html - - ("_a" . ("ₐ")) - ;; ("_b" . ("b")) - ;; ("_c" . ("c")) - ;; ("_d" . ("d")) - ("_e" . ("ₑ")) - ;; ("_f" . ("f")) - ;; ("_g" . ("g")) - ("_h" . ("ₕ")) - ("_i" . ("ᵢ")) - ("_j" . ("ⱼ")) - ("_k" . ("ₖ")) - ("_l" . ("ₗ")) - ("_m" . ("ₘ")) - ("_n" . ("ₙ")) - ("_o" . ("ₒ")) - ("_p" . ("ₚ")) - ;; ("_q" . ("q")) - ("_r" . ("ᵣ")) - ("_s" . ("ₛ")) - ("_t" . ("ₜ")) - ("_u" . ("ᵤ")) - ("_v" . ("ᵥ")) - ;; ("_w" . ("w")) - ("_x" . ("ₓ")) - ;; ("_y" . ("y")) - ;; ("_z" . ("z")) - - ("_Gb" . ("ᵦ")) - ("_Gg" . ("ᵧ")) - ("_Gr" . ("ᵨ")) - ("_Gf" . ("ᵩ")) - ("_Gc" . ("ᵪ")) - - ("^a" . ("ᵃ")) - ("^b" . ("ᵇ")) - ("^c" . ("ᶜ")) - ("^d" . ("ᵈ")) - ("^e" . ("ᵉ")) - ("^f" . ("ᶠ")) - ("^g" . ("ᵍ")) - ("^h" . ("ʰ")) - ("^i" . ("ⁱ")) - ("^j" . ("ʲ")) - ("^k" . ("ᵏ")) - ("^l" . ("ˡ")) - ("^m" . ("ᵐ")) - ("^n" . ("ⁿ")) - ("^o" . ("ᵒ")) - ("^p" . ("ᵖ")) - ;; ("^q" . ("q")) - ("^r" . ("ʳ")) - ("^s" . ("ˢ")) - ("^t" . ("ᵗ")) - ("^u" . ("ᵘ")) - ("^v" . ("ᵛ")) - ("^w" . ("ʷ")) - ("^x" . ("ˣ")) - ("^y" . ("ʸ")) - ("^z" . ("ᶻ")) - - ("^A" . ("ᴬ")) - ("^B" . ("ᴮ")) - ;; ("^C" . ("C")) - ("^D" . ("ᴰ")) - ("^E" . ("ᴱ")) - ;; ("^F" . ("F")) - ("^G" . ("ᴳ")) - ("^H" . ("ᴴ")) - ("^I" . ("ᴵ")) - ("^J" . ("ᴶ")) - ("^K" . ("ᴷ")) - ("^L" . ("ᴸ")) - ("^M" . ("ᴹ")) - ("^N" . ("ᴺ")) - ("^O" . ("ᴼ")) - ("^P" . ("ᴾ")) - ;; ("^Q" . ("Q")) - ("^R" . ("ᴿ")) - ;; ("^S" . ("S")) - ("^T" . ("ᵀ")) - ("^U" . ("ᵁ")) - ("^V" . ("ⱽ")) - ("^W" . ("ᵂ")) - ;; ("^X" . ("X")) - ;; ("^Y" . ("Y")) - ;; ("^Z" . ("Z")) - - ("^Gb" . ("ᵝ")) - ("^Gg" . ("ᵞ")) - ("^Gd" . ("ᵟ")) - ("^Ge" . ("ᵋ")) - ("^Gth" . ("ᶿ")) - ("^Gf" . ("ᵠ")) - ("^Gc" . ("ᵡ")) - - ;; Some ISO8859-1 characters. - - (" " . (" ")) - ("!" . ("¡")) - ("cent" . ("¢")) - ("brokenbar" . ("¦")) - ("degree" . ("°")) - ("?" . ("¿")) - ("^a_" . ("ª")) - ("^o_" . ("º")) - - ;; Circled, parenthesised etc. numbers and letters. - - ( "(0)" . ,(agda-input-to-string-list " ⓪🄀⓿🄋🄌")) - ( "(1)" . ,(agda-input-to-string-list "⑴①⒈❶➀➊")) - ( "(2)" . ,(agda-input-to-string-list "⑵②⒉❷➁➋")) - ( "(3)" . ,(agda-input-to-string-list "⑶③⒊❸➂➌")) - ( "(4)" . ,(agda-input-to-string-list "⑷④⒋❹➃➍")) - ( "(5)" . ,(agda-input-to-string-list "⑸⑤⒌❺➄➎")) - ( "(6)" . ,(agda-input-to-string-list "⑹⑥⒍❻➅➏")) - ( "(7)" . ,(agda-input-to-string-list "⑺⑦⒎❼➆➐")) - ( "(8)" . ,(agda-input-to-string-list "⑻⑧⒏❽➇➑")) - ( "(9)" . ,(agda-input-to-string-list "⑼⑨⒐❾➈➒")) - ("(10)" . ,(agda-input-to-string-list "⑽⑩⒑❿➉➓")) - ("(11)" . ,(agda-input-to-string-list "⑾⑪⒒⓫")) - ("(12)" . ,(agda-input-to-string-list "⑿⑫⒓⓬")) - ("(13)" . ,(agda-input-to-string-list "⒀⑬⒔⓭")) - ("(14)" . ,(agda-input-to-string-list "⒁⑭⒕⓮")) - ("(15)" . ,(agda-input-to-string-list "⒂⑮⒖⓯")) - ("(16)" . ,(agda-input-to-string-list "⒃⑯⒗⓰")) - ("(17)" . ,(agda-input-to-string-list "⒄⑰⒘⓱")) - ("(18)" . ,(agda-input-to-string-list "⒅⑱⒙⓲")) - ("(19)" . ,(agda-input-to-string-list "⒆⑲⒚⓳")) - ("(20)" . ,(agda-input-to-string-list "⒇⑳⒛⓴")) - - ("(a)" . ,(agda-input-to-string-list "⒜Ⓐⓐ🅐🄰🅰")) - ("(b)" . ,(agda-input-to-string-list "⒝Ⓑⓑ🅑🄱🅱")) - ("(c)" . ,(agda-input-to-string-list "⒞Ⓒⓒ🅒🄲🅲")) - ("(d)" . ,(agda-input-to-string-list "⒟Ⓓⓓ🅓🄳🅳")) - ("(e)" . ,(agda-input-to-string-list "⒠Ⓔⓔ🅔🄴🅴")) - ("(f)" . ,(agda-input-to-string-list "⒡Ⓕⓕ🅕🄵🅵")) - ("(g)" . ,(agda-input-to-string-list "⒢Ⓖⓖ🅖🄶🅶")) - ("(h)" . ,(agda-input-to-string-list "⒣Ⓗⓗ🅗🄷🅷")) - ("(i)" . ,(agda-input-to-string-list "⒤Ⓘⓘ🅘🄸🅸")) - ("(j)" . ,(agda-input-to-string-list "⒥Ⓙⓙ🅙🄹🅹")) - ("(k)" . ,(agda-input-to-string-list "⒦Ⓚⓚ🅚🄺🅺")) - ("(l)" . ,(agda-input-to-string-list "⒧Ⓛⓛ🅛🄻🅻")) - ("(m)" . ,(agda-input-to-string-list "⒨Ⓜⓜ🅜🄼🅼")) - ("(n)" . ,(agda-input-to-string-list "⒩Ⓝⓝ🅝🄽🅽")) - ("(o)" . ,(agda-input-to-string-list "⒪Ⓞⓞ🅞🄾🅾")) - ("(p)" . ,(agda-input-to-string-list "⒫Ⓟⓟ🅟🄿🅿")) - ("(q)" . ,(agda-input-to-string-list "⒬Ⓠⓠ🅠🅀🆀")) - ("(r)" . ,(agda-input-to-string-list "⒭Ⓡⓡ🅡🅁🆁")) - ("(s)" . ,(agda-input-to-string-list "⒮Ⓢⓢ🅢🅂🆂")) - ("(t)" . ,(agda-input-to-string-list "⒯Ⓣⓣ🅣🅃🆃")) - ("(u)" . ,(agda-input-to-string-list "⒰Ⓤⓤ🅤🅄🆄")) - ("(v)" . ,(agda-input-to-string-list "⒱Ⓥⓥ🅥🅅🆅")) - ("(w)" . ,(agda-input-to-string-list "⒲Ⓦⓦ🅦🅆🆆")) - ("(x)" . ,(agda-input-to-string-list "⒳Ⓧⓧ🅧🅇🆇")) - ("(y)" . ,(agda-input-to-string-list "⒴Ⓨⓨ🅨🅈🆈")) - ("(z)" . ,(agda-input-to-string-list "⒵Ⓩⓩ🅩🅉🆉")) - - )) - "A list of translations specific to the Agda input method. -Each element is a pair (KEY-SEQUENCE-STRING . LIST-OF-TRANSLATION-STRINGS). -All the translation strings are possible translations -of the given key sequence; if there is more than one you can choose -between them using the arrow keys. - -Note that if you customize this setting you will not -automatically benefit (or suffer) from modifications to its -default value when the library is updated. If you just want to -add some bindings it is probably a better idea to customize -`agda-input-user-translations'. - -These translation pairs are included after those in -`agda-input-user-translations', but before the ones inherited -from other input methods (see `agda-input-inherit'). - -If you change this setting manually (without using the -customization buffer) you need to call `agda-input-setup' in -order for the change to take effect." - :group 'agda-input - :set 'agda-input-incorporate-changed-setting - :initialize 'custom-initialize-default - :type '(repeat (cons (string :tag "Key sequence") - (repeat :tag "Translations" string)))) - -(defcustom agda-input-user-translations nil - "Like `agda-input-translations', but more suitable for user -customizations since by default it is empty. - -These translation pairs are included first, before those in -`agda-input-translations' and the ones inherited from other input -methods." - :group 'agda-input - :set 'agda-input-incorporate-changed-setting - :initialize 'custom-initialize-default - :type '(repeat (cons (string :tag "Key sequence") - (repeat :tag "Translations" string)))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Inspecting and modifying translation maps - -(defun agda-input-get-translations (qp) - "Return a list containing all translations from the Quail -package QP (except for those corresponding to ASCII). -Each pair in the list has the form (KEY-SEQUENCE . TRANSLATION)." - (with-temp-buffer - (activate-input-method qp) ; To make sure that the package is loaded. - (unless (quail-package qp) - (error "%s is not a Quail package." qp)) - (let ((decode-map (list 'decode-map))) - (quail-build-decode-map (list (quail-map)) "" decode-map 0) - (cdr decode-map)))) - -(defun agda-input-show-translations (qp) - "Display all translations used by the Quail package QP (a string). -\(Except for those corresponding to ASCII)." - (interactive (list (read-input-method-name - "Quail input method (default %s): " "Agda"))) - (let ((buf (concat "*" qp " input method translations*"))) - (with-output-to-temp-buffer buf - (with-current-buffer buf - (quail-insert-decode-map - (cons 'decode-map (agda-input-get-translations qp))))))) - -(defun agda-input-add-translations (trans) - "Add the given translations TRANS to the Agda input method. -TRANS is a list of pairs (KEY-SEQUENCE . TRANSLATION). The -translations are appended to the current translations." - (with-temp-buffer - (dolist (tr (agda-input-concat-map (eval agda-input-tweak-all) trans)) - (quail-defrule (car tr) (cdr tr) "Agda" t)))) - -(defun agda-input-inherit-package (qp &optional fun) - "Let the Agda input method inherit the translations from the -Quail package QP (except for those corresponding to ASCII). - -The optional function FUN can be used to modify the translations. -It is given a pair (KEY-SEQUENCE . TRANSLATION) and should return -a list of such pairs." - (let ((trans (agda-input-get-translations qp))) - (agda-input-add-translations - (if fun (agda-input-concat-map fun trans) - trans)))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Setting up the input method - -(defun agda-input-setup () - "Set up the Agda input method based on the customisable -variables and underlying input methods." - - ;; Create (or reset) the input method. - (with-temp-buffer - (quail-define-package "Agda" "UTF-8" "∏" t ; guidance - "Agda input method. -The purpose of this input method is to edit Agda programs, but -since it is highly customisable it can be made useful for other -tasks as well." - nil nil nil nil nil nil t ; maximum-shortest - )) - - (agda-input-add-translations - (mapcar (lambda (tr) (cons (car tr) (vconcat (cdr tr)))) - (append agda-input-user-translations - agda-input-translations))) - (dolist (def agda-input-inherit) - (agda-input-inherit-package (car def) - (eval (cdr def))))) - -(defun agda-input-incorporate-changed-setting (sym val) - "Update the Agda input method based on the customisable -variables and underlying input methods. -Suitable for use in the :set field of `defcustom'." - (set-default sym val) - (agda-input-setup)) - -;; Set up the input method. - -(agda-input-setup) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Administrative details - -(provide 'agda-input) -;;; agda-input.el ends here diff --git a/src/data/emacs-mode/agda2-abbrevs.el b/src/data/emacs-mode/agda2-abbrevs.el deleted file mode 100644 index c6b04466..00000000 --- a/src/data/emacs-mode/agda2-abbrevs.el +++ /dev/null @@ -1,106 +0,0 @@ -;; agda2-abbrevs.el --- Default Agda abbrevs -;; SPDX-License-Identifier: MIT License - -;;; Commentary: - -;;; Code: - -;; Skeletons - -(require 'skeleton) - -(define-skeleton agda2-abbrevs-module - "Inserts a module header template." - nil - "module " _ " where\n") - -(define-skeleton agda2-abbrevs-data - "Inserts a data template." - nil - "data " _ " : Set where\n") - -(define-skeleton agda2-abbrevs-record - "Inserts a record type template." - nil - "record " _ " : Set where\n" - " field\n") - -(define-skeleton agda2-abbrevs-record-value - "Inserts a record value template." - nil - "record {" _ "}") - -(define-skeleton agda2-abbrevs-using - "Inserts a using template." - nil - "using (" _ ")") - -(define-skeleton agda2-abbrevs-hiding - "Inserts a hiding template." - nil - "hiding (" _ ")") - -(define-skeleton agda2-abbrevs-renaming - "Inserts a renaming template." - nil - "renaming (" _ " to " _ ")") - -(define-skeleton agda2-abbrevs-forall - "Inserts a forall template." - nil - "∀ {" _ "} ") - -(define-skeleton agda2-abbrevs-code-block - "Inserts a code block." - nil - "\\begin{code}\n " _ "\n\\end{code}\n") - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Abbrevs - -(defvar agda2-abbrevs-defaults '( - ("m" "" agda2-abbrevs-module) - ("d" "" agda2-abbrevs-data) - ("c" "" agda2-abbrevs-code-block) - ("re" "" agda2-abbrevs-record) - ("rec" "" agda2-abbrevs-record-value) - ("u" "" agda2-abbrevs-using) - ("h" "" agda2-abbrevs-hiding) - ("r" "" agda2-abbrevs-renaming) - ("w" "where\n") - ("po" "postulate") - ("a" "abstract\n") - ("pr" "private\n") - ("pu" "public") - ("mu" "mutual\n") - ("f" "" agda2-abbrevs-forall) - ("oi" "open import ")) - "Abbreviations defined by default in the Agda mode.") - -(defcustom agda2-mode-abbrevs-use-defaults nil - "If non-nil include the default Agda mode abbrevs in `agda2-mode-abbrev-table'. -The abbrevs are designed to be expanded explicitly, so users of `abbrev-mode' -probably do not want to include them. - -Restart Emacs in order for this change to take effect." - :group 'agda2 - :type '(choice (const :tag "Yes" t) - (const :tag "No" nil))) - -(defvar agda2-mode-abbrev-table nil - "Agda mode abbrev table.") - -(define-abbrev-table - 'agda2-mode-abbrev-table - (if agda2-mode-abbrevs-use-defaults - (mapcar (lambda (abbrev) - (append abbrev - (make-list (- 4 (length abbrev)) nil) - '((:system t)))) - agda2-abbrevs-defaults))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Administrative details - -(provide 'agda2-abbrevs) -;;; agda2-abbrevs.el ends here diff --git a/src/data/emacs-mode/agda2-highlight.el b/src/data/emacs-mode/agda2-highlight.el deleted file mode 100644 index 73cbcdd5..00000000 --- a/src/data/emacs-mode/agda2-highlight.el +++ /dev/null @@ -1,596 +0,0 @@ -;;; agda2-highlight.el --- Syntax highlighting for Agda (version ≥ 2) -;; SPDX-License-Identifier: MIT License - -;;; Commentary: - -;; Code to apply syntactic highlighting to Agda source code. This uses -;; Agda's own annotations to figure out what is what, so the parsing -;; is always done correctly, but highlighting is not done on the fly. - -;;; Code: - -(require 'annotation) -(require 'font-lock) - -(defgroup agda2-highlight nil - "Syntax highlighting for Agda." - :group 'agda2) - -(defcustom agda2-highlight-level 'non-interactive - "How much syntax highlighting should be produced? -Interactive highlighting includes highlighting of the expression -that is currently being type-checked." - :type '(choice - (const :tag "None" none) - (const :tag "Non-interactive" non-interactive) - (const :tag "Interactive" interactive)) - :group 'agda2-highlight) - -(defun agda2-highlight-level nil - "Formats the highlighting level in a Haskelly way." - (cond ((equal agda2-highlight-level 'none) "None") - ((equal agda2-highlight-level 'non-interactive) "NonInteractive") - ((equal agda2-highlight-level 'interactive) "Interactive") - (t "None"))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Functions for setting faces - -(defun agda2-highlight-set-face-attribute (face attrs) - "Reset (globally) all attributes of the face FACE according to ATTRS. -If the face does not exist, then it is created first." - (make-face face) - (set-face-attribute face nil - :family 'unspecified - :width 'unspecified - :height 'unspecified - :weight 'unspecified - :slant 'unspecified - :foreground 'unspecified - :background 'unspecified - :inverse-video 'unspecified - :stipple 'unspecified - :underline 'unspecified - :overline 'unspecified - :strike-through 'unspecified - :inherit 'unspecified - :box 'unspecified - :font 'unspecified) - (eval `(set-face-attribute face nil ,@attrs))) - -(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." - (set-default variable group) - (mapc (lambda (face-and-attrs) - (agda2-highlight-set-face-attribute - (car face-and-attrs) (cdr face-and-attrs))) - (cond - ((equal group 'conor) - '((agda2-highlight-keyword-face - :bold t) - (agda2-highlight-string-face - :foreground "firebrick3") - (agda2-highlight-number-face - :foreground "firebrick3") - (agda2-highlight-symbol-face - :foreground "grey25") - (agda2-highlight-primitive-type-face - :foreground "medium blue") - (agda2-highlight-bound-variable-face - :foreground "purple") - (agda2-highlight-generalizable-variable-face - :foreground "purple") - (agda2-highlight-inductive-constructor-face - :foreground "firebrick3") - (agda2-highlight-coinductive-constructor-face - :foreground "firebrick3") - (agda2-highlight-datatype-face - :foreground "medium blue") - (agda2-highlight-field-face - :foreground "deeppink") - (agda2-highlight-function-face - :foreground "darkgreen") - (agda2-highlight-module-face - :foreground "medium blue") - (agda2-highlight-postulate-face - :foreground "darkgreen") - (agda2-highlight-primitive-face - :foreground "darkgreen") - (agda2-highlight-macro-face - :foreground "aquamarine4") - (agda2-highlight-record-face - :foreground "medium blue") - (agda2-highlight-dotted-face) - (agda2-highlight-error-face - :foreground "red" - :underline t) - (agda2-highlight-error-warning-face - :background "light coral" - :underline t) - (agda2-highlight-unsolved-meta-face - :foreground "black" - :background "yellow") - (agda2-highlight-unsolved-constraint-face - :foreground "black" - :background "yellow") - (agda2-highlight-termination-problem-face - :foreground "black" - :background "light salmon") - (agda2-highlight-positivity-problem-face - :foreground "black" - :background "peru") - (agda2-highlight-incomplete-pattern-face - :foreground "black" - :background "purple") - (agda2-highlight-typechecks-face - :foreground "black" - :background "light blue"))) - ((equal group 'default-faces) - (list (cons 'agda2-highlight-keyword-face - (list :inherit font-lock-keyword-face)) - (cons 'agda2-highlight-string-face - (list :inherit font-lock-string-face)) - (cons 'agda2-highlight-number-face - (list :inherit font-lock-constant-face)) - (cons 'agda2-highlight-symbol-face - (list :inherit font-lock-keyword-face)) - (cons 'agda2-highlight-primitive-type-face - (list :inherit font-lock-keyword-face)) - (cons 'agda2-highlight-bound-variable-face - (list :inherit font-lock-variable-name-face)) - (cons 'agda2-highlight-generalizable-variable-face - (list :inherit font-lock-variable-name-face)) - (cons 'agda2-highlight-inductive-constructor-face - (list :inherit font-lock-type-face)) - (cons 'agda2-highlight-coinductive-constructor-face - (list :inherit font-lock-type-face)) - (cons 'agda2-highlight-datatype-face - (list :inherit font-lock-type-face)) - (cons 'agda2-highlight-field-face - (list :inherit font-lock-variable-name-face)) - (cons 'agda2-highlight-function-face - (list :inherit font-lock-function-name-face)) - (cons 'agda2-highlight-module-face - (list :inherit font-lock-type-face)) - (cons 'agda2-highlight-postulate-face - (list :inherit font-lock-type-face)) - (cons 'agda2-highlight-primitive-face - (list :inherit font-lock-constant-face)) - (cons 'agda2-highlight-macro-face - (list :inherit font-lock-function-name-face)) - (cons 'agda2-highlight-record-face - (list :inherit font-lock-variable-name-face)) - (cons 'agda2-highlight-dotted-face - (list :inherit font-lock-variable-name-face)) - (cons 'agda2-highlight-operator-face - (list :inherit font-lock-function-name-face)) - (cons 'agda2-highlight-error-face - (list :inherit font-lock-warning-face)) - (cons 'agda2-highlight-typechecks-face - (list :inherit font-lock-type-face)) - (cons 'agda2-highlight-typechecking-face - (list :inherit font-lock-preprocessor-face))))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Faces - -(defcustom agda2-highlight-face-groups nil - "Colour scheme used in Agda buffers. -Changes to this variable may not take full effect until you have -restarted Emacs. Note also that if you are using the -default-faces option and change your colour theme, then the -changes may not take effect in Agda buffers until you have -restarted Emacs." - :type '(choice - (const :tag "Use the settings in the \"Agda2 Highlight Faces\" subgroup." nil) - (const :tag "Use an approximation of Conor McBride's colour scheme." - conor) - (const :tag "Use simplified highlighting and default font-lock faces." - default-faces)) - :group 'agda2-highlight - :set 'agda2-highlight-set-faces) - -(defgroup agda2-highlight-faces nil - "Faces used to highlight Agda code. -If `agda2-highlight-face-groups' is nil." - :group 'agda2-highlight) - -(defface agda2-highlight-keyword-face - '((((background light)) - (:foreground "DarkOrange3")) - (((background dark)) - (:foreground "#FF9932"))) - "The face used for keywords." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-string-face - '((((background light)) - (:foreground "firebrick")) - (((background dark)) - (:foreground "#DD4D4D"))) - "The face used for strings." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-number-face - '((((background light)) - (:foreground "purple")) - (((background dark)) - (:foreground "#9010E0"))) - "The face used for numbers." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-symbol-face - '((((background light)) - (:foreground "gray25")) - (((background dark)) - (:foreground "gray75"))) - "The face used for symbols like forall, =, ->, etc." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-primitive-type-face - '((((background light)) - (:foreground "medium blue")) - (((background dark)) - (:foreground "#8080FF"))) - "The face used for primitive types (like Set and Prop)." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-bound-variable-face - '((t nil)) - "The face used for bound variables." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-generalizable-variable-face - '((t nil)) - "The face used for generalizable variables." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-inductive-constructor-face - '((((background light)) - :foreground "green4") - (((background dark)) - :foreground "#29CC29")) - "The face used for inductive constructors." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-coinductive-constructor-face - '((((background light)) - :foreground "gold4") - (((background dark)) - :foreground "#FFEA75")) - "The face used for coinductive constructors." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-datatype-face - '((((background light)) - (:foreground "medium blue")) - (((background dark)) - (:foreground "#8080FF"))) - "The face used for datatypes." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-field-face - '((((background light)) - (:foreground "DeepPink2")) - (((background dark)) - (:foreground "#F570B7"))) - "The face used for record fields." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-function-face - '((((background light)) - (:foreground "medium blue")) - (((background dark)) - (:foreground "#8080FF"))) - "The face used for functions." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-module-face - '((((background light)) - (:foreground "purple")) - (((background dark)) - (:foreground "#CD80FF"))) - "The face used for module names." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-postulate-face - '((((background light)) - (:foreground "medium blue")) - (((background dark)) - (:foreground "#8080FF"))) - "The face used for postulates." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-pragma-face - '((t nil)) - "The face used for (some text in) pragmas." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-primitive-face - '((((background light)) - (:foreground "medium blue")) - (((background dark)) - (:foreground "#8080FF"))) - "The face used for primitive functions." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-macro-face - '((((background light)) - (:foreground "aquamarine4")) - (((background dark)) - (:foreground "#73BAA2"))) - "The face used for macros." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-record-face - '((((background light)) - (:foreground "medium blue")) - (((background dark)) - (:foreground "#8080FF"))) - "The face used for record types." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-dotted-face - '((t nil)) - "The face used for dotted patterns." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-operator-face - '((t nil)) - "The face used for operators." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-error-face - '((((background light)) - (:foreground "red" :underline t)) - (((background dark)) - (:foreground "#FF0000" :underline t))) - "The face used for errors." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-error-warning-face - '((((background light)) - (:background "light coral" :underline t)) - (((background dark)) - (:background "#802400" :underline t))) - "The face used for fatal warnings." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-unsolved-meta-face - '((((background light)) - (:background "yellow")) - (((background dark)) - (:background "#806B00"))) - "The face used for unsolved meta variables." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-unsolved-constraint-face - '((((background light)) - (:background "yellow")) - (((background dark)) - (:background "#806B00"))) - "The face used for unsolved constraints which are not connected to metas." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-termination-problem-face - '((((background light)) - (:background "light salmon")) - (((background dark)) - (:background "#802400"))) - "The face used for termination problems." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-positivity-problem-face - '((((background light)) - (:background "peru")) - (((background dark)) - (:background "#803F00"))) - "The face used for positivity problems." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-deadcode-face - '((((background light)) - (:background "dark gray")) - (((background dark)) - (:background "#808080"))) - "The face used for dead code (unreachable clauses, etc.)." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-shadowing-in-telescope-face - '((((background light)) - (:background "dark gray")) - (((background dark)) - (:background "#808080"))) - "The face used for shadowed repeated variable names in telescopes." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-coverage-problem-face - '((((background light)) - (:background "wheat")) - (((background dark)) - (:background "#805300"))) - "The face used for coverage problems." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-catchall-clause-face - '((((background light)) - (:background "white smoke")) - (((background dark)) - (:background "#404040"))) - "The face used for catchall clauses." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-confluence-problem-face - '((((background light)) - (:background "pink")) - (((background dark)) - (:background "#800080"))) - "The face used for confluence problems." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-missing-definition-face - '((((background light)) - (:background "orange")) - (((background dark)) - (:background "#804040"))) - "The face used for type declarations with missing definitions." - :group 'agda2-highlight-faces) - -(defface agda2-highlight-typechecks-face - '((((background light)) - (:background "light blue" :foreground "black")) - (((background dark)) - (:background "#006080" :foreground "white"))) - "The face used for code which is being type-checked." - :group 'agda2-highlight-faces) - -(defvar agda2-highlight-faces - '((keyword . agda2-highlight-keyword-face) - (comment . font-lock-comment-face) - (background . default) - (markup . font-lock-comment-delimiter-face) - (string . agda2-highlight-string-face) - (number . agda2-highlight-number-face) - (symbol . agda2-highlight-symbol-face) - (primitivetype . agda2-highlight-primitive-type-face) - (bound . agda2-highlight-bound-variable-face) - (generalizable . agda2-highlight-generalizable-variable-face) - (inductiveconstructor . agda2-highlight-inductive-constructor-face) - (coinductiveconstructor . agda2-highlight-coinductive-constructor-face) - (datatype . agda2-highlight-datatype-face) - (field . agda2-highlight-field-face) - (function . agda2-highlight-function-face) - (module . agda2-highlight-module-face) - (postulate . agda2-highlight-postulate-face) - (pragma . agda2-highlight-pragma-face) - (primitive . agda2-highlight-primitive-face) - (macro . agda2-highlight-macro-face) - (record . agda2-highlight-record-face) - (dotted . agda2-highlight-dotted-face) - (operator . agda2-highlight-operator-face) - (error . agda2-highlight-error-face) - (errorwarning . agda2-highlight-error-warning-face) - (unsolvedmeta . agda2-highlight-unsolved-meta-face) - (unsolvedconstraint . agda2-highlight-unsolved-constraint-face) - (terminationproblem . agda2-highlight-termination-problem-face) - (deadcode . agda2-highlight-deadcode-face) - (shadowingintelescope . agda2-highlight-shadowing-in-telescope-face) - (coverageproblem . agda2-highlight-coverage-problem-face) - (positivityproblem . agda2-highlight-positivity-problem-face) - (incompletepattern . agda2-highlight-incomplete-pattern-face) - (catchallclause . agda2-highlight-catchall-clause-face) - (confluenceproblem . agda2-highlight-confluence-problem-face) - (missingdefinition . agda2-highlight-missing-definition-face) - (typechecks . agda2-highlight-typechecks-face)) - "Alist mapping code aspects to the face used when displaying them. - -The aspects currently recognised are the following: - -`background' Non-Agda code contents in literate mode. -`bound' Bound variables. -`catchallclause' Clause not holding definitionally. -`coinductiveconstructor' Coinductive constructors. -`comment' Comments. -`coverageproblem' Coverage problems. -`datatype' Data types. -`deadcode' Deadcode (like unreachable clauses or RHS). -`dotted' Dotted patterns. -`error' Errors. -`errorwarning' Fatal warnings. -`field' Record fields. -`function' Functions. -`generalizable' Generalizable variables. -`incompletepattern' Incomplete patterns. -`inductiveconstructor' Inductive constructors. -`keyword' Keywords. -`macro' Macros. -`markup' Delimiters to separate the Agda code blocks - from other contents. -`module' Module names. -`number' Numbers. -`operator' Operators. -`positivityproblem' Positivity problems. -`postulate' Postulates. -`pragma' Text occurring in pragmas that does not have - a more specific (syntactic) aspect. -`primitive' Primitive functions. -`primitivetype' Primitive types (like Set and Prop). -`record' Record types. -`shadowingintelescope' Shadowed repeated variable names in telescopes. -`string' Strings. -`symbol' Symbols like forall, =, ->, etc. -`terminationproblem' Termination problems. -`typechecks' Code which is being type-checked. -`unsolvedconstraint' Unsolved constraints, not connected to meta - variables. -`unsolvedmeta' Unsolved meta variables.") - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Variables - -(defvar agda2-highlight-in-progress nil - "If nil, then highlighting annotations are not applied.") -(make-variable-buffer-local 'agda2-highlight-in-progress) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Functions - -(defun agda2-highlight-setup nil - "Set up the `annotation' library for use with `agda2-mode'." - (agda2-highlight-set-faces 'agda2-highlight-face-groups agda2-highlight-face-groups) - (setq annotation-bindings agda2-highlight-faces)) - -(defun agda2-highlight-apply (remove &rest cmds) - "Adds the syntax highlighting information in the annotation list CMDS. - -If REMOVE is nil, then old syntax highlighting information is not -removed. Otherwise all token-based syntax highlighting is removed." - (let (;; Ignore read-only status, otherwise this function may fail. - (inhibit-read-only t)) - (apply 'annotation-load - "Click mouse-2 to jump to definition" - remove - cmds))) - -(defun agda2-highlight-add-annotations (remove &rest cmds) - "Like `agda2-highlight-apply'. -But only if `agda2-highlight-in-progress' is non-nil." - (if agda2-highlight-in-progress - (apply 'agda2-highlight-apply remove cmds))) - -(defun agda2-highlight-load (file) - "Load syntax highlighting information from FILE. - -Old syntax highlighting information is not removed." - (let* ((coding-system-for-read 'utf-8) - (cmds (with-temp-buffer - (insert-file-contents file) - (goto-char (point-min)) - (read (current-buffer))))) - (apply 'agda2-highlight-apply cmds))) - -(defun agda2-highlight-load-and-delete-action (file) - "Like `agda2-highlight-load', but deletes FILE when done. -And highlighting is only updated if `agda2-highlight-in-progress' -is non-nil." - (unwind-protect - (if agda2-highlight-in-progress - (agda2-highlight-load file)) - (delete-file file))) - -(defun agda2-highlight-clear (&optional token-based) - "Remove all syntax highlighting. - -If TOKEN-BASED is non-nil, then only token-based highlighting is -removed." - (interactive) - (let ((inhibit-read-only t)) - ; Ignore read-only status, otherwise this function may fail. - (annotation-remove-annotations token-based))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Administrative details - -(provide 'agda2-highlight) -;;; agda2-highlight.el ends here diff --git a/src/data/emacs-mode/agda2-mode-pkg.el b/src/data/emacs-mode/agda2-mode-pkg.el deleted file mode 100644 index 3bd1da96..00000000 --- a/src/data/emacs-mode/agda2-mode-pkg.el +++ /dev/null @@ -1,3 +0,0 @@ -(define-package "agda2-mode" "2.6.4" - "interactive development for Agda, a dependently typed functional programming language" - '((emacs "24.3"))) ;; dep defs for `annotation.el` and `eri.el` are not required if they are packaged together diff --git a/src/data/emacs-mode/agda2-mode.el b/src/data/emacs-mode/agda2-mode.el deleted file mode 100644 index 85ce62a1..00000000 --- a/src/data/emacs-mode/agda2-mode.el +++ /dev/null @@ -1,2063 +0,0 @@ -;;; agda2-mode.el --- Major mode for agda2hs -;; SPDX-License-Identifier: MIT License - -;;; Commentary: - -;; A major mode for editing Agda (the dependently typed programming -;; language / interactive theorem prover). -;; -;; Modified to work with agda2hs, a new backend compiling -;; lightly annotated Agda code to readable Haskell. -;; -;; Major features include: -;; -;; - syntax highlighting. -;; -;; - on the fly Agda interpretation. -;; -;; - goal-driven development -;; -;; - interactive case-splitting -;; -;; - proof search -;; -;; - input support (for utf8 characters) -;; -;; see https://agda.readthedocs.io/ for more information - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;; Dependency - - -;;; Code: - -(defvar agda2-version "2.6.4" - "The version of the Agda mode. -Note that the same version of the Agda executable must be used.") - -(require 'cl-lib) -(require 'compile) -(require 'pp) -(require 'time-date) -(require 'eri) -(require 'annotation) -(require 'fontset) -(require 'agda-input) -(require 'agda2) -(require 'agda2-highlight) -(require 'agda2-abbrevs) -(require 'agda2-queue) -(eval-and-compile - ;; Load filladapt, if it is installed. - (condition-case nil - (require 'filladapt) - (error nil)) - (unless (fboundp 'overlays-in) (load "overlay")) ; for Xemacs - (unless (fboundp 'propertize) ; for Xemacs 21.4 - ;; FIXME: XEmacs-21.4 (patch 22) does have `propertize' and so does Emacs-22 - ;; (and agda2-mode doesn't work in Emacs-21, AFAICT). - (defun propertize (string &rest properties) - "Return a copy of STRING with text properties added. -First argument is the string to copy. -Remaining arguments form a sequence of PROPERTY VALUE pairs for text -properties to add to the result." - (let ((str (copy-sequence string))) - (add-text-properties 0 (length str) properties str) - str))) - (unless (fboundp 'prog-mode) ;For Emacs<24. - (defalias 'prog-mode 'fundamental-mode))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;; Utilities - -(defmacro agda2-let (varbind funcbind &rest body) - "Expands to (let* VARBIND (cl-labels FUNCBIND BODY...)). -Or possibly (let* VARBIND (labels FUNCBIND BODY...))." - (declare (debug ((&rest [&or symbolp (symbolp form)]) - (&rest (cl-defun)) - body)) - (indent 2)) - ;; Use cl-labels if available to avoid obsolescence warnings. - `(let* ,varbind (,(if (fboundp 'cl-labels) 'cl-labels 'labels) ,funcbind ,@body))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;; User options - -(defgroup agda2 nil - "Major mode for interactively developing Agda programs." - :group 'languages) - -(defcustom agda2-program-name "agda2hs" - "The name of the Agda executable." - :type 'string - :group 'agda2) - -(defcustom agda2-program-args - '("--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. - -The flag \"--interaction\" is always included as the first -argument, and does not need to be listed here." - :type '(repeat string) - :group 'agda2) - -(defvar agda2-backends '("AGDA2HS" "GHC" "GHCNoMain" "JS" "LaTeX" "QuickLaTeX") - "Compilation backends.") - -(defcustom agda2-backend - "" - "The backend used to compile Agda programs (leave blank to ask every time)." - :type 'string - :group 'agda2) - -(defcustom agda2-information-window-max-height - 0.35 - "The maximum height of the information window. -A multiple of the frame height." - :type 'number - :group 'agda2) - -(defcustom agda2-fontset-name - (unless (or (eq window-system 'mac) - ;; Emacs-23 uses a revamped font engine which should - ;; make agda2-fontset-name unnecessary in most cases. - ;; And if it turns out to be necessary, we should - ;; probably use face-remapping-alist rather than - ;; set-frame-font so the special font only applies to - ;; Agda buffers, and so it applies in all frames where - ;; Agda buffers are displayed. - (boundp 'face-remapping-alist)) - "fontset-agda2") - "Default font to use in the selected frame when activating the Agda mode. -This is only used if it's non-nil and Emacs is not running in a -terminal. - -Note that this setting (if non-nil) affects non-Agda buffers as -well, and that you have to restart Emacs if you want settings to -this variable to take effect." - :type '(choice (string :tag "Fontset name") - (const :tag "Do not change the font" nil)) - :group 'agda2) - -(defcustom agda2-fontset-spec-of-fontset-agda2 - "-*-fixed-Medium-r-Normal-*-18-*-*-*-c-*-fontset-agda2, - ascii:-Misc-Fixed-Medium-R-Normal--18-120-100-100-C-90-ISO8859-1, - latin-iso8859-2:-*-Fixed-*-r-*-*-18-*-*-*-c-*-iso8859-2, - latin-iso8859-3:-*-Fixed-*-r-*-*-18-*-*-*-c-*-iso8859-3, - latin-iso8859-4:-*-Fixed-*-r-*-*-18-*-*-*-c-*-iso8859-4, - cyrillic-iso8859-5:-*-Fixed-*-r-*-*-18-*-*-*-c-*-iso8859-5, - greek-iso8859-7:-*-Fixed-*-r-*-*-18-*-*-*-c-*-iso8859-7, - latin-iso8859-9:-*-Fixed-*-r-*-*-18-*-*-*-c-*-iso8859-9, - mule-unicode-0100-24ff:-Misc-Fixed-Medium-R-Normal--18-120-100-100-C-90-ISO10646-1, - mule-unicode-2500-33ff:-Misc-Fixed-Medium-R-Normal--18-120-100-100-C-90-ISO10646-1, - mule-unicode-e000-ffff:-Misc-Fixed-Medium-R-Normal--18-120-100-100-C-90-ISO10646-1, - japanese-jisx0208:-Misc-Fixed-Medium-R-Normal-ja-18-*-*-*-C-*-JISX0208.1990-0, - japanese-jisx0212:-Misc-Fixed-Medium-R-Normal-ja-18-*-*-*-C-*-JISX0212.1990-0, - thai-tis620:-Misc-Fixed-Medium-R-Normal--24-240-72-72-C-120-TIS620.2529-1, - lao:-Misc-Fixed-Medium-R-Normal--24-240-72-72-C-120-MuleLao-1, - tibetan:-TibMdXA-fixed-medium-r-normal--16-160-72-72-m-160-MuleTibetan-0, - tibetan-1-column:-TibMdXA-fixed-medium-r-normal--16-160-72-72-m-80-MuleTibetan-1, - korean-ksc5601:-Daewoo-Mincho-Medium-R-Normal--16-120-100-100-C-160-KSC5601.1987-0, - chinese-gb2312:-ISAS-Fangsong ti-Medium-R-Normal--16-160-72-72-c-160-GB2312.1980-0, - chinese-cns11643-1:-HKU-Fixed-Medium-R-Normal--16-160-72-72-C-160-CNS11643.1992.1-0, - chinese-big5-1:-ETen-Fixed-Medium-R-Normal--16-150-75-75-C-160-Big5.ETen-0, - chinese-big5-2:-ETen-Fixed-Medium-R-Normal--16-150-75-75-C-160-Big5.ETen-0" - "Specification of the \"fontset-agda2\" fontset. -This fontset is only created if `agda2-fontset-name' is -\"fontset-agda2\" and Emacs is not run in a terminal. - -Note that the text \"fontset-agda2\" has to be part of the -string (in a certain way; see the default setting) in order for the -agda2 fontset to be created properly. - -Note also that the default setting may not work unless suitable -fonts are installed on your system. Refer to the README file -accompanying the Agda distribution for more details. - -Note finally that you have to restart Emacs if you want settings -to this variable to take effect." - :group 'agda2 - :type 'string) - -(if (and (equal agda2-fontset-name "fontset-agda2") window-system) - (create-fontset-from-fontset-spec agda2-fontset-spec-of-fontset-agda2 t t)) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;; Global and buffer-local vars, initialization - -(defvar agda2-mode-syntax-table - (let ((tbl (make-syntax-table))) - ;; Set the syntax of every char to "w" except for those whose default - ;; syntax in `standard-syntax-table' is `paren' or `whitespace'. - (map-char-table (lambda (keys val) - ;; `keys' here can be a normal char, a generic char - ;; (Emacs<23), or a char range (Emacs>=23). - (unless (memq (car val) - (eval-when-compile - (mapcar 'car - (list (string-to-syntax "(") - (string-to-syntax ")") - (string-to-syntax " "))))) - (modify-syntax-entry keys "w" tbl))) - (standard-syntax-table)) - ;; Then override the remaining special cases. - (dolist (cs '((?- . "w 12") (?\n . ">") - (?. . ".") (?\; . ".") (?! . "."))) - (modify-syntax-entry (car cs) (cdr cs) tbl)) - tbl) - "Syntax table used by the Agda mode: - -- | Comment character, word constituent. -\n | Comment ender. -.;! | Punctuation. - -Remaining characters inherit their syntax classes from the -standard syntax table if that table treats them as matching -parentheses or whitespace. Otherwise they are treated as word -constituents.") - -(defconst agda2-command-table - `( - (agda2-load "\C-c\C-l" (global) "Load") - (agda2-load "\C-c\C-x\C-l") - (agda2-compile "\C-c\C-x\C-c" (global) "Compile") - (agda2-quit "\C-c\C-x\C-q" (global) "Quit") - (agda2-restart "\C-c\C-x\C-r" (global) "Kill and restart Agda") - (agda2-abort "\C-c\C-x\C-a" (global) "Abort a command") - (agda2-remove-annotations "\C-c\C-x\C-d" (global) "Remove goals and highlighting (\"deactivate\")") - (agda2-display-implicit-arguments "\C-c\C-x\C-h" (global) "Toggle display of hidden arguments") - (agda2-display-irrelevant-arguments "\C-c\C-x\C-i" (global) "Toggle display of irrelevant arguments") - (agda2-show-constraints ,(kbd "C-c C-=") (global) "Show constraints") - (agda2-solve-maybe-all ,(kbd "C-c C-s") (local global) "Solve constraints") - (agda2-show-goals ,(kbd "C-c C-?") (global) "Show goals") - (agda2-next-goal "\C-c\C-f" (global) "Next goal") ; Forward. - (agda2-previous-goal "\C-c\C-b" (global) "Previous goal") ; Back. - (agda2-give ,(kbd "C-c C-SPC") (local) "Give") - (agda2-elaborate-give ,(kbd "C-c C-m") (local) "Elaborate and Give") - (agda2-refine "\C-c\C-r" (local) "Refine") - (agda2-auto-maybe-all "\C-c\C-a" (local global) "Auto") - (agda2-make-case "\C-c\C-c" (local) "Case") - (agda2-goal-type "\C-c\C-t" (local) "Goal type") - (agda2-show-context "\C-c\C-e" (local) "Context (environment)") - (agda2-helper-function-type "\C-c\C-h" (local) "Helper function type") - (agda2-infer-type-maybe-toplevel "\C-c\C-d" (local global) "Infer (deduce) type") - (agda2-why-in-scope-maybe-toplevel "\C-c\C-w" (local global) "Explain why a particular name is in scope") - (agda2-goal-and-context ,(kbd "C-c C-,") (local) "Goal type and context") - (agda2-goal-and-context-and-inferred ,(kbd "C-c C-.") (local) "Goal type, context and inferred type") - (agda2-goal-and-context-and-checked ,(kbd "C-c C-;") (local) "Goal type, context and checked type") - (agda2-search-about-toplevel ,(kbd "C-c C-z") (local global) "Search About") - (agda2-module-contents-maybe-toplevel ,(kbd "C-c C-o") (local global) "Module contents") - (agda2-compute-normalised-maybe-toplevel "\C-c\C-n" (local global) "Evaluate term to normal form") - (describe-char nil (global) "Information about the character at point") - (agda2-comment-dwim-rest-of-buffer ,(kbd "C-c C-x M-;") (global) "Comment/uncomment the rest of the buffer") - (agda2-display-program-version nil (global) "Version") - (agda2-set-program-version "\C-c\C-x\C-s" (global) "Switch to another version of Agda") - (eri-indent ,(kbd "TAB")) - (eri-indent-reverse [S-iso-lefttab]) - (eri-indent-reverse [S-lefttab]) - (eri-indent-reverse [S-tab]) - (agda2-goto-definition-mouse [mouse-2]) - (agda2-goto-definition-keyboard "\M-.") - (agda2-go-back ,(if (version< emacs-version "25.1") "\M-*" "\M-,")) - ) - "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 -menu; and DESC is the description of the command used in the -menus.") - -(defvar agda2-mode-map - (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) - (dolist (d (reverse agda2-command-table)) - (cl-destructuring-bind (f &optional keys kinds desc) d - (if keys (define-key map keys f)) - (if (member 'global kinds) - (define-key map - (vector 'menu-bar 'Agda (intern desc)) (cons desc f))))) - map) - "Keymap for `agda2-mode'.") - -(defvar agda2-goal-map - (let ((map (make-sparse-keymap "Agda goal"))) - (dolist (d (reverse agda2-command-table)) - (cl-destructuring-bind (f &optional keys kinds desc) d - (if (member 'local kinds) - (define-key map - (vector (intern desc)) (cons desc f))))) - map) - "Keymap for agda2 goal menu.") - -(defvar agda2-info-buffer nil - "Agda information buffer.") - -(defvar agda2-process-buffer nil - "Agda subprocess buffer. -Set in `agda2-restart'.") - -(defvar agda2-process nil - "Agda subprocess. -Set in `agda2-restart'.") - -(defvar agda2-in-progress nil - "Is the Agda process currently busy? -Valid values: `nil' (not busy), `busy' (busy), -`not-so-busy' (busy with something that should typically -terminate fairly quickly).") - -;; Some buffer locals -(defvar agda2-buffer-external-status "" - "External status of an `agda2-mode' buffer (dictated by the Haskell side).") -(make-variable-buffer-local 'agda2-buffer-external-status) - -(defvar agda2-output-prompt "Agda2> " - "The Agda2 buffer's prompt.") - -(defconst agda2-help-address - "" - "Address accepting submissions of bug reports and questions.") - -;; Annotation for a goal -;; {! .... !} -;; ---------- overlay: agda2-gn num, face highlight, after-string num, -;; modification-hooks (agda2-protect-goal-markers) -;; - text-props: category agda2-delim1 -;; - text-props: category agda2-delim2 -;; - text-props: category agda2-delim3 -;; - text-props: category agda2-delim4 -;; -;; Char categories for {! ... !} -(defvar agda2-open-brace "{") -(defvar agda2-close-brace " }") -(setplist 'agda2-delim1 `(display ,agda2-open-brace)) -(setplist 'agda2-delim2 `(display ,agda2-open-brace rear-nonsticky t - agda2-delim2 t)) -(setplist 'agda2-delim3 `(display ,agda2-close-brace agda2-delim3 t)) -(setplist 'agda2-delim4 `(display ,agda2-close-brace rear-nonsticky t)) - -;; Note that strings used with the display property are compared by -;; reference. If the agda2-*-brace definitions were inlined, then -;; goals would be displayed as "{{ }}n" instead of "{ }n". - -;; The following variables are used by the filter process, -;; `agda2-output-filter'. Their values are only modified by the filter -;; process, `agda2-go', `agda2-restart', `agda2-abort-highlighting', -;; and `agda2-abort-done'. - -(defvar agda2-output-chunk-incomplete (agda2-queue-empty) - "Buffer for incomplete lines. -\(See `agda2-output-filter'.)") -(make-variable-buffer-local 'agda2-output-chunk-incomplete) - -(defvar agda2-last-responses nil - "Response commands which should be run after other commands. -The command which arrived last is stored first in the list.") -(make-variable-buffer-local 'agda2-last-responses) - -(defvar agda2-file-buffer nil - "The Agda buffer. -Note that this variable is not buffer-local.") - -(defvar agda2-in-agda2-file-buffer nil - "Was `agda2-file-buffer' active when `agda2-output-filter' started? -Note that this variable is not buffer-local.") - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;; agda2-mode - -;;;###autoload -(add-to-list 'auto-mode-alist '("\\.l?agda\\'" . agda2-mode)) -;;;###autoload -(modify-coding-system-alist 'file "\\.l?agda\\'" 'utf-8) -;;;###autoload -(define-derived-mode agda2-mode prog-mode "Agda2Hs" - "Major mode for Agda files. - -The following paragraph does not apply to Emacs 23 or newer. - - Note that when this mode is activated the default font of the - current frame is changed to the fontset `agda2-fontset-name'. - The reason is that Agda programs often use mathematical symbols - and other Unicode characters, so we try to provide a suitable - default font setting, which can display many of the characters - encountered. If you prefer to use your own settings, set - `agda2-fontset-name' to nil. - -Special commands: -\\{agda2-mode-map}" - - (if (boundp 'agda2-include-dirs) - (display-warning 'agda2 "Note that the variable agda2-include-dirs is -no longer used. You may want to update your configuration. You -have at least two choices: -* Use the library management system. -* Set the include path using agda2-program-args. - -One way to avoid seeing this warning is to make sure that -agda2-include-dirs is not bound." :warning)) - - (setq local-abbrev-table agda2-mode-abbrev-table - indent-tabs-mode nil - mode-line-process - '((:eval (unless (eq 0 (length agda2-buffer-external-status)) - (concat ":" agda2-buffer-external-status))))) - (let ((l '(max-specpdl-size 2600 - max-lisp-eval-depth 2800))) - (while l (set (make-local-variable (pop l)) (pop l)))) - (if (and window-system agda2-fontset-name) - (condition-case nil - (set-frame-font agda2-fontset-name) - (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 '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)) - ;; Make sure that Font Lock mode is not used. - (font-lock-mode 0) - (agda2-highlight-setup) - (condition-case err - (agda2-highlight-reload) - (error (message "Highlighting not loaded: %s" - (error-message-string err)))) - (agda2-comments-and-paragraphs-setup) - (force-mode-line-update) - ;; Protect global value of default-input-method from set-input-method. - (make-local-variable 'default-input-method) - ;; Don't take script into account when determining word boundaries - (set (make-local-variable 'word-combining-categories) (cons '(nil . nil) word-combining-categories)) - (set-input-method "Agda") - ;; Highlighting etc. is removed when we switch from the Agda mode. - ;; Use case: When a file M.lagda with a local variables list - ;; including "mode: latex" is loaded chances are that the Agda mode - ;; is activated before the LaTeX mode, and the LaTeX mode does not - ;; seem to remove the text properties set by the Agda mode. - (add-hook 'change-major-mode-hook 'agda2-quit nil 'local)) - -(defun agda2-restart () - "Tries to start or restart the Agda process." - (interactive) - - ;; Kill any running instance of the Agda process. - (condition-case nil - (agda2-term) - (error nil)) - - ;; Check that the right version of Agda is used. - (let* ((coding-system-for-read 'utf-8) - (output (with-output-to-string - (call-process agda2-program-name - nil standard-output nil "--version"))) - (version (and (string-match "^Agda version \\([0-9.]+\\)" output) - (match-string 1 output)))) - (unless (equal version agda2-version) - (error "The Agda mode's version (%s) does not match that of %s (%s)." - agda2-version - agda2-program-name (or version "unknown")))) - - (let ((all-program-args (cons "--interaction" agda2-program-args))) - - ;; Check that the arguments are not malformed. - (let* ((coding-system-for-read 'utf-8) - (status) - (output - (with-output-to-string - (setq status - (apply 'call-process agda2-program-name - nil standard-output nil all-program-args))))) - (unless (equal status 0) - (error "Failed to start the Agda process:\n%s" output))) - - ;; Start the Agda process. - (let ((agda2-bufname "*agda2*")) - - (let ((process-connection-type nil)) ; Pipes are faster than PTYs. - (setq agda2-process - (apply 'start-process "Agda2" agda2-bufname - agda2-program-name all-program-args))) - - (set-process-coding-system agda2-process 'utf-8 'utf-8) - (set-process-query-on-exit-flag agda2-process nil) - (set-process-filter agda2-process 'agda2-output-filter) - (setq agda2-in-progress nil - agda2-file-buffer (current-buffer)) - - (with-current-buffer agda2-bufname - (setq agda2-process-buffer (current-buffer) - mode-name "Agda executable" - agda2-last-responses nil) - (set-buffer-file-coding-system 'utf-8)) - - (agda2-remove-annotations)))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;; Communicating with Agda - -(defun agda2-raise-error () - "Raises an error. -The error message directs the user to the *agda2* buffer." - (error "Problem encountered. The *agda2* buffer can perhaps explain why.")) - -(defun agda2-running-p nil - "Does the *agda2* buffer exist, and is the Agda2 process running?" - (and (buffer-live-p agda2-process-buffer) - (eq (agda2-process-status) 'run))) - -(defun agda2-send-command (restart &rest args) - "Send a command to the Agda process. -Sends the list of strings ARGS to the process. If RESTART is -non-nil and the process is not running, or the *agda2* -buffer does not exist, then an attempt is made to restart the -process." - (when (and restart (not (agda2-running-p))) - ;; Try restarting automatically, but only once, in case there is - ;; some major problem. - (agda2-restart) - (unless (agda2-running-p) - (agda2-raise-error))) - (let ((command (apply 'concat (agda2-intersperse " " args)))) - (with-current-buffer agda2-process-buffer - (goto-char (point-max)) - (insert command) - (insert "\n") - (process-send-string agda2-process (concat command "\n"))))) - -(defun agda2-go (save highlight how-busy do-abort &rest args) - "Executes commands in the Agda2 interpreter. -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 HIGHLIGHT is non-nil, then the buffer's syntax highlighting -may be updated. This is also the case if the Agda process is -busy (or `not-so-busy') and `agda2-highlight-in-process' is -non-nil. - -The value HOW-BUSY should be `busy' if it should not be possible -to invoke other commands while this command is running (with the -exception of commands for which DO-ABORT is nil). Otherwise it -should be `not-so-busy' (which should only be used for commands -that typically terminate fairly quickly). - -If the Agda process is busy (or `not-so-busy'), and the current -buffer does not match `agda2-file-buffer', then the command is -not executed and an error is raised. The same applies if DO-ABORT -is non-nil and the Agda process is `busy'." - - ; Check that how-busy is well-formed. - (cl-assert (or (equal how-busy 'busy) - (equal how-busy 'not-so-busy))) - - (when (and agda2-in-progress - (not (equal agda2-file-buffer - (current-buffer)))) - (error "Agda is busy with something in the buffer %s" - agda2-file-buffer)) - - (when (and do-abort - (equal agda2-in-progress 'busy)) - (error "Agda is busy with something -\(you have the option to abort or restart Agda)")) - - (setq agda2-file-buffer (current-buffer)) - - (setq agda2-highlight-in-progress - (or highlight - (and agda2-in-progress - agda2-highlight-in-progress))) - - (unless agda2-in-progress - (setq agda2-output-chunk-incomplete (agda2-queue-empty))) - - (setq agda2-in-progress - (if (or (equal how-busy 'busy) - (equal agda2-in-progress 'busy)) - 'busy - 'not-so-busy)) - - (when (equal save 'save) (save-buffer)) - - (apply 'agda2-send-command - 'restart - "IOTCM" - (agda2-string-quote (buffer-file-name)) - (if highlight (agda2-highlight-level) "None") - "Indirect" - "(" - (append args '(")")))) - -(defun agda2-abort () - "Tries to abort the current computation, if any. -May be more efficient than restarting Agda." - (interactive) - (agda2-send-command nil - "IOTCM" - (agda2-string-quote (buffer-file-name)) - "None" - "Indirect" - "Cmd_abort")) - -(defun agda2-abort-done () - "Resets certain variables. -Intended to be used by the backend if an abort command was -successful." - (agda2-info-action "*Aborted*" "Aborted." t) - (setq agda2-highlight-in-progress nil - agda2-last-responses nil)) - -(defun agda2-output-filter (proc chunk) - "Evaluate the Agda process's commands. -This filter function assumes that every line contains either some -kind of error message (which cannot be parsed as a list), or -exactly one command. Incomplete lines are stored in a -buffer (`agda2-output-chunk-incomplete'). - -Every command is run by this function, unless it has the form -\"(('last . priority) . cmd)\", in which case it is run by -`agda2-run-last-commands' at the end, after the Agda2 prompt -has reappeared, after all non-last commands, and after all -interactive highlighting is complete. The last commands can have -different integer priorities; those with the lowest priority are -executed first. - -Non-last commands should not call the Agda process. - -All commands are echoed to the *agda2* buffer, with the exception -of commands of the form \"(agda2-highlight-... ...)\". - -The non-last commands are run in the order in which they appear. - -When the prompt has been reached highlighting annotations are -reloaded from `agda2-highlighting-file', unless -`agda2-highlighting-in-progress' is nil." - - ;; Beware: the buffer may have been killed in the mean time. E.g. when - ;; viewing an attachment containing Agda code in Gnus, Gnus will - ;; create a temp buffer, set it in agda2-mode, call font-lock-ensure on it - ;; (which won't know that it needs to wait for some process to reply), then - ;; extract the fontified text and kill the temp buffer; so when Agda - ;; finally answers, the temp buffer is long gone. - (when (buffer-live-p agda2-file-buffer) - (setq agda2-in-agda2-file-buffer - (and agda2-file-buffer - (equal (current-buffer) agda2-file-buffer))) - (let (;; The input lines in the current chunk. - (lines (split-string chunk "\n")) - - ;; Non-last commands found in the current chunk (reversed). - (non-last-commands ()) - - ;; Last incomplete line, if any. - (output-chunk-incomplete "")) - (with-current-buffer agda2-file-buffer - (when (consp lines) - (agda2-queue-enqueue agda2-output-chunk-incomplete (pop lines)) - (when (consp lines) - ;; The previous uncomplete chunk is now complete. - (push (agda2-queue-to-string agda2-output-chunk-incomplete) - lines) - - ;; Stash away the last incomplete line, if any. (Note that - ;; (split-string "...\n" "\n") evaluates to (... "").) - (setq output-chunk-incomplete (car (last lines)) - agda2-output-chunk-incomplete - (agda2-queue-from-string output-chunk-incomplete)) - - ;; Handle every complete line. - (dolist (line (butlast lines)) - (let* (;; The command. Lines which cannot be parsed as a single - ;; list, without any junk, are ignored. - (cmd (condition-case nil - (let ((result (read-from-string line))) - (if (and (listp (car result)) - (= (cdr result) (length line))) - (car result))) - (error nil))) - (is-highlighting-command - (and cmd - (symbolp (car cmd)) - (let ((case-fold-search nil)) - (string-match "^agda2-highlight-" - (symbol-name (car cmd))))))) - - ;; Do not echo highlighting commands. - (unless is-highlighting-command - (with-current-buffer agda2-process-buffer - (save-excursion - (goto-char (point-max)) - (insert line) - (insert "\n")))) - (when cmd - (if (equal 'last (car-safe (car cmd))) - (push (cons (cdr (car cmd)) (cdr cmd)) - agda2-last-responses) - (push cmd non-last-commands))))) - - ;; Run non-last commands. - (mapc 'agda2-exec-response (nreverse non-last-commands))) - - ;; Check if the prompt has been reached. This function assumes - ;; that the prompt does not include any newline characters. - (when (agda2-queue-is-prefix-of agda2-output-prompt - agda2-output-chunk-incomplete) - (with-current-buffer agda2-process-buffer - (insert output-chunk-incomplete)) - (setq agda2-output-chunk-incomplete (agda2-queue-empty) - agda2-in-progress nil - agda2-last-responses (nreverse agda2-last-responses)) - - (agda2-run-last-commands))))))) - -(defun agda2-run-last-commands nil - "Execute the last commands in the right order. -\(After the prompt has reappeared.) See `agda2-output-filter'." - - ;; with-current-buffer is used repeatedly below, because some last - ;; commands may switch the focus to another buffer. - - (while (with-current-buffer agda2-file-buffer - (and (not agda2-in-progress) (consp agda2-last-responses))) - (with-current-buffer agda2-file-buffer - ;; The list is sorted repeatedly because this function may be - ;; called recursively (via `agda2-exec-response'). - (setq agda2-last-responses (sort agda2-last-responses - (lambda (x y) (<= (car x) (car y))))) - (let ((r (pop agda2-last-responses))) - (agda2-exec-response (cdr r))))) - - ;; Unset agda2-highlight-in-progress when all the asynchronous - ;; commands have terminated. - (unless agda2-in-progress - (setq agda2-highlight-in-progress nil))) - -(defun agda2-abort-highlighting nil - "Abort any interactive highlighting. -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." - (buffer-name (current-buffer))))) - -(defun agda2-goal-cmd (cmd save &optional want ask &rest args) - "Reads input from goal or minibuffer and sends command to Agda. - -An error is raised if point is not in a goal. - -The command sent to Agda is - - CMD ARGS. - -The user input is computed as follows: - -* If WANT is nil, then the user input is the empty string. - -* If WANT is a string, and either ASK is non-nil or the goal only - 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 - 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 -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")) - (let ((txt (buffer-substring-no-properties (+ (overlay-start o) 2) - (- (overlay-end o) 2))) - (input-from-goal nil)) - (cond ((null want) (setq txt "")) - ((and (stringp want) - (or ask (string-match "\\`\\s *\\'" txt))) - (setq txt (read-string (concat want ": ") nil nil txt t))) - (t (setq input-from-goal t))) - (apply 'agda2-go save input-from-goal 'busy t cmd - (format "%d" g) - (if input-from-goal (agda2-goal-Range o) (agda2-mkRange nil)) - (agda2-string-quote txt) args)))) - -;; Note that the following function is a security risk, since it -;; evaluates code without first inspecting it. The code (supposedly) -;; comes from the Agda backend, but there could be bugs in the backend -;; which can be exploited by an attacker which manages to trick -;; someone into type-checking compromised Agda code. - -(defun agda2-exec-response (response) - "Interprets response." - (let ((inhibit-read-only t)) - (eval response))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;; User commands and response processing - -(defun agda2-load () - "Load current buffer." - (interactive) - (agda2-go 'save t 'busy t "Cmd_load" - (agda2-string-quote (buffer-file-name)) - (agda2-list-quote agda2-program-args) - )) - -(defun agda2-compile () - "Compile the current module. - -The variable `agda2-backend' determines which backend is used." - (interactive) - (let ((backend (cond ((equal agda2-backend "MAlonzo") "GHC") - ((equal agda2-backend "MAlonzoNoMain") "GHCNoMain") - ((equal agda2-backend "") - (completing-read "Backend: " agda2-backends - nil nil nil nil nil - 'inherit-input-method)) - (t agda2-backend)))) - (when (equal backend "") (error "No backend chosen")) - (agda2-go 'save t 'busy t "Cmd_compile" - backend - (agda2-string-quote (buffer-file-name)) - (agda2-list-quote agda2-program-args) - ))) - -(defmacro agda2-maybe-forced (name comment cmd save want) - "This macro constructs a function NAME which runs CMD. -COMMENT is used to build the function's comment. The function -NAME takes a prefix argument which tells whether it should -apply force or not when running CMD (through -`agda2-goal-cmd'; -SAVE is used as `agda2-goal-cmd's SAVE argument and -WANT is used as `agda2-goal-cmd's WANT argument)." - (let ((eval (make-symbol "eval"))) - `(defun ,name (&optional prefix) - ,(concat comment ". - -The action depends on the prefix argument: - -* If the prefix argument is `nil' (i.e., if no prefix argument is - given), then no force is applied. - -* If any other prefix argument is used (for instance, if C-u is - typed once or twice right before the command is invoked), then - force is applied.") - (interactive "P") - (let ((,eval (cond ((equal prefix nil) "WithoutForce") - ("WithForce")))) - (agda2-goal-cmd (concat ,cmd " " ,eval) - ,save ,want))))) - -(agda2-maybe-forced - agda2-give - "Give to the goal at point the expression in it" - "Cmd_give" - 'save - "expression to give") - -;; (defun agda2-give() -;; "Give to the goal at point the expression in it" (interactive) -;; (agda2-goal-cmd "Cmd_give" 'save "expression to give")) - -(defun agda2-give-action (old-g paren) - "Update the goal OLD-G with the expression in it." - (let - ;; Don't run modification hooks: we don't want this to - ;; trigger agda2-abort-highlighting. - ((inhibit-modification-hooks t)) - (agda2-update old-g paren))) - -(defun agda2-refine (pmlambda) - "Refine the goal at point. -If the goal contains an expression e, and some \"suffix\" of the -type of e unifies with the goal type, then the goal is replaced -by e applied to a suitable number of new goals. - -PMLAMBDA is only used if the goal has a functional type. -When the prefix argument is given a pattern maching lambda will -be inserted, otherwise a standard lambda will be used. - -If the goal is empty, the goal type is a data type, and there is -exactly one constructor which unifies with this type, then the -goal is replaced by the constructor applied to a suitable number -of new goals." - (interactive "P") - (if pmlambda - (agda2-goal-cmd "Cmd_refine_or_intro True" 'save 'goal) - (agda2-goal-cmd "Cmd_refine_or_intro False" 'save 'goal))) - -(defun agda2-autoOne () - "Simple proof search" (interactive) - (agda2-goal-cmd "Cmd_autoOne" 'save 'goal)) - -(defun agda2-autoAll () - "Solves all goals by simple proof search." - (interactive) - (agda2-go nil nil 'busy t "Cmd_autoAll") -) - -(defun agda2-make-case () - "Refine the pattern variables given in the goal. -Assumes that = {!!} is on one line." - (interactive) - (agda2-goal-cmd "Cmd_make_case" 'save "pattern variables to case (empty for split on result)")) - -(defun agda2-make-case-action (newcls) - "Replace the line at point with new clauses NEWCLS and reload." - (agda2-forget-all-goals);; we reload later anyway. - (let* ((p0 (point)) - (p1 (goto-char (+ (current-indentation) (line-beginning-position)))) - (indent (current-column)) - cl) - (delete-region p1 (line-end-position)) - (while (setq cl (pop newcls)) - (insert cl) - (if newcls (insert "\n" (make-string indent ? )))) - (goto-char p0)) - (agda2-load)) - -(defun agda2-make-case-action-extendlam (newcls) - "Replace definition of extended lambda with new clauses NEWCLS and reload." - (agda2-forget-all-goals);; we reload later anyway. - (let* ((p0 (point)) - (pmax (re-search-forward "!}")) - (bracketCount 0) - (p1 (goto-char (+ (current-indentation) (line-beginning-position)))) - (indent (current-column)) - cl) - (goto-char p0) - (re-search-backward "{!") - (while (and (not (equal (preceding-char) ?\;)) (>= bracketCount 0) (> (point) p1)) - (backward-char) - (if (equal (preceding-char) ?}) (cl-incf bracketCount)) - (if (equal (preceding-char) ?{) (cl-decf bracketCount))) - (let* ((is-lambda-where (= (point) p1)) - (p (point))) - (delete-region (point) pmax) - (if (not is-lambda-where) (insert " ")) - (while (setq cl (pop newcls)) - (insert cl) - (if newcls (if is-lambda-where (insert "\n" (make-string indent ? )) (insert " ; ")))) - (goto-char p))) - (agda2-load)) - -(defun agda2-status-action (status) - "Display the string STATUS in the current buffer's mode line. -\(precondition: the current buffer has to use the Agda mode as the -major mode)." - (setq agda2-buffer-external-status status) - (force-mode-line-update)) - -(defmacro agda2-information-buffer (buffer kind title) - "Used to define functions like `agda2-info-buffer'." - `(defun ,buffer nil - ,(concat "Creates the Agda " kind - " buffer, if it does not already exist. -The buffer is returned.") - (unless (buffer-live-p ,buffer) - (setq ,buffer - (generate-new-buffer ,title)) - - (with-current-buffer ,buffer - (compilation-mode "AgdaInfo") - ;; Support for jumping to positions mentioned in the text. - (set (make-local-variable 'compilation-error-regexp-alist) - '(("\\([\\\\/][^[:space:]]*\\):\\([0-9]+\\),\\([0-9]+\\)-\\(\\([0-9]+\\),\\)?\\([0-9]+\\)" - 1 (2 . 5) (3 . 6)))) - ;; Do not skip errors that start in the same position as the - ;; current one. - (set (make-local-variable 'compilation-skip-to-next-location) nil) - ;; No support for recompilation. The key binding is removed, and - ;; attempts to run `recompile' will (hopefully) result in an - ;; error. - (let ((map (copy-keymap (current-local-map)))) - (define-key map (kbd "g") 'undefined) - (use-local-map map)) - (set (make-local-variable 'compile-command) - 'agda2-does-not-support-compilation-via-the-compilation-mode) - - (set-syntax-table agda2-mode-syntax-table) - (set (make-local-variable 'word-combining-categories) (cons '(nil . nil) word-combining-categories)) - (set-input-method "Agda"))) - - ,buffer)) - -(agda2-information-buffer agda2-info-buffer "info" "*Agda information*") - -(defun agda2-info-action (name text &optional append) - "Insert TEXT into the Agda info buffer and display it. -NAME is displayed in the buffer's mode line. - -If APPEND is non-nil, then TEXT is appended at the end of the -buffer, and point placed after this text. - -If APPEND is nil, then any previous text is removed before TEXT -is inserted, and point is placed before this text." - (interactive) - (let ((buf (agda2-info-buffer))) - (with-current-buffer buf - ;; In some cases the jump-to-position-mentioned-in-text - ;; functionality (see compilation-error-regexp-alist above) - ;; didn't work: Emacs jumped to the wrong position. However, it - ;; seems to work if compilation-forget-errors is used. This - ;; problem may be related to Emacs bug #9679 - ;; (http://debbugs.gnu.org/cgi/bugreport.cgi?bug=9679). The idea - ;; to use compilation-forget-errors comes from a comment due to - ;; Oleksandr Manzyuk - ;; (https://github.com/haskell/haskell-mode/issues/67). - (compilation-forget-errors) - (unless append (erase-buffer)) - (save-excursion - (goto-char (point-max)) - (insert text)) - (put-text-property 0 (length name) 'face '(:weight bold) name) - (setq mode-line-buffer-identification name) - (force-mode-line-update)) - ;; If the current window displays the information buffer, then the - ;; window configuration is left untouched. - (unless (equal (window-buffer) buf) - (let ((agda-window - (and agda2-file-buffer - (car-safe - ;; All windows, including minibuffers, on any - ;; frame on the current terminal, displaying the - ;; present Agda file buffer. - (get-buffer-window-list agda2-file-buffer t 0))))) - (save-selected-window - ;; Select a window displaying the Agda file buffer (if such - ;; a window exists). With certain configurations of - ;; display-buffer this should increase the likelihood that - ;; the info buffer will be displayed on the same frame. - (when agda-window - (select-window agda-window 'no-record)) - (let* (;; If there is only one window, then the info window - ;; should be created above or below the code window, - ;; not to the left or right. - (split-width-threshold nil) - (window - (display-buffer - buf - ;; Under Emacs 23 the effect of the following - ;; argument is only that the current window - ;; should not be used. - '(nil - . - (;; Do not use the same window. - (inhibit-same-window . t) - ;; Do not raise or select another frame. - (inhibit-switch-frame . t)))))) - (if window - (fit-window-to-buffer window - (truncate - (* (frame-height) - agda2-information-window-max-height)))))))) - ;; Move point in every window displaying the information buffer. - ;; Exception: If we are appending, don't move point in selected - ;; windows. - (dolist (window (get-buffer-window-list buf 'no-minibuffer t)) - (unless (and append - (equal window (selected-window))) - (with-selected-window window - (if append - (goto-char (point-max)) - (goto-char (point-min)))))))) - -(defun agda2-info-action-and-copy (name text &optional append) - "Same as agda2-info-action but also puts TEXT in the kill ring." - (kill-new text) - (agda2-info-action name text append)) - -(defun agda2-show-constraints() - "Show constraints." (interactive) - (agda2-go nil t 'busy t "Cmd_constraints")) - -(defun agda2-remove-annotations () - "Removes buffer annotations (overlays and text properties)." - (interactive) - (dolist (o (overlays-in (point-min) (point-max))) - (delete-overlay o)) - (let ((inhibit-read-only t)) - (annotation-preserve-mod-p-and-undo - (set-text-properties (point-min) (point-max) '())) - (force-mode-line-update))) - -(defun agda2-next-goal () "Go to the next goal, if any." (interactive) - (agda2-mv-goal 'next-single-property-change 'agda2-delim2 1 (point-min))) -(defun agda2-previous-goal () "Go to the previous goal, if any." (interactive) - (agda2-mv-goal 'previous-single-property-change 'agda2-delim3 0 (point-max))) -(defun agda2-mv-goal (change delim adjust wrapped) - (agda2-let () - ((go (p) (while (and (setq p (funcall change p 'category)) - (not (eq (get-text-property p 'category) delim)))) - (if p (goto-char (+ adjust p))))) - (or (go (point)) (go wrapped) (message "No goals in the buffer")))) - -(defun agda2-quit () - "Quit and clean up after agda2." - (interactive) - (remove-hook 'first-change-hook 'agda2-abort-highlighting 'local) - (remove-hook 'after-save-hook 'agda2-highlight-tokens 'local) - (agda2-remove-annotations) - (agda2-term)) - -(defun agda2-term (&optional nicely) - "Interrupt the Agda process and kill its buffer. -If this function is invoked with a prefix argument, then Agda is -asked nicely to terminate itself after any previously invoked -commands have completed." - (interactive "P") - (if nicely - (progn - ;; Set up things so that if the Agda process terminates, then - ;; its buffer is killed. - (when (and agda2-process - (process-status agda2-process)) - (set-process-sentinel agda2-process 'agda2-kill-process-buffer)) - ;; Kill the process buffer if the Agda process has already - ;; been killed. - (agda2-kill-process-buffer) - ;; Try to kill the Agda process. - (agda2-send-command nil - "IOTCM" - (agda2-string-quote (buffer-file-name)) - "None" - "Indirect" - "Cmd_exit")) - ;; Try to kill the Agda process and the process buffer. - (when (and agda2-process - (process-status agda2-process)) - (interrupt-process agda2-process)) - (when (buffer-live-p agda2-process-buffer) - (kill-buffer agda2-process-buffer)))) - -(defun agda2-kill-process-buffer (&optional process event) - "Kills the Agda process buffer, if any. -But only if the Agda process does not exist or has terminated. - -This function can be used as a process sentinel." - (when (and (or (null agda2-process) - (member (process-status agda2-process) - '(exit signal failed nil))) - (buffer-live-p agda2-process-buffer)) - (kill-buffer agda2-process-buffer))) - -(cl-defmacro agda2--with-gensyms ((&rest names) &body body) - "Bind NAMES to fresh symbols in BODY" - (declare (indent 1)) - `(let ,(cl-loop for x in names collecting `(,x (make-symbol (symbol-name',x)))) - ,@body)) - -;; This macro is meant to be used to generate other macros which define -;; functions which can be used either directly from a goal or at a global -;; level and are modifiable using one of three levels of normalisation. - -(defmacro agda2-proto-maybe-normalised (name comment cmd norm0 norm1 norm2 norm3 spec) - "This macro constructs a function NAME which runs CMD. -COMMENT is used to build the function's comment. -The function NAME takes a prefix argument which tells whether it -should normalise types according to either NORM0, NORM1, NORM2, or NORM3 -when running CMD through `agda2-goal-cmd`. -SPEC can be either (fromgoal want) or (global prompt). -" - - ;; Names bound in a macro should be ``uninterned'' to avoid name capture - ;; We use the macro `agda2--with-gensyms' to bind these. - (agda2--with-gensyms (eval prefix args) - `(defun ,name (,prefix &rest ,args) - ,(format "%s. - -The form of the result depends on the prefix argument: - -* If the prefix argument is `nil' (i.e., if no prefix argument is - given), then the result is %s. - -* If the prefix argument is `(4)' (for instance if C-u is typed - exactly once right before the command is invoked), then the - result is %s. - -* If the prefix argument is `(16)' (for instance if C-u is typed - exactly twice right before the command is invoked), then the - result is %s. - -* If any other prefix argument is used (for instance if C-u is - typed thrice right before the command is invoked), then the - result is %s." comment (nth 1 norm0) (nth 1 norm1) (nth 1 norm2) (nth 1 norm3)) - - ;; All the commands generated by the macro are interactive. - ;; Those called from a goal, grab the value present there (if any) - ;; Whereas those called globally always use a prompt - (interactive ,(pcase spec - (`(fromgoal ,want) - "P") - (`(global ,prompt) - (if prompt - (concat "P\nM" prompt ": ") - "P")))) - ;; Depending on the prefix's value we pick one of the three - ;; normalisation levels - (let ((,eval (cond ((null ,prefix) - ,(car norm0)) - ((equal ,prefix '(4)) - ,(car norm1)) - ((equal ,prefix '(16)) - ,(car norm2)) - (t ,(car norm3))))) - ;; Finally, if the command is called from a goal, we use `agda2-goal-cmd' - ;; Otherwise we resort to `agda2-go' - ,(pcase spec - (`(fromgoal ,want) - `(agda2-goal-cmd (concat ,cmd " " ,eval) nil ,want)) - (`(global ,prompt) - `(agda2-go nil t 'busy t - (concat ,cmd " " - ,eval " " - (if ,prompt - (agda2-string-quote (car ,args)) - ""))))))))) - -(defmacro agda2-maybe-normalised (name comment cmd want) - `(agda2-proto-maybe-normalised - ,name ,comment ,cmd - ("Simplified" "simplified") - ("Instantiated" "neither explicitly normalised nor simplified") - ("Normalised" "normalised") - ("HeadNormal" "head normalised") - (fromgoal ,want))) - -(defmacro agda2-maybe-normalised-asis (name comment cmd want) - `(agda2-proto-maybe-normalised - ,name ,comment ,cmd - ("AsIs" "returned as is") - ("Simplified" "simplified") - ("Normalised" "normalised") - ("HeadNormal" "head normalised") - (fromgoal ,want))) - -(defmacro agda2-maybe-normalised-toplevel (name comment cmd prompt) - `(agda2-proto-maybe-normalised - ,name ,comment ,cmd - ("Simplified" "simplified") - ("Instantiated" "neither explicitly normalised nor simplified") - ("Normalised" "normalised") - ("HeadNormal" "head normalised") - (global ,prompt))) - -(defmacro agda2-maybe-normalised-toplevel-asis-noprompt (name comment cmd) - `(agda2-proto-maybe-normalised - ,name ,comment ,cmd - ("AsIs" "returned as is") - ("Simplified" "simplified") - ("Normalised" "normalised") - ("HeadNormal" "head normalised") - (global nil))) - -(agda2-maybe-normalised - agda2-goal-type - "Show the type of the goal at point" - "Cmd_goal_type" - nil) - -(agda2-maybe-normalised - agda2-infer-type - "Infer the type of the goal at point" - "Cmd_infer" - "expression to type") - -(agda2-maybe-normalised-toplevel - agda2-infer-type-toplevel - "Infers the type of the given expression. The scope used for -the expression is that of the last point inside the current -top-level module" - "Cmd_infer_toplevel" - "Expression") - -(defun agda2-infer-type-maybe-toplevel () - "Infers the type of the given expression. -Either uses the scope of the current goal or, if point is not in a goal, the -top-level scope." - (interactive) - (call-interactively (if (agda2-goal-at (point)) - 'agda2-infer-type - 'agda2-infer-type-toplevel))) - -(defun agda2-why-in-scope () - "Explain why something is in scope in a goal." - (interactive) - (agda2-goal-cmd "Cmd_why_in_scope" nil "Name")) - -(defun agda2-why-in-scope-toplevel (name) - "Explain why something is in scope at the top level." - (interactive "MName: ") - (agda2-go nil t 'busy t - "Cmd_why_in_scope_toplevel" - (agda2-string-quote name))) - -(defun agda2-why-in-scope-maybe-toplevel () - "Explains why a given name is in scope." - (interactive) - (call-interactively (if (agda2-goal-at (point)) - 'agda2-why-in-scope - 'agda2-why-in-scope-toplevel))) - -(agda2-maybe-normalised - agda2-elaborate-give - "Elaborate check the given expression against the hole's type and fill in the - hole with the elaborated term" - "Cmd_elaborate_give" - "expression to elaborate and give") - -(agda2-maybe-normalised - agda2-goal-and-context - "Shows the type of the goal at point and the currect context" - "Cmd_goal_type_context" - nil) - -(agda2-maybe-normalised - agda2-goal-and-context-and-inferred - "Shows the context, the goal and the given expression's inferred type" - "Cmd_goal_type_context_infer" - "expression to type") - -(agda2-maybe-normalised - agda2-goal-and-context-and-checked - "Shows the context, the goal and check the given expression's against - the hole's type" - "Cmd_goal_type_context_check" - "expression to type") - -(agda2-maybe-normalised - agda2-show-context - "Show the context of the goal at point" - "Cmd_context" - nil) - -(agda2-maybe-normalised-asis - agda2-helper-function-type - "Compute the type of a hypothetical helper function." - "Cmd_helper_function" - "Expression") - -(agda2-maybe-normalised - agda2-module-contents - "Shows all the top-level names in the given module. -Along with their types." - "Cmd_show_module_contents" - "Module name (empty for current module)") - -(agda2-maybe-normalised-toplevel - agda2-module-contents-toplevel - "Shows all the top-level names in the given module. -Along with their types." - "Cmd_show_module_contents_toplevel" - "Module name (empty for top-level module)" -) - -(agda2-maybe-normalised-toplevel - agda2-search-about-toplevel - "Search About an identifier" - "Cmd_search_about_toplevel" - "Name" -) - -(defun agda2-module-contents-maybe-toplevel () - "Shows all the top-level names in the given module. -Along with their types. - -Uses either the scope of the current goal or, if point is not in -a goal, the top-level scope." - (interactive) - (call-interactively (if (agda2-goal-at (point)) - 'agda2-module-contents - 'agda2-module-contents-toplevel))) - -(defun agda2-solve-maybe-all () - "Solves goals that are already instantiated internally. -Either only one if point is a goal, or all of them." - (interactive) - (call-interactively (if (agda2-goal-at (point)) - 'agda2-solveOne - 'agda2-solveAll)) -) - -(defun agda2-auto-maybe-all () - "Run auto. -Either only one if point is a goal, or all of them." - (interactive) - (call-interactively (if (agda2-goal-at (point)) - 'agda2-autoOne - 'agda2-autoAll)) -) - -(agda2-maybe-normalised-toplevel-asis-noprompt - agda2-show-goals - "Show all goals." - "Cmd_metas" - ) - -(agda2-maybe-normalised-toplevel-asis-noprompt - agda2-solveAll - "Solves all goals that are already instantiated internally." - "Cmd_solveAll" - ) - -(agda2-maybe-normalised - agda2-solveOne - "Solves the goal at point if it is already instantiated internally" - "Cmd_solveOne" - nil -) - -(defun agda2-solveAll-action (iss) - (while iss - (let* ((g (pop iss)) (txt (pop iss)) - (cmd (cons 'agda2-solve-action (cons g (cons txt nil))))) - (if (null agda2-last-responses) - (push (cons 1 cmd) agda2-last-responses) - (nconc agda2-last-responses (cons (cons 3 cmd) nil)))))) - -(defun agda2-solve-action (g txt) - (save-excursion - (agda2-replace-goal g txt) - (agda2-goto-goal g) - (agda2-give))) - -(defun agda2-compute-normalised (&optional arg) - "Compute the normal form of the expression in the goal at point. - -With the prefix argument `(4)' \"abstract\" is ignored during the -computation. - -With a prefix argument `(16)' the normal form of -\"show \" is computed, and then the resulting string -is printed. - -With any other prefix the head normal form is computed." - (interactive "P") - (let ((cmd (concat "Cmd_compute" - (cond ((equal arg nil) " DefaultCompute") - ((equal arg '(4)) " IgnoreAbstract") - ((equal arg '(16)) " UseShowInstance") - (" HeadCompute"))))) - (agda2-goal-cmd cmd nil "expression to normalise"))) - -(defun agda2-compute-normalised-toplevel (expr &optional arg) - "Compute the normal form of the given expression. -The scope used for the expression is that of the last point -inside the current top-level module. - -With a prefix argument distinct from `(4)' the normal form of -\"show \" is computed, and then the resulting string -is printed. - -With the prefix argument `(4)' \"abstract\" is ignored during the -computation." - (interactive "MExpression: \nP") - (let ((cmd (concat "Cmd_compute_toplevel" - (cond ((equal arg nil) " DefaultCompute") - ((equal arg '(4)) " IgnoreAbstract") - ((equal arg '(16)) " UseShowInstance") - (" HeadCompute")) " "))) - (agda2-go nil t 'busy t - (concat cmd (agda2-string-quote expr))))) - -(defun agda2-compute-normalised-maybe-toplevel () - "Compute the normal form of the given expression. -The scope used for the expression is that of the last point -inside the current top-level module. - -With a prefix argument distinct from `(4)' the normal form of -\"show \" is computed, and then the resulting string -is printed. - -With the prefix argument `(4)' \"abstract\" is ignored during the -computation." - (interactive) - (if (agda2-goal-at (point)) - (call-interactively 'agda2-compute-normalised) - (call-interactively 'agda2-compute-normalised-toplevel))) - -(defun agda2-display-program-version () - "Display version of Agda" - (interactive) - (agda2-go nil nil 'busy t "Cmd_show_version")) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;; - -(defun agda2-highlight-reload nil - "Loads precomputed syntax highlighting info for the current buffer. -Only if the buffer is unmodified, and only if there is anything to load." - (unless (buffer-modified-p) - (agda2-go nil t 'not-so-busy t - "Cmd_load_highlighting_info" - (agda2-string-quote (buffer-file-name))))) - -(defun agda2-literate-p () - "Is the current buffer a literate Agda buffer?" - (not (equal (file-name-extension (buffer-file-name)) "agda"))) - -(defmacro agda2--case (exp &rest branches) ;FIXME: Use `pcase' instead! - (declare (debug t) (indent 1)) - (let ((s (make-symbol "v"))) - `(let ((,s ,exp)) - (cond - ,@(mapcar (lambda (branch) - `((equal ,s ,(car branch)) ,@(cdr branch))) - branches))))) - -(defun agda2-goals-action (goals) - "Annotates the goals in the current buffer with text properties. -GOALS is a list of the buffer's goal numbers, in the order in -which they appear in the buffer. Note that this function should -be run /after/ syntax highlighting information has been loaded, -because the two highlighting mechanisms interact in unfortunate -ways." - (agda2-forget-all-goals) - (agda2-let - ((literate (agda2-literate-p)) - stk - top - ;; Don't run modification hooks: we don't want this function to - ;; trigger agda2-abort-highlighting. - (inhibit-modification-hooks t)) - ((delims() (re-search-forward "[?]\\|[{][-!]\\|[-!][}]\\|--\\|^%.*\\\\begin{code}\\|\\\\begin{code}\\|\\\\end{code}\\|```\\|\\#\\+begin_src agda2\\|\\#\\+end_src agda2" nil t)) - ;; is-proper checks whether string s (e.g. "?" or "--") is proper - ;; i.e., is not part of an identifier. - ;; comment-starter is true if s starts a comment (e.g. "--") - (is-proper (s comment-starter) - (save-excursion - (save-match-data - (backward-char (length s)) - (unless (bolp) (backward-char 1)) ;; bolp = pointer at beginning of line - ;; Andreas, 2014-05-17 Issue 1132 - ;; A questionmark can also follow immediately after a . - ;; for instance to be a place holder for a dot pattern. - (looking-at (concat "\\([.{}();]\\|^\\|\\s \\)" ;; \\s = whitespace - (regexp-quote s) - (unless comment-starter - "\\([{}();]\\|$\\|\\s \\)")))))) - (make(p) (agda2-make-goal p (point) (pop goals))) - (inside-comment() (and stk (null (car stk)))) - (inside-goal() (and stk (integerp (car stk)))) - (outside-code() (and stk (eq (car stk) 'outside))) - (inside-code() (not (outside-code))) - ;; inside a multi-line comment ignore everything but the multi-line comment markers - (safe-delims() - (if (inside-comment) - (re-search-forward "{-\\|-}" nil t) - (delims)))) - (save-excursion - ;; In literate mode we should start out in the "outside of code" - ;; state. - (if literate (push 'outside stk)) - (goto-char (point-min)) - (while (and goals (safe-delims)) - (agda2--case (match-string 0) - ("\\begin{code}" (when (outside-code) (pop stk))) - ("\\end{code}" (when (not stk) (push 'outside stk))) - ("#+begin_src agda2" (when (outside-code) (pop stk))) - ("#+end_src agda2" (when (not stk) (push 'outside stk))) - ("```" (if (outside-code) (pop stk) - (when (not stk) (push 'outside stk)))) - ("--" (when (and (not stk) - (is-proper "--" t)) (end-of-line))) - ("{-" (when (and (inside-code) - (not (inside-goal))) (push nil stk))) - ("-}" (when (inside-comment) (pop stk))) - ("{!" (when (and (inside-code) - (not (inside-comment))) (push (- (point) 2) stk))) - ("!}" (when (inside-goal) - (setq top (pop stk)) - (unless stk (make top)))) - ("?" (progn - (when (and (not stk) (is-proper "?" nil)) - (delete-char -1) - (insert "{!!}") - (make (- (point) 4)))))))))) - -(defun agda2-make-goal (p q n) - "Make a goal with number N at

{!...!}. Assume the region is clean." - (annotation-preserve-mod-p-and-undo - (let ((atp (lambda (x ps) (add-text-properties x (1+ x) ps)))) - (funcall atp p '(category agda2-delim1)) - (funcall atp (1+ p) '(category agda2-delim2)) - (funcall atp (- q 2) '(category agda2-delim3)) - (funcall atp (1- q) '(category agda2-delim4))) - (let ((o (make-overlay p q nil t nil))) - (overlay-put o 'modification-hooks '(agda2-protect-goal-markers)) - (overlay-put o 'agda2-gn n) - (overlay-put o 'face 'highlight) - (overlay-put o 'after-string (propertize (format "%s" n) 'face 'highlight))))) - -(defun agda2-protect-goal-markers (ol action beg end &optional length) - "Ensures that the goal markers cannot be tampered with. -Except if `inhibit-read-only' is non-nil or /all/ of the goal is -modified." - (if action - ;; This is the after-change hook. - nil - ;; This is the before-change hook. - (cond - ((and (<= beg (overlay-start ol)) (>= end (overlay-end ol))) - ;; The user is trying to remove the whole goal: - ;; manually evaporate the overlay and add an undo-log entry so - ;; it gets re-added if needed. - (when (listp buffer-undo-list) - (push (list 'apply 0 (overlay-start ol) (overlay-end ol) - 'move-overlay ol (overlay-start ol) (overlay-end ol)) - buffer-undo-list)) - (delete-overlay ol)) - ((or (< beg (+ (overlay-start ol) 2)) - (> end (- (overlay-end ol) 2))) - (unless inhibit-read-only - (signal 'text-read-only nil)))))) - -(defun agda2-update (old-g new-txt) - "Update the goal OLD-G. -If NEW-TXT is a string, then the goal is replaced by the string, -and otherwise the text inside the goal is retained (parenthesised -if NEW-TXT is `'paren'). - -Removes the goal braces, but does not remove the goal overlay or -text properties." - (cl-multiple-value-bind (p q) (agda2-range-of-goal old-g) - (save-excursion - (cond ((stringp new-txt) - (agda2-replace-goal old-g new-txt)) - ((equal new-txt 'paren) - (goto-char (- q 2)) (insert ")") - (goto-char (+ p 2)) (insert "("))) - (cl-multiple-value-bind (p q) (agda2-range-of-goal old-g) - (delete-region (- q 2) q) - (delete-region p (+ p 2))) - ;; Update highlighting - (if (and (not (equal new-txt 'paren)) (not (equal new-txt 'no-paren))) - (apply 'agda2-go 'save t 'busy nil "Cmd_highlight" - (format "%d" old-g) - (agda2-mkRange `(,p ,(- q 2))) - (agda2-string-quote new-txt) nil)) - ))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;; Misc - -(defun agda2-process-status () - "Status of `agda2-process-buffer', or \"no process\"." - (condition-case nil - (process-status agda2-process) - (error "no process"))) - -(defun agda2-intersperse (sep xs) - (let(ys)(while xs (push (pop xs) ys)(push sep ys))(pop ys)(nreverse ys))) - -(defun agda2-goal-Range (o) - "The Haskell Range of goal overlay O." - (agda2-mkRange `(,(+ (overlay-start o) 2) - ,(- (overlay-end o) 2)))) - -(defun agda2-mkRange (points) - "A string representing a range corresponding to POINTS. -POINTS must be a list of integers, and its length must be 0 or 2." - (if points - (format "(intervalsToRange (Just (mkAbsolute %s)) %s)" - (agda2-string-quote (file-truename (buffer-file-name))) - (format "[Interval %s %s]" - (agda2-mkPos (car points)) - (agda2-mkPos (cadr points)))) - "noRange")) - -(defun agda2-mkPos (&optional p) - "The Haskell PositionWithoutFile corresponding to P or `point'." - (save-excursion - (save-restriction - (widen) - (if p (goto-char p)) - (format "(Pn () %d %d %d)" - (point) - (count-lines (point-min) (point)) - (1+ (current-column)))))) - -(defun agda2-char-quote (c) - "Convert character C to the notation used in Haskell strings. -The non-ASCII characters are actually rendered as -\"\\xNNNN\\&\", i.e. followed by a \"null character\", to avoid -problems if they are followed by digits. ASCII characters (code -points < 128) are converted to singleton strings." - (if (< c 128) - (list c) - ;; FIXME: Why return a list rather than a string? --Stef - (append (format "\\x%x\\&" (encode-char c 'ucs)) nil))) - -(defun agda2-string-quote (s) - "Format S as a Haskell string literal. -Removes any text properties, escapes newlines, double quotes, -etc., adds surrounding double quotes, and converts non-ASCII -characters to the \\xNNNN notation used in Haskell strings." - (let ((pp-escape-newlines t) - (s2 (copy-sequence s))) - (set-text-properties 0 (length s2) nil s2) - (mapconcat 'agda2-char-quote (pp-to-string s2) ""))) - -(defun agda2-list-quote (strings) - "Convert a list of STRINGS into a string representing it in Haskell syntax." - (concat "[" (mapconcat 'agda2-string-quote strings ", ") "]")) - -(defun agda2-goal-at(pos) - "Return (goal overlay, goal number) at POS, or nil." - (let ((os (and pos (overlays-at pos))) o g) - (while (and os (not(setq g (overlay-get (setq o (pop os)) 'agda2-gn))))) - (if g (list o g)))) - -(defun agda2-goal-overlay (g) - "Returns the overlay of goal number G, if any." - (car - (remove nil - (mapcar (lambda (o) (if (equal (overlay-get o 'agda2-gn) g) o)) - (overlays-in (point-min) (point-max)))))) - -(defun agda2-range-of-goal (g) - "The range of goal G." - (let ((o (agda2-goal-overlay g))) - (if o (list (overlay-start o) (overlay-end o))))) - -(defun agda2-goto-goal (g) - (let ((p (+ 2 (car (agda2-range-of-goal g))))) - (if p (goto-char p)))) - -(defun agda2-replace-goal (g newtxt) - "Replace the content of goal G with NEWTXT." (interactive) - (save-excursion - (cl-multiple-value-bind (p q) (agda2-range-of-goal g) - (setq p (+ p 2) q (- q 2)) - (let ((indent (and (goto-char p) (current-column)))) - (delete-region p q) (insert newtxt) - (while (re-search-backward "^" p t) - (insert-char ? indent) (backward-char (1+ indent))))))) - -(defun agda2-forget-all-goals () - "Remove all goal annotations. -\(Including some text properties which might be used by other -\(minor) modes.)" - (annotation-preserve-mod-p-and-undo - (remove-text-properties (point-min) (point-max) - '(category nil agda2-delim2 nil agda2-delim3 nil - display nil rear-nonsticky nil))) - (let ((p (point-min))) - (while (< (setq p (next-single-char-property-change p 'agda2-gn)) - (point-max)) - (delete-overlay (car (agda2-goal-at p)))))) - -(defun agda2-decl-beginning () - "Find the beginning point of the declaration containing the point. -To do: dealing with semicolon separated decls." - (interactive) - (save-excursion - (let* ((pEnd (point)) - (pDef (progn (goto-char (point-min)) - (re-search-forward "\\s *" pEnd t))) - (cDef (current-column))) - (while (re-search-forward - "where\\(\\s +\\)\\S \\|^\\(\\s *\\)\\S " pEnd t) - (if (match-end 1) - (setq pDef (goto-char (match-end 1)) - cDef (current-column)) - (goto-char (match-end 2)) - (if (>= cDef (current-column)) - (setq pDef (point) - cDef (current-column)))) - (forward-char)) - (goto-char pDef) - (if (equal (current-word) "mutual") - (or (match-end 2) (match-end 1)) - pDef)))) - -(defun agda2-beginning-of-decl () - (interactive) - (goto-char (agda2-decl-beginning))) - -(defvar agda2-debug-buffer-name "*Agda debug*" - "The name of the buffer used for Agda debug messages.") - -(defun agda2-verbose (msg) - "Appends the string MSG to the `agda2-debug-buffer-name' buffer. -Note that this buffer's contents is not erased automatically when -a file is loaded." - (with-current-buffer (get-buffer-create agda2-debug-buffer-name) - (save-excursion - (goto-char (point-max)) - (insert msg)))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Comments and paragraphs - -(defun agda2-comments-and-paragraphs-setup nil - "Set up comment and paragraph handling for the Agda mode." - - ;; Empty lines (all white space according to Emacs) delimit - ;; paragraphs. - (set (make-local-variable 'paragraph-start) "\\s-*$") - (set (make-local-variable 'paragraph-separate) paragraph-start) - - ;; Support for adding/removing comments. - (set (make-local-variable 'comment-start) "-- ") - - ;; Use the syntax table to locate comments (and possibly other - ;; 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. - (add-hook 'after-save-hook 'agda2-highlight-tokens nil 'local) - - ;; Support for proper filling of text in comments (requires that - ;; Filladapt is activated). - (when (featurep 'filladapt) - (add-to-list (make-local-variable - 'filladapt-token-table) - '("--" agda2-comment)) - (add-to-list (make-local-variable 'filladapt-token-match-table) - '(agda2-comment agda2-comment) t) - (add-to-list (make-local-variable 'filladapt-token-conversion-table) - '(agda2-comment . exact)))) - -(defun agda2-comment-dwim-rest-of-buffer () - "Comment or uncomment the rest of the buffer. -From the beginning of the current line to the end of the buffer." - (interactive) - (save-excursion - (forward-line 0) - (push-mark (point) 'no-message 'activate-mark) - (unwind-protect - (progn - (goto-char (point-max)) - (comment-dwim nil)) - (pop-mark)))) - -(defun agda2-highlight-tokens nil - "Compute token-based highlighting information. - -Unless `agda2-highlight-level' is `none' or the Agda process is -busy (or `not-so-busy') with something. This command might save -the buffer." - (unless (or agda2-in-progress - (equal agda2-highlight-level 'none)) - (agda2-go 'save t 'not-so-busy t - "Cmd_tokenHighlighting" - (agda2-string-quote (buffer-file-name)) - "Keep"))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Go to definition site - -(defun agda2-goto-definition-keyboard (&optional other-window) - "Go to the definition site of the name under point (if any). -If this function is invoked with a prefix argument then another window is used -to display the given position." - (interactive "P") - (annotation-goto-indirect (point) other-window)) - -(defun agda2-goto-definition-mouse (ev) - "Go to the definition site of the name clicked on, if any. -Otherwise, yank (see `mouse-yank-primary')." - (interactive "e") - (unless (annotation-goto-indirect ev) - ;; FIXME: Shouldn't we use something like - ;; (call-interactively (key-binding ev))? --Stef - (mouse-yank-primary ev))) - -(defun agda2-go-back nil - "Go back to the previous position in which -`agda2-goto-definition-keyboard' or `agda2-goto-definition-mouse' was -invoked." - (interactive) - (annotation-go-back)) - -(defun agda2-maybe-goto (filepos) - "Might move point to the given error. -FILEPOS should have the form (FILE . POSITION). - -If `agda2-highlight-in-progress' is nil, then nothing happens. -Otherwise, if the current buffer is the one that is connected to -the Agda process, then point is moved to POSITION in -FILE (assuming that the FILE is readable). Otherwise point is -moved to the given position in the buffer visiting the file, if -any, and in every window displaying the buffer, but the window -configuration and the selected window are not changed." - (when (and agda2-highlight-in-progress - (consp filepos) - (stringp (car filepos)) - (integerp (cdr filepos))) - (if agda2-in-agda2-file-buffer - (annotation-goto-and-push (current-buffer) (point) filepos) - (save-excursion - (let ((buffer (find-buffer-visiting (car filepos)))) - (when buffer - (let ((windows (get-buffer-window-list buffer - 'no-minibuffer t))) - (if windows - (dolist (window windows) - (with-selected-window window - (goto-char (cdr filepos)))) - (with-current-buffer buffer - (goto-char (cdr filepos))))))))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Implicit arguments - -(defun agda2-display-implicit-arguments (&optional arg) - "Toggle display of implicit arguments. -With prefix argument, turn on display of implicit arguments if -the argument is a positive number, otherwise turn it off." - (interactive "P") - (cond - ((eq arg nil) - (agda2-go nil t 'not-so-busy t "ToggleImplicitArgs")) - ((and (numberp arg) (> arg 0)) - (agda2-go nil t 'not-so-busy t "ShowImplicitArgs" "True")) - (t (agda2-go nil t 'not-so-busy t "ShowImplicitArgs" "False")))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Irrelevant arguments - -(defun agda2-display-irrelevant-arguments (&optional arg) - "Toggle display of irrelevant arguments. -With prefix argument, turn on display of irrelevant arguments if -the argument is a positive number, otherwise turn it off." - (interactive "P") - (cond - ((eq arg nil) - (agda2-go nil t 'not-so-busy t "ToggleIrrelevantArgs")) - ((and (numberp arg) (> arg 0)) - (agda2-go nil t 'not-so-busy t "ShowIrrelevantArgs" "True")) - (t (agda2-go nil t 'not-so-busy t "ShowIrrelevantArgs" "False")))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;; - -(defun agda2-popup-menu-3 (ev) - "If in a goal, popup the goal menu and call chosen command." - (interactive "e") - (let (choice) - (save-excursion - (and (agda2-goal-at (goto-char (posn-point (event-end ev)))) - (setq choice (x-popup-menu ev agda2-goal-map)) - (call-interactively - (lookup-key agda2-goal-map (apply 'vector choice))))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Switching to a different version of Agda - -(defun agda2-get-agda-program-versions () - "Get \"version strings\" of executables starting with -\\='agda2hs-mode\\=' in current path." - (delete-dups - (mapcar (lambda (path) - ;; strip 'agda2hs-mode' prefix - (replace-regexp-in-string "^agda2hs-mode-?" "" - (file-name-nondirectory path))) - (cl-remove-if-not 'file-executable-p - ;; concatenate result - (cl-reduce 'append - ;; for each directory in exec-path, get list of - ;; files whose name starts with 'agda-mode' - (mapcar (lambda (path) - (when (file-accessible-directory-p path) - (directory-files path 't "^agda2hs-mode"))) - exec-path)))))) - -;; Note that other versions of Agda may use different protocols, so -;; this function unloads the Emacs mode. - -(defun agda2-set-program-version (version) - "Tries to switch to Agda version VERSION. - -This command assumes that the agda and agda-mode executables for -Agda version VERSION are called agda-VERSION and -agda-mode-VERSION, and that they are located on the PATH. (If -VERSION is empty, then agda and agda-mode are used instead.) - -An attempt is made to preserve the default value of -`agda2-mode-hook'." - (interactive - (list (completing-read "Version: " (agda2-get-agda-program-versions)))) - - (let* - ((agda-buffers - (cl-mapcan (lambda (buf) - (with-current-buffer buf - (when (equal major-mode 'agda2-mode) - (list buf)))) - (buffer-list))) - - (default-hook (default-value 'agda2-mode-hook)) - - (version-suffix (if (or (equal version "") - (equal version nil)) - "" - (concat "-" version))) - - ;; Run agda-mode and make sure that it returns - ;; successfully. - (coding-system-for-read 'utf-8) - (agda-mode-prog (concat "agda2hs-mode" version-suffix)) - (agda-mode-path - (condition-case nil - (with-temp-buffer - (unless - (equal 0 (call-process agda-mode-prog - nil (current-buffer) nil - "locate")) - (error "%s" (concat "Error when running " - agda-mode-prog))) - (buffer-string)) - (file-error - (error "%s" (concat "Could not find " agda-mode-prog)))))) - - ;; Make sure that agda-mode returns a valid file. - (unless (file-readable-p agda-mode-path) - (error "%s" (concat "Could not read " agda-mode-path))) - - ;; Turn off the Agda mode. - (agda2-quit) - - ;; Kill some buffers related to Agda. - (when (buffer-live-p agda2-info-buffer) - (kill-buffer agda2-info-buffer)) - (when (and agda2-debug-buffer-name - (get-buffer agda2-debug-buffer-name)) - (kill-buffer agda2-debug-buffer-name)) - - ;; Remove the Agda mode directory from the load path. - (setq load-path (delete agda2-directory load-path)) - - ;; Unload the Agda mode and its dependencies. - (unload-feature 'agda2-mode 'force) - (unload-feature 'agda2 'force) - (unload-feature 'eri 'force) - (unload-feature 'annotation 'force) - (unload-feature 'agda-input 'force) - (unload-feature 'agda2-highlight 'force) - (unload-feature 'agda2-abbrevs 'force) - (unload-feature 'agda2-queue 'force) - - ;; Load the new version of Agda. - (load-file agda-mode-path) - (require 'agda2-mode) - (setq agda2-program-name (concat "agda2hs" version-suffix)) - - ;; Restore the Agda mode's default hook (if any). - (when default-hook - (set-default 'agda2-mode-hook default-hook)) - - ;; Restart the Agda mode in all former Agda mode buffers. - (mapc (lambda (buf) - (with-current-buffer buf - (agda2-mode))) - agda-buffers))) - -(provide 'agda2-mode) -;;; agda2-mode.el ends here diff --git a/src/data/emacs-mode/agda2-queue.el b/src/data/emacs-mode/agda2-queue.el deleted file mode 100644 index 7988661b..00000000 --- a/src/data/emacs-mode/agda2-queue.el +++ /dev/null @@ -1,44 +0,0 @@ -;;; agda2-queue.el --- Simple FIFO character queues. -;; SPDX-License-Identifier: MIT License - -(defun agda2-queue-empty () - "Creates a new empty FIFO character queue. -Queues are represented as pairs. The car contains the queue. If -the queue is empty, then the cdr contains the symbol nil, and -otherwise it points to the queue's last cons-cell." - (cons nil nil)) - -(defun agda2-queue-is-prefix-of (prefix queue) - "Returns a non-nil result iff the string PREFIX is a prefix of QUEUE. -Linear in the length of PREFIX." - (let ((queue (car queue)) - (prefix (append prefix nil))) - (while (and (consp queue) (consp prefix) - (equal (car queue) (car prefix))) - (pop queue) - (pop prefix)) - (null prefix))) - -(defun agda2-queue-enqueue (queue string) - "Adds the characters in STRING to the end of QUEUE. -This function updates QUEUE destructively, and is linear in the -length of STRING." - (let ((chars (append string nil))) - (when (consp chars) - (if (null (cdr queue)) - (setcar queue chars) - (setcdr (cdr queue) chars)) - (setcdr queue (last chars)))) - queue) - -(defun agda2-queue-from-string (string) - "Creates a new FIFO containing the characters in STRING. -Linear in the length of STRING." - (agda2-queue-enqueue (agda2-queue-empty) string)) - -(defun agda2-queue-to-string (queue) - "Constructs a string containing all the characters in QUEUE. -Linear in the length of QUEUE." - (concat "" (car queue))) - -(provide 'agda2-queue) diff --git a/src/data/emacs-mode/agda2.el b/src/data/emacs-mode/agda2.el deleted file mode 100644 index 25e046e8..00000000 --- a/src/data/emacs-mode/agda2.el +++ /dev/null @@ -1,16 +0,0 @@ -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Agda mode code which should run before the first Agda file is -;; loaded -;; SPDX-License-Identifier: MIT License - -(defvar agda2-directory (file-name-directory load-file-name) - "Path to the directory that contains agda2.el(c).") - -(add-to-list 'load-path (or agda2-directory (car load-path))) - -(autoload 'agda2-mode "agda2-mode" - "Major mode for editing Agda files (version ≥ 2)." t) -(add-to-list 'auto-mode-alist '("\\.l?agda\\'" . agda2-mode)) -(modify-coding-system-alist 'file "\\.l?agda\\'" 'utf-8) - -(provide 'agda2) diff --git a/src/data/emacs-mode/annotation.el b/src/data/emacs-mode/annotation.el deleted file mode 100644 index 22b22217..00000000 --- a/src/data/emacs-mode/annotation.el +++ /dev/null @@ -1,301 +0,0 @@ -;;; annotation.el --- Functions for annotating text with faces and help bubbles - -;; Version: 1.0 - -;; SPDX-License-Identifier: MIT License -;; URL: https://github.com/agda/agda -;; Version: 1.0 - -;;; Commentary: - -;; Note that this library enumerates buffer positions starting from 1, -;; just like Emacs. - -(require 'cl-lib) - -(defvar annotation-bindings nil - "An association list mapping symbols to faces.") -(make-variable-buffer-local 'annotation-bindings) - -(defvar annotation-goto-stack nil - "Positions from which `annotation-goto' was invoked.") - -(defun annotation-goto-indirect (link &optional other-window) - "Follow the `annotation-goto' hyperlink pointed to by LINK, if any. - -LINK should be a buffer position, or an event object (in which -case the ending position is used). - -If the hyperlink exists and the jump is performed successfully, -then `t' is returned, and otherwise `nil' (unless an error is -raised). - -If OTHER-WINDOW is non-nil, then another window is used to -display the target position." - (let (source-pos - source-window - source-buffer - source-file-name - target) - (cond ((eventp link) - (let ((pn (event-end link))) - (when (not (posn-area pn)) - (setq source-pos (posn-point pn)) - (setq source-window (posn-window pn)) - (setq source-buffer (window-buffer source-window))))) - ((integerp link) - (setq source-pos link) - (setq source-window (selected-window)) - (setq source-buffer (current-buffer))) - (t (error "Not an integer or event object: %S" link))) - (when (and source-pos source-buffer) - (with-current-buffer source-buffer - (setq target (get-text-property source-pos 'annotation-goto))) - (when target - (unless (equal source-window (selected-window)) - (select-window source-window)) - (annotation-goto-and-push source-buffer source-pos target - other-window))))) - -(defun annotation-go-back nil - "Go back to the previous position. -The previous position in which `annotation-goto-and-push' was -successfully invoked." - (when annotation-goto-stack - (let ((pos (pop annotation-goto-stack))) - (annotation-goto pos)))) - -(defun annotation-goto-and-push (source-buffer source-pos filepos &optional other-window) - "Like `annotation-goto', but pushes a position when successful. -The position consists of the file visited by SOURCE-BUFFER, and -the position given by SOURCE-POS." - (let (source-file-name) - (with-current-buffer source-buffer - (setq source-file-name buffer-file-name)) - (when (annotation-goto filepos other-window) - (unless (and (equal source-buffer (current-buffer)) - (eq source-pos (point))) - (push `(,source-file-name . ,source-pos) - annotation-goto-stack)) - t))) - -(defun annotation-goto (filepos &optional other-window) - "Go to file position FILEPOS if the file is readable. -FILEPOS should have the form (FILE . POS). Return t if successful. - -If OTHER-WINDOW is non-nil, use another window to display the -given position." - (when (consp filepos) - (let ((file (car filepos))) - (if (file-readable-p file) - (progn - (if other-window - (find-file-other-window file) - (find-file file)) - (goto-char (cdr filepos)) - t) - (error "File does not exist or is unreadable: %s." file))))) - -(defun annotation-merge-faces (start end faces) - "Helper procedure used by `annotation-annotate'. -For each position in the range the FACES are merged -with the current value of the annotation-faces text property, and -both the face and the annotation-faces text properties are set to -the resulting list of faces. - -Precondition: START and END must be numbers, and START must be -less than END." - (cl-assert (condition-case nil (< start end) (error nil))) - (let ((pos start) - mid) - (while (< pos end) - (setq mid (next-single-property-change pos 'annotation-faces - nil end)) - (let* ((old-faces (get-text-property pos 'annotation-faces)) - (all-faces (cl-union old-faces faces))) - (mapc (lambda (prop) (put-text-property pos mid prop all-faces)) - '(annotation-faces face)) - (setq pos mid))))) - -(defun annotation-annotate - (start end anns &optional token-based info goto) - "Annotate text between START and END in the current buffer. - -Nothing happens if either START or END are out of bounds for the -current (possibly narrowed) buffer, or END <= START. - -If ANNS is nil, then those text properties between START and END -that have been set by this function are deleted. Otherwise the -following happens. - -All the symbols in ANNS are looked up in `annotation-bindings', -and the resulting list of faces is used to set the face text -property. For each position in the range the faces are merged -with the current value of the annotation-faces text property, and -both the face and the annotation-faces text properties are set to -the resulting list of faces. - -If TOKEN-BASED is non-nil, then the annotation-token-based -property is set to t. This means that all text properties set by -`annotation-annotate' in this range are interpreted as being -token-based, including those set by previous calls to this -procedure. - -If the string INFO is non-nil, the mouse-face -property is set to highlight, and INFO is used as the help-echo -string. If GOTO has the form (FILENAME . POSITION), then the -mouse-face property is set to highlight, and the given -filename/position will be used by `annotation-goto-indirect' when -it is invoked with a position in the given range. - -Note that if a given attribute is defined by several faces, then -the first face's setting takes precedence. - -All characters whose text properties get set also have the -annotation-annotated property set to t, and -annotation-annotations is set to a list with all the properties -that have been set; this ensures that the text properties can -later be removed (if the annotation-* properties are not tampered -with)." - (when (and (<= (point-min) start) - (< start end) - (<= end (point-max))) - (if (null anns) - (annotation-remove-annotations nil start end) - (let ((faces (delq nil - (mapcar (lambda (ann) - (cdr (assoc ann annotation-bindings))) - anns))) - (props nil)) - (when faces - (annotation-merge-faces start end faces) - (add-to-list 'props 'face) - (add-to-list 'props 'annotation-faces)) - (when token-based - (add-text-properties start end - `(annotation-token-based t)) - (add-to-list 'props 'annotation-token-based)) - (when (consp goto) - (add-text-properties start end - `(annotation-goto ,goto - mouse-face highlight)) - (add-to-list 'props 'annotation-goto) - (add-to-list 'props 'mouse-face)) - (when info - (add-text-properties start end - `(mouse-face highlight help-echo ,info)) - (add-to-list 'props 'mouse-face) - (add-to-list 'props 'help-echo)) - (when props - (add-to-list 'props 'annotation-annotated) - (let ((pos start) - mid) - (while (< pos end) - (setq mid (next-single-property-change pos - 'annotation-annotations nil end)) - (let* ((old-props (get-text-property pos 'annotation-annotations)) - (all-props (cl-union old-props props))) - (add-text-properties pos mid - `(annotation-annotated t annotation-annotations ,all-props)) - (setq pos mid))))))))) - -(defmacro annotation-preserve-mod-p-and-undo (&rest code) - "Run CODE preserving both the undo data and the modification bit. -Modification hooks are also disabled." - (declare (debug (&rest form))) - (let ((modp (make-symbol "modp"))) - `(let ((,modp (buffer-modified-p)) - ;; Don't check if the file is being modified by some other process. - (buffer-file-name nil) - ;; Don't record those changes on the undo-log. - (buffer-undo-list t) - ;; Don't run modification hooks. - (inhibit-modification-hooks t)) - (unwind-protect - (progn ,@code) - (restore-buffer-modified-p ,modp))))) - -(defun annotation-remove-annotations (&optional token-based start end) - "Remove text properties set by `annotation-annotate'. - -In the current buffer. If START and END are given, then -properties are only removed between these positions. If -TOKEN-BASED is non-nil, then only token-based properties are -removed. - -This function preserves the file modification stamp of the -current buffer, does not modify the undo list, and temporarily -disables all modification hooks. - -Note: This function may fail if there is read-only text in the -buffer." - - ;; remove-text-properties fails for read-only text. - - (annotation-preserve-mod-p-and-undo - (let ((tag (if token-based - 'annotation-token-based - 'annotation-annotated)) - (pos (or start (point-min))) - (end (or end (point-max))) - pos2) - (while pos - (let ((props (get-text-property pos 'annotation-annotations))) - (setq pos2 (next-single-property-change pos tag nil end)) - (when (and props - (or (not token-based) - (member 'annotation-token-based props))) - (remove-text-properties pos (or pos2 (point-max)) - (cl-mapcan (lambda (prop) (list prop nil)) - (cons 'annotation-annotations props))))) - (setq pos (unless (or (not pos2) (>= pos2 end)) pos2)))))) - -(defun annotation-load (goto-help remove &rest cmds) - "Apply highlighting annotations in CMDS in the current buffer. - -The argument CMDS should be a list of lists (start end anns -&optional info goto). Text between start and end will be -annotated with the annotations in the list anns (using -`annotation-annotate'). If info and/or goto are present they will -be used as the corresponding arguments to `annotation-annotate'. - -If INFO is nil in a call to `annotation-annotate', and the GOTO -argument is a cons-cell, then the INFO argument is set to -GOTO-HELP. The intention is that the default help text should -inform the user about the \"goto\" facility. - -If REMOVE is nil, then old syntax highlighting information is not -removed. Otherwise all token-based syntax highlighting is -removed. In order to reduce the risk of flicker this highlighting -is removed step by step, in conjunction with the addition of new -highlighting. (This process assumes that CMDS is ordered by the -positions of the annotations. If it isn't, then the highlighting -is still applied correctly, but perhaps with more flicker.) - -This function preserves the file modification stamp of the -current buffer, does not modify the undo list, and temporarily -disables all modification hooks. - -Note: This function may fail if there is read-only text in the -buffer." - (annotation-preserve-mod-p-and-undo - (when (listp cmds) - (let ((pos (point-min))) - (dolist (cmd cmds) - (cl-destructuring-bind - (start end anns &optional token-based info goto) cmd - (let ((info (if (and (not info) (consp goto)) - goto-help - info))) - (when remove - (annotation-remove-annotations - 'token-based pos end) - (setq pos end)) - (annotation-annotate - start end anns token-based info goto)))) - (when remove - (annotation-remove-annotations - 'token-based pos (point-max))))))) - -(provide 'annotation) -;;; annotation.el ends here diff --git a/src/data/emacs-mode/eri.el b/src/data/emacs-mode/eri.el deleted file mode 100644 index 2cd5d7e7..00000000 --- a/src/data/emacs-mode/eri.el +++ /dev/null @@ -1,212 +0,0 @@ -;;; eri.el --- Enhanced relative indentation (eri) - -;; SPDX-License-Identifier: MIT License -;; URL: https://github.com/agda/agda -;; Version: 1.0 - -;;; Commentary: - -;; Cycle between indentation points with enhanced relative indentation. - -;;; Code: - -(require 'cl-lib) - -(defun eri-current-line-length nil - "Calculate length of current line." - (- (line-end-position) (line-beginning-position))) - -(defun eri-current-line-empty nil - "Return non-nil if the current line is empty (not counting white space)." - (equal (current-indentation) - (eri-current-line-length))) - -(defun eri-maximum (xs) - "Calculate maximum element in XS. -Returns nil if the list is empty." - (if xs (apply 'max xs))) - -(defun eri-take (n xs) - "Return the first N elements of XS." - (butlast xs (- (length xs) n))) - -(defun eri-split (x xs) - "Return a pair of lists (XS1 . XS2). -If XS is sorted, then XS = (append XS1 XS2), and all elements in -XS1 are <= X, whereas all elements in XS2 are > X." - (let* ((pos (or (cl-position-if (lambda (y) (> y x)) xs) (length xs))) - (xs1 (eri-take pos xs)) - (xs2 (nthcdr pos xs))) - (cons xs1 xs2))) - -(defun eri-calculate-indentation-points-on-line (max) - "Calculate indentation points on current line. -Only points left of column number MAX are included. If MAX is -nil, then all points are included. Points are returned in -ascending order. - -Example (positions marked with ^ are returned): - - f x y = g 3 (Just y) 5 4 - ^ ^ ^ ^ ^ ^ ^ ^ | - | - MAX" - (let ((result)) - (save-excursion - (save-restriction - (beginning-of-line) - ; To make \\` work in the regexp below: - (narrow-to-region (line-beginning-position) (line-end-position)) - (while - (progn - (let ((pos (and (search-forward-regexp - "\\(?:\\s-\\|\\`\\)\\(\\S-\\)" nil t) - (match-beginning 1)))) - (when (not (null pos)) - (let ((pos1 (- pos (line-beginning-position)))) - (when (or (null max) (< pos1 max)) - (add-to-list 'result pos1)))) - (and pos - (< (point) (line-end-position)) - (or (null max) (< (current-column) max)))))) - (nreverse result) ; Destructive operation. - )))) - -(defun eri-new-indentation-points () - "Calculate new indentation points. -Returns a singleton list containing the column number two steps -in from the indentation of the first non-empty line (white space -excluded) above the current line. If there is no such line, -then the empty list is returned." - (let ((start (line-beginning-position))) - (save-excursion - ; Find a non-empty line above the current one, if any. - (while - (progn - (forward-line -1) - (not (or (bobp) - (not (eri-current-line-empty)))))) - (if (or (equal (point) start) - (eri-current-line-empty)) - nil - (list (+ 2 (current-indentation))))))) - -(defun eri-calculate-indentation-points (reverse) - "Calculate points used to indent the current line. -The points are given in reverse order if REVERSE is non-nil. See -`eri-indent' for a description of how the indentation points are -calculated; note that the current indentation is not included in -the returned list." - ;; First find a bunch of indentations used above the current line. - (let ((points) - (max) - (start (line-beginning-position))) - (save-excursion - (while - (progn - (forward-line -1) - ; Skip the line we started from and lines with nothing but - ; white space. - (unless (or (equal (point) start) - (eri-current-line-empty)) - (setq points - (append - (eri-calculate-indentation-points-on-line max) - points)) - (setq max (car points))) - ;; Stop after hitting the beginning of the buffer or a - ;; non-empty, non-indented line. - (not (or (bobp) - (and (equal (current-indentation) 0) - (> (eri-current-line-length) 0))))))) - ;; Add new indentation points, but remove the current indentation. - ;; Sort the indentations. Rearrange the points so that the next - ;; point is the one after the current one. Reverse if necessary. - ;; - ;; Note: sort and nreverse are destructive. - (let* ((ps0 (remove (current-indentation) - (append (eri-new-indentation-points) points))) - (ps1 (eri-split (current-indentation) (sort ps0 '<))) - (ps2 (append (cdr ps1) (car ps1)))) - (if reverse - (nreverse ps2) - ps2)))) - -(defun eri-indent (&optional reverse) - "Cycle between some possible indentation points. -With prefix argument REVERSE, cycle in reverse order. - -Assume that a file contains the following lines of code, with -point on the line with three dots: - -frob = loooooooooooooooooooooooooong identifier -foo = f a b - where - f (Foo x) y = let bar = x - baz = 3 + 5 - -... - -^ ^ ^ ^ ^ ^ ^ ^ ^ * ^ ^ ^ ^ - -Then the ^'s and the * mark the indentation points that this -function cycles through. The indentation points are selected as -follows: - - * All lines before the current one, up to and including the - first non-indented line (or the beginning of the buffer) are - considered. - - foo = f a b - where - f (Foo x) y = let bar = x - baz = 3 + 5 - - * On these lines, erase all characters that stand to the right - of some non-white space character on a lower line. - - foo - whe - f (Foo x) y = let b - baz = 3 + 5 - - * Also erase all characters not immediately preceded by white - space. - - f - w - f ( x y = l b - b = 3 + 5 - - * The columns of all remaining characters are indentation - points. - - f w f ( x y = l b = 3 + 5 - ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ - - * A new indentation point is also added, two steps in from the - indentation of the first non-empty line (white space - excluded) above the current line (if there is such a line). - - f w f ( x y = l b = 3 + 5 - ^ ^ ^ ^ ^ ^ ^ ^ ^ * ^ ^ ^ ^" - (interactive "P") - (let* ((points (eri-calculate-indentation-points reverse)) - (remaining-points (cdr (member (current-indentation) points))) - (indentation (if remaining-points - (car remaining-points) - (car points)))) - (when indentation - (save-excursion (indent-line-to indentation)) - (if (< (current-column) indentation) - (indent-line-to indentation))))) - -(defun eri-indent-reverse nil - "Cycle between some possible indentation points (in reverse order). -See `eri-indent' for a description of how the indentation points -are calculated." - (interactive) - (eri-indent t)) - -(provide 'eri) -;;; eri.el ends here