1
;;; agda-input.el --- The Agda input method
5
;; A highly customisable input method which can inherit from other
6
;; Quail input methods. By default the input method is geared towards
7
;; the input of mathematical and other symbols in Agda programs.
9
;; Use M-x customize-group agda-input to customise this input method.
10
;; Note that the functions defined under "Functions used to tweak
11
;; translation pairs" below can be used to tweak both the key
12
;; translations inherited from other input methods as well as the
13
;; ones added specifically for this one.
15
;; Use agda-input-show-translations to see all the characters which
16
;; can be typed using this input method (except for those
17
;; corresponding to ASCII characters).
24
;; Quail is quite stateful, so be careful when editing this code. Note
25
;; that with-temp-buffer is used below whenever buffer-local state is
28
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
31
(defun agda-input-concat-map (f xs)
33
(apply 'append (mapcar f xs)))
35
(defun agda-input-to-string-list (s)
36
"Convert a string S to a list of one-character strings, after
37
removing all space and newline characters."
38
(agda-input-concat-map
39
(lambda (c) (if (member c (string-to-list " \n"))
44
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
45
;; Functions used to tweak translation pairs
47
;; lexical-let is used since Elisp lacks lexical scoping.
49
(defun agda-input-compose (f g)
50
"\x -> concatMap F (G x)"
51
(lexical-let ((f1 f) (g1 g))
52
(lambda (x) (agda-input-concat-map f1 (funcall g1 x)))))
54
(defun agda-input-or (f g)
56
(lexical-let ((f1 f) (g1 g))
57
(lambda (x) (append (funcall f1 x) (funcall g1 x)))))
59
(defun agda-input-nonempty ()
60
"Only keep pairs with a non-empty first component."
61
(lambda (x) (if (> (length (car x)) 0) (list x))))
63
(defun agda-input-prepend (prefix)
64
"Prepend PREFIX to all key sequences."
65
(lexical-let ((prefix1 prefix))
66
(lambda (x) `((,(concat prefix1 (car x)) . ,(cdr x))))))
68
(defun agda-input-prefix (prefix)
69
"Only keep pairs whose key sequence starts with PREFIX."
70
(lexical-let ((prefix1 prefix))
72
(if (equal (substring (car x) 0 (length prefix1)) prefix1)
75
(defun agda-input-suffix (suffix)
76
"Only keep pairs whose key sequence ends with SUFFIX."
77
(lexical-let ((suffix1 suffix))
79
(if (equal (substring (car x)
80
(- (length (car x)) (length suffix1)))
84
(defun agda-input-drop (ss)
85
"Drop pairs matching one of the given key sequences.
86
SS should be a list of strings."
87
(lexical-let ((ss1 ss))
88
(lambda (x) (unless (member (car x) ss1) (list x)))))
90
(defun agda-input-drop-beginning (n)
91
"Drop N characters from the beginning of each key sequence."
93
(lambda (x) `((,(substring (car x) n1) . ,(cdr x))))))
95
(defun agda-input-drop-end (n)
96
"Drop N characters from the end of each key sequence."
99
`((,(substring (car x) 0 (- (length (car x)) n1)) .
102
(defun agda-input-drop-prefix (prefix)
103
"Only keep pairs whose key sequence starts with PREFIX.
104
This prefix is dropped."
106
(agda-input-drop-beginning (length prefix))
107
(agda-input-prefix prefix)))
109
(defun agda-input-drop-suffix (suffix)
110
"Only keep pairs whose key sequence ends with SUFFIX.
111
This suffix is dropped."
112
(lexical-let ((suffix1 suffix))
114
(agda-input-drop-end (length suffix1))
115
(agda-input-suffix suffix1))))
117
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
120
;; The :set keyword is set to 'agda-input-incorporate-changed-setting
121
;; so that the input method gets updated immediately when users
122
;; customize it. However, the setup functions cannot be run before all
123
;; variables have been defined. Hence the :initialize keyword is set to
124
;; 'custom-initialize-default to ensure that the setup is not performed
125
;; until agda-input-setup is called at the end of this file.
127
(defgroup agda-input nil
128
"The Agda input method.
129
After tweaking these settings you may want to inspect the resulting
130
translations using `agda-input-show-translations'."
134
(defcustom agda-input-tweak-all
136
(agda-input-prepend "\\")
137
(agda-input-nonempty))
138
"An expression yielding a function which can be used to tweak
139
all translations before they are included in the input method.
140
The resulting function (if non-nil) is applied to every
141
\(KEY-SEQUENCE . TRANSLATION) pair and should return a list of such
142
pairs. (Note that the translations can be anything accepted by
145
If you change this setting manually (without using the
146
customization buffer) you need to call `agda-input-setup' in
147
order for the change to take effect."
149
:set 'agda-input-incorporate-changed-setting
150
:initialize 'custom-initialize-default
153
(defcustom agda-input-inherit
154
`(("TeX" . (agda-input-compose
155
(agda-input-drop '("geq" "leq" "bullet" "qed"))
157
(agda-input-drop-prefix "\\")
160
(agda-input-drop '("^o"))
161
(agda-input-prefix "^"))
162
(agda-input-prefix "_")))))
164
"A list of Quail input methods whose translations should be
165
inherited by the Agda input method (with the exception of
166
translations corresponding to ASCII characters).
168
The list consists of pairs (qp . tweak), where qp is the name of
169
a Quail package, and tweak is an expression of the same kind as
170
`agda-input-tweak-all' which is used to tweak the translation
171
pairs of the input method.
173
The inherited translation pairs are added last, after
174
`agda-input-user-translations' and `agda-input-translations'.
176
If you change this setting manually (without using the
177
customization buffer) you need to call `agda-input-setup' in
178
order for the change to take effect."
180
:set 'agda-input-incorporate-changed-setting
181
:initialize 'custom-initialize-default
182
:type '(repeat (cons (string :tag "Quail package")
183
(sexp :tag "Tweaking function"))))
185
(defcustom agda-input-translations
186
(let ((max-lisp-eval-depth 2800)) `(
188
;; Equality and similar symbols.
190
("eq" . ,(agda-input-to-string-list "=∼∽≈≋∻∾∿≀≃⋍≂≅ ≌≊≡≣≐≑≒≓≔≕≖≗≘≙≚≛≜≝≞≟≍≎≏≬⋕"))
191
("eqn" . ,(agda-input-to-string-list "≠≁ ≉ ≄ ≇≆ ≢ ≭ "))
194
("~" . ("∼")) ("~n" . ("≁"))
195
("~~" . ("≈")) ("~~n" . ("≉"))
198
("~-" . ("≃")) ("~-n" . ("≄"))
200
("~=" . ("≅")) ("~=n" . ("≇"))
202
("==" . ("≡")) ("==n" . ("≢"))
204
(".=" . ("≐")) (".=." . ("≑"))
205
(":=" . ("≔")) ("=:" . ("≕"))
208
("and=" . ("≙")) ("or=" . ("≚"))
215
;; Inequality and similar symbols.
217
("leq" . ,(agda-input-to-string-list "<≪⋘≤≦≲ ≶≺≼≾⊂⊆ ⋐⊏⊑ ⊰⊲⊴⋖⋚⋜⋞"))
218
("leqn" . ,(agda-input-to-string-list "≮ ≰≨≴⋦≸⊀ ⋨⊄⊈⊊ ⋢⋤ ⋪⋬ ⋠"))
219
("geq" . ,(agda-input-to-string-list ">≫⋙≥≧≳ ≷≻≽≿⊃⊇ ⋑⊐⊒ ⊱⊳⊵⋗⋛⋝⋟"))
220
("geqn" . ,(agda-input-to-string-list "≯ ≱≩≵⋧≹⊁ ⋩⊅⊉⊋ ⋣⋥ ⋫⋭ ⋡"))
222
("<=" . ("≤")) (">=" . ("≥"))
223
("<=n" . ("≰")) (">=n" . ("≱"))
224
("len" . ("≰")) ("gen" . ("≱"))
225
("<n" . ("≮")) (">n" . ("≯"))
226
("<~" . ("≲")) (">~" . ("≳"))
227
("<~n" . ("⋦")) (">~n" . ("⋧"))
228
("<~nn" . ("≴")) (">~nn" . ("≵"))
230
("sub" . ("⊂")) ("sup" . ("⊃"))
231
("subn" . ("⊄")) ("supn" . ("⊅"))
232
("sub=" . ("⊆")) ("sup=" . ("⊇"))
233
("sub=n" . ("⊈")) ("sup=n" . ("⊉"))
235
("squb" . ("⊏")) ("squp" . ("⊐"))
236
("squb=" . ("⊑")) ("squp=" . ("⊒"))
237
("squb=n" . ("⋢")) ("squp=n" . ("⋣"))
239
;; Set membership etc.
241
("member" . ,(agda-input-to-string-list "∈∉∊∋∌∍⋲⋳⋴⋵⋶⋷⋸⋹⋺⋻⋼⋽⋾⋿"))
246
;; Intersections, unions etc.
248
("intersection" . ,(agda-input-to-string-list "∩⋂∧⋀⋏⨇⊓⨅⋒∏ ⊼ ⨉"))
249
("union" . ,(agda-input-to-string-list "∪⋃∨⋁⋎⨈⊔⨆⋓∐⨿⊽⊻⊍⨃⊎⨄⊌∑⅀"))
251
("and" . ("∧")) ("or" . ("∨"))
252
("And" . ("⋀")) ("Or" . ("⋁"))
253
("i" . ("∩")) ("un" . ("∪")) ("u+" . ("⊎")) ("u." . ("⊍"))
254
("I" . ("⋂")) ("Un" . ("⋃")) ("U+" . ("⨄")) ("U." . ("⨃"))
255
("glb" . ("⊓")) ("lub" . ("⊔"))
256
("Glb" . ("⨅")) ("Lub" . ("⨆"))
260
("entails" . ,(agda-input-to-string-list "⊢⊣⊤⊥⊦⊧⊨⊩⊪⊫⊬⊭⊮⊯"))
262
("|-" . ("⊢")) ("|-n" . ("⊬"))
264
("|=" . ("⊨")) ("|=n" . ("⊭"))
265
("||-" . ("⊩")) ("||-n" . ("⊮"))
266
("||=" . ("⊫")) ("||=n" . ("⊯"))
269
;; Divisibility, parallelity.
271
("|" . ("∣")) ("|n" . ("∤"))
272
("||" . ("∥")) ("||n" . ("∦"))
274
;; Some symbols from logic and set theory.
282
;; Corners, ceilings and floors.
284
("c" . ,(agda-input-to-string-list "⌜⌝⌞⌟⌈⌉⌊⌋"))
285
("cu" . ,(agda-input-to-string-list "⌜⌝ ⌈⌉ "))
286
("cl" . ,(agda-input-to-string-list " ⌞⌟ ⌊⌋"))
288
("cul" . ("⌜")) ("cuL" . ("⌈"))
289
("cur" . ("⌝")) ("cuR" . ("⌉"))
290
("cll" . ("⌞")) ("clL" . ("⌊"))
291
("clr" . ("⌟")) ("clR" . ("⌋"))
293
;; Various operators/symbols.
310
("increment" . ("∆"))
313
;; Circled operators.
339
("integral" . ,(agda-input-to-string-list "∫∬∭∮∯∰∱∲∳"))
340
("angle" . ,(agda-input-to-string-list "∟∡∢⊾⊿"))
341
("join" . ,(agda-input-to-string-list "⋈⋉⋊⋋⋌⨝⟕⟖⟗"))
345
("l" . ,(agda-input-to-string-list "←⇐⇚⇇⇆↤⇦↞↼↽⇠⇺↜⇽⟵⟸↚⇍⇷ ↹ ↢↩↫⇋⇜⇤⟻⟽⤆↶↺⟲ "))
346
("r" . ,(agda-input-to-string-list "→⇒⇛⇉⇄↦⇨↠⇀⇁⇢⇻↝⇾⟶⟹↛⇏⇸⇶ ↴ ↣↪↬⇌⇝⇥⟼⟾⤇↷↻⟳⇰⇴⟴⟿ ➵➸➙➔➛➜➝➞➟➠➡➢➣➤➧➨➩➪➫➬➭➮➯➱➲➳➺➻➼➽➾"))
347
("u" . ,(agda-input-to-string-list "↑⇑⟰⇈⇅↥⇧↟↿↾⇡⇞ ↰↱➦ ⇪⇫⇬⇭⇮⇯ "))
348
("d" . ,(agda-input-to-string-list "↓⇓⟱⇊⇵↧⇩↡⇃⇂⇣⇟ ↵↲↳➥ ↯ "))
349
("ud" . ,(agda-input-to-string-list "↕⇕ ↨⇳ "))
350
("lr" . ,(agda-input-to-string-list "↔⇔ ⇼↭⇿⟷⟺↮⇎⇹ "))
351
("ul" . ,(agda-input-to-string-list "↖⇖ ⇱↸ "))
352
("ur" . ,(agda-input-to-string-list "↗⇗ ➶➹➚ "))
353
("dr" . ,(agda-input-to-string-list "↘⇘ ⇲ ➴➷➘ "))
354
("dl" . ,(agda-input-to-string-list "↙⇙ "))
356
("l-" . ("←")) ("<-" . ("←")) ("l=" . ("⇐"))
357
("r-" . ("→")) ("->" . ("→")) ("r=" . ("⇒")) ("=>" . ("⇒"))
358
("u-" . ("↑")) ("u=" . ("⇑"))
359
("d-" . ("↓")) ("d=" . ("⇓"))
360
("ud-" . ("↕")) ("ud=" . ("⇕"))
361
("lr-" . ("↔")) ("<->" . ("↔")) ("lr=" . ("⇔")) ("<=>" . ("⇔"))
362
("ul-" . ("↖")) ("ul=" . ("⇖"))
363
("ur-" . ("↗")) ("ur=" . ("⇗"))
364
("dr-" . ("↘")) ("dr=" . ("⇘"))
365
("dl-" . ("↙")) ("dl=" . ("⇙"))
367
("l==" . ("⇚")) ("l-2" . ("⇇")) ("l-r-" . ("⇆"))
368
("r==" . ("⇛")) ("r-2" . ("⇉")) ("r-3" . ("⇶")) ("r-l-" . ("⇄"))
369
("u==" . ("⟰")) ("u-2" . ("⇈")) ("u-d-" . ("⇅"))
370
("d==" . ("⟱")) ("d-2" . ("⇊")) ("d-u-" . ("⇵"))
372
("l--" . ("⟵")) ("<--" . ("⟵")) ("l~" . ("↜" "⇜"))
373
("r--" . ("⟶")) ("-->" . ("⟶")) ("r~" . ("↝" "⇝" "⟿"))
374
("lr--" . ("⟷")) ("<-->" . ("⟷")) ("lr~" . ("↭"))
376
("l-n" . ("↚")) ("<-n" . ("↚")) ("l=n" . ("⇍"))
377
("r-n" . ("↛")) ("->n" . ("↛")) ("r=n" . ("⇏")) ("=>n" . ("⇏"))
378
("lr-n" . ("↮")) ("<->n" . ("↮")) ("lr=n" . ("⇎")) ("<=>n" . ("⇎"))
380
("l-|" . ("↤")) ("ll-" . ("↞"))
381
("r-|" . ("↦")) ("rr-" . ("↠"))
382
("u-|" . ("↥")) ("uu-" . ("↟"))
383
("d-|" . ("↧")) ("dd-" . ("↡"))
390
("..." . ,(agda-input-to-string-list "⋯⋮⋰⋱"))
392
;; Box-drawing characters.
394
("---" . ,(agda-input-to-string-list "─│┌┐└┘├┤┬┼┴╴╵╶╷╭╮╯╰╱╲╳"))
395
("--=" . ,(agda-input-to-string-list "═║╔╗╚╝╠╣╦╬╩ ╒╕╘╛╞╡╤╪╧ ╓╖╙╜╟╢╥╫╨"))
396
("--_" . ,(agda-input-to-string-list "━┃┏┓┗┛┣┫┳╋┻╸╹╺╻
397
┍┯┑┕┷┙┝┿┥┎┰┒┖┸┚┠╂┨┞╀┦┟╁┧┢╈┪┡╇┩
398
┮┭┶┵┾┽┲┱┺┹╊╉╆╅╄╃ ╿╽╼╾"))
399
("--." . ,(agda-input-to-string-list "╌╎┄┆┈┊
404
;; Big/small, black/white.
406
("t" . ,(agda-input-to-string-list "◂◃◄◅▸▹►▻▴▵▾▿◢◿◣◺◤◸◥◹"))
407
("T" . ,(agda-input-to-string-list "◀◁▶▷▲△▼▽◬◭◮"))
409
("tb" . ,(agda-input-to-string-list "◂▸▴▾◄►◢◣◤◥"))
410
("tw" . ,(agda-input-to-string-list "◃▹▵▿◅▻◿◺◸◹"))
412
("Tb" . ,(agda-input-to-string-list "◀▶▲▼"))
413
("Tw" . ,(agda-input-to-string-list "◁▷△▽"))
417
("sq" . ,(agda-input-to-string-list "■□◼◻◾◽▣▢▤▥▦▧▨▩◧◨◩◪◫◰◱◲◳"))
418
("sqb" . ,(agda-input-to-string-list "■◼◾"))
419
("sqw" . ,(agda-input-to-string-list "□◻◽"))
425
("re" . ,(agda-input-to-string-list "▬▭▮▯"))
426
("reb" . ,(agda-input-to-string-list "▬▮"))
427
("rew" . ,(agda-input-to-string-list "▭▯"))
431
("pa" . ,(agda-input-to-string-list "▰▱"))
437
("di" . ,(agda-input-to-string-list "◆◇◈"))
444
("ci" . ,(agda-input-to-string-list "●○◎◌◯◍◐◑◒◓◔◕◖◗◠◡◴◵◶◷⚆⚇⚈⚉"))
453
("st" . ,(agda-input-to-string-list "⋆✦✧✶✴✹ ★☆✪✫✯✰✵✷✸"))
454
("st4" . ,(agda-input-to-string-list "✦✧"))
459
;; Blackboard bold letters.
471
("(" . ,(agda-input-to-string-list "([{⁅⁽₍〈⎴⟦⟨⟪〈《「『【〔〖〚︵︷︹︻︽︿﹁﹃﹙﹛﹝（［｛｢"))
472
(")" . ,(agda-input-to-string-list ")]}⁆⁾₎〉⎵⟧⟩⟫〉》」』】〕〗〛︶︸︺︼︾﹀﹂﹄﹚﹜﹞）］｝｣"))
483
("'" . ,(agda-input-to-string-list "′″‴⁗"))
484
("`" . ,(agda-input-to-string-list "‵‶‷"))
488
("frac" . ,(agda-input-to-string-list "¼½¾⅓⅔⅕⅖⅗⅘⅙⅚⅛⅜⅝⅞⅟"))
492
("bu" . ,(agda-input-to-string-list "•◦‣⁌⁍"))
499
("note" . ,(agda-input-to-string-list "♩♪♫♬"))
503
;; Other punctuation and symbols.
513
("die" . ,(agda-input-to-string-list "⚀⚁⚂⚃⚄⚅"))
514
("asterisk" . ,(agda-input-to-string-list "⁎⁑⁂✢✣✤✥✱✲✳✺✻✼✽❃❉❊❋"))
518
("apl" . ,(agda-input-to-string-list "⌶⌷⌸⌹⌺⌻⌼⌽⌾⌿⍀⍁⍂⍃⍄⍅⍆⍇⍈
523
;; Shorter forms of many greek letters.
525
("Ga" . ("α")) ("GA" . ("Α"))
526
("Gb" . ("β")) ("GB" . ("Β"))
527
("Gg" . ("γ")) ("GG" . ("Γ"))
528
("Gd" . ("δ")) ("GD" . ("Δ"))
529
("Ge" . ("ε")) ("GE" . ("Ε"))
530
("Gz" . ("ζ")) ("GZ" . ("Ζ"))
532
("Gth" . ("θ")) ("GTH" . ("θ"))
533
("Gi" . ("ι")) ("GI" . ("Ι"))
534
("Gk" . ("κ")) ("GK" . ("Κ"))
535
("Gl" . ("λ")) ("GL" . ("Λ"))
536
("Gm" . ("μ")) ("GM" . ("Μ"))
537
("Gn" . ("ν")) ("GN" . ("Ν"))
538
("Gx" . ("ξ")) ("GX" . ("Ξ"))
541
("Gr" . ("ρ")) ("GR" . ("Ρ"))
542
("Gs" . ("σ")) ("GS" . ("Σ"))
543
("Gt" . ("τ")) ("GT" . ("Τ"))
544
("Gu" . ("υ")) ("GU" . ("Υ"))
545
("Gf" . ("φ")) ("GF" . ("Φ"))
546
("Gc" . ("χ")) ("GC" . ("Χ"))
547
("Gp" . ("ψ")) ("GP" . ("Ψ"))
548
("Go" . ("ω")) ("GO" . ("Ω"))
550
;; Some ISO8859-1 characters.
555
("brokenbar" . ("¦"))
561
;; Circled, parenthesised etc. numbers and letters.
563
( "(0)" . ,(agda-input-to-string-list " ⓪"))
564
( "(1)" . ,(agda-input-to-string-list "⑴①⒈❶➀➊"))
565
( "(2)" . ,(agda-input-to-string-list "⑵②⒉❷➁➋"))
566
( "(3)" . ,(agda-input-to-string-list "⑶③⒊❸➂➌"))
567
( "(4)" . ,(agda-input-to-string-list "⑷④⒋❹➃➍"))
568
( "(5)" . ,(agda-input-to-string-list "⑸⑤⒌❺➄➎"))
569
( "(6)" . ,(agda-input-to-string-list "⑹⑥⒍❻➅➏"))
570
( "(7)" . ,(agda-input-to-string-list "⑺⑦⒎❼➆➐"))
571
( "(8)" . ,(agda-input-to-string-list "⑻⑧⒏❽➇➑"))
572
( "(9)" . ,(agda-input-to-string-list "⑼⑨⒐❾➈➒"))
573
("(10)" . ,(agda-input-to-string-list "⑽⑩⒑❿➉➓"))
574
("(11)" . ,(agda-input-to-string-list "⑾⑪⒒"))
575
("(12)" . ,(agda-input-to-string-list "⑿⑫⒓"))
576
("(13)" . ,(agda-input-to-string-list "⒀⑬⒔"))
577
("(14)" . ,(agda-input-to-string-list "⒁⑭⒕"))
578
("(15)" . ,(agda-input-to-string-list "⒂⑮⒖"))
579
("(16)" . ,(agda-input-to-string-list "⒃⑯⒗"))
580
("(17)" . ,(agda-input-to-string-list "⒄⑰⒘"))
581
("(18)" . ,(agda-input-to-string-list "⒅⑱⒙"))
582
("(19)" . ,(agda-input-to-string-list "⒆⑲⒚"))
583
("(20)" . ,(agda-input-to-string-list "⒇⑳⒛"))
585
("(a)" . ,(agda-input-to-string-list "⒜Ⓐⓐ"))
586
("(b)" . ,(agda-input-to-string-list "⒝Ⓑⓑ"))
587
("(c)" . ,(agda-input-to-string-list "⒞Ⓒⓒ"))
588
("(d)" . ,(agda-input-to-string-list "⒟Ⓓⓓ"))
589
("(e)" . ,(agda-input-to-string-list "⒠Ⓔⓔ"))
590
("(f)" . ,(agda-input-to-string-list "⒡Ⓕⓕ"))
591
("(g)" . ,(agda-input-to-string-list "⒢Ⓖⓖ"))
592
("(h)" . ,(agda-input-to-string-list "⒣Ⓗⓗ"))
593
("(i)" . ,(agda-input-to-string-list "⒤Ⓘⓘ"))
594
("(j)" . ,(agda-input-to-string-list "⒥Ⓙⓙ"))
595
("(k)" . ,(agda-input-to-string-list "⒦Ⓚⓚ"))
596
("(l)" . ,(agda-input-to-string-list "⒧Ⓛⓛ"))
597
("(m)" . ,(agda-input-to-string-list "⒨Ⓜⓜ"))
598
("(n)" . ,(agda-input-to-string-list "⒩Ⓝⓝ"))
599
("(o)" . ,(agda-input-to-string-list "⒪Ⓞⓞ"))
600
("(p)" . ,(agda-input-to-string-list "⒫Ⓟⓟ"))
601
("(q)" . ,(agda-input-to-string-list "⒬Ⓠⓠ"))
602
("(r)" . ,(agda-input-to-string-list "⒭Ⓡⓡ"))
603
("(s)" . ,(agda-input-to-string-list "⒮Ⓢⓢ"))
604
("(t)" . ,(agda-input-to-string-list "⒯Ⓣⓣ"))
605
("(u)" . ,(agda-input-to-string-list "⒰Ⓤⓤ"))
606
("(v)" . ,(agda-input-to-string-list "⒱Ⓥⓥ"))
607
("(w)" . ,(agda-input-to-string-list "⒲Ⓦⓦ"))
608
("(x)" . ,(agda-input-to-string-list "⒳Ⓧⓧ"))
609
("(y)" . ,(agda-input-to-string-list "⒴Ⓨⓨ"))
610
("(z)" . ,(agda-input-to-string-list "⒵Ⓩⓩ"))
613
"A list of translations specific to the Agda input method.
614
Each element is a pair (KEY-SEQUENCE-STRING . LIST-OF-TRANSLATION-STRINGS).
615
All the translation strings are possible translations
616
of the given key sequence; if there is more than one you can choose
617
between them using the arrow keys.
619
Note that if you customize this setting you will not
620
automatically benefit (or suffer) from modifications to its
621
default value when the library is updated. If you just want to
622
add some bindings it is probably a better idea to customize
623
`agda-input-user-translations'.
625
These translation pairs are included after those in
626
`agda-input-user-translations', but before the ones inherited
627
from other input methods (see `agda-input-inherit').
629
If you change this setting manually (without using the
630
customization buffer) you need to call `agda-input-setup' in
631
order for the change to take effect."
633
:set 'agda-input-incorporate-changed-setting
634
:initialize 'custom-initialize-default
635
:type '(repeat (cons (string :tag "Key sequence")
636
(repeat :tag "Translations" string))))
638
(defcustom agda-input-user-translations nil
639
"Like `agda-input-translations', but more suitable for user
640
customizations since by default it is empty.
642
These translation pairs are included first, before those in
643
`agda-input-translations' and the ones inherited from other input
646
:set 'agda-input-incorporate-changed-setting
647
:initialize 'custom-initialize-default
648
:type '(repeat (cons (string :tag "Key sequence")
649
(repeat :tag "Translations" string))))
651
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
652
;; Inspecting and modifying translation maps
654
(defun agda-input-get-translations (qp)
655
"Return a list containing all translations from the Quail
656
package QP (except for those corresponding to ASCII).
657
Each pair in the list has the form (KEY-SEQUENCE . TRANSLATION)."
659
(activate-input-method qp) ; To make sure that the package is loaded.
660
(unless (quail-package qp)
661
(error "%s is not a Quail package." qp))
662
(let ((decode-map (list 'decode-map)))
663
(quail-build-decode-map (list (quail-map)) "" decode-map 0)
666
(defun agda-input-show-translations (qp)
667
"Display all translations used by the Quail package QP (a string).
668
\(Except for those corresponding to ASCII)."
669
(interactive (list (read-input-method-name
670
"Quail input method (default %s): " "Agda")))
671
(let ((buf (concat "*" qp " input method translations*")))
672
(with-output-to-temp-buffer buf
673
(with-current-buffer buf
674
(quail-insert-decode-map
675
(cons 'decode-map (agda-input-get-translations qp)))))))
677
(defun agda-input-add-translations (trans)
678
"Add the given translations TRANS to the Agda input method.
679
TRANS is a list of pairs (KEY-SEQUENCE . TRANSLATION). The
680
translations are appended to the current translations."
682
(dolist (tr (agda-input-concat-map (eval agda-input-tweak-all) trans))
683
(quail-defrule (car tr) (cdr tr) "Agda" t))))
685
(defun agda-input-inherit-package (qp &optional fun)
686
"Let the Agda input method inherit the translations from the
687
Quail package QP (except for those corresponding to ASCII).
689
The optional function FUN can be used to modify the translations.
690
It is given a pair (KEY-SEQUENCE . TRANSLATION) and should return
691
a list of such pairs."
692
(let ((trans (agda-input-get-translations qp)))
693
(agda-input-add-translations
694
(if fun (agda-input-concat-map fun trans)
697
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
698
;; Setting up the input method
700
(defun agda-input-setup ()
701
"Set up the Agda input method based on the customisable
702
variables and underlying input methods."
704
;; Create (or reset) the input method.
706
(quail-define-package "Agda" "UTF-8" "∏" t ; guidance
708
The purpose of this input method is to edit Agda programs, but
709
since it is highly customisable it can be made useful for other
711
nil nil nil nil nil nil t ; maximum-shortest
714
(agda-input-add-translations
715
(mapcar (lambda (tr) (cons (car tr) (vconcat (cdr tr))))
716
(append agda-input-user-translations
717
agda-input-translations)))
718
(dolist (def agda-input-inherit)
719
(agda-input-inherit-package (car def)
722
(defun agda-input-incorporate-changed-setting (sym val)
723
"Update the Agda input method based on the customisable
724
variables and underlying input methods.
725
Suitable for use in the :set field of `defcustom'."
726
(set-default sym val)
729
;; Set up the input method.
733
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
734
;; Administrative details
736
(provide 'agda-input)
737
;;; agda-input.el ends here
added
removed
src/data/emacs-mode/agda-input.el
