← Back to branch summary

~ubuntu-branches/ubuntu/trusty/agda/trusty

« back to all changes in this revision

Viewing changes to src/data/emacs-mode/agda-input.el

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2011-11-23 10:12:59 UTC
  • mfrom: (12.1.3 sid)
  • Revision ID: package-import@ubuntu.com-20111123101259-zhs3e4ynpck20hmu
Tags: 2.3.0-1
* [c0e4746] Imported Upstream version 2.3.0. New/changed features include:
  + New more liberal syntax for mutually recursive definitions
  + Pattern matching on lambdas
  + New syntax for updating (some fields of) records
  + Universe polymorphism is now enabled by default
  + New type of hidden function argument: instance arguments
  + Dependent irrelevant function types and records with irrelevant fields
  + See http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Version-2-3-0
    for a full list
* [369ed3a] Update BDs in line with cabal requirements in new upstream
* [3798aee] Remove all patches. They are all now upstream.

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/data/emacs-mode/agda-input.el
41
41
            (list (string c))))
42
42
   (string-to-list s)))
43
43
 
 
44
(defun agda-input-character-range (from to)
 
45
  "A string consisting of the characters from FROM to TO."
 
46
  (let (seq)
 
47
    (dotimes (i (1+ (- to from)))
 
48
      (setq seq (cons (+ from i) seq)))
 
49
    (concat (nreverse seq))))
 
50
 
44
51
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
45
52
;; Functions used to tweak translation pairs
46
53
 
383
390
  ("d-|"  . ("↧"))  ("dd-" . ("↡"))
384
391
  ("ud-|" . ("↨"))
385
392
 
 
393
  ("l->" . ("↢"))
 
394
  ("r->" . ("↣"))
 
395
 
386
396
  ("dz" . ("↯"))
387
397
 
388
398
  ;; Ellipsis.
468
478
 
469
479
  ;; Parentheses.
470
480
 
471
 
  ("(" . ,(agda-input-to-string-list "([{⁅⁽₍〈⎴⟦⟨⟪〈《「『【〔〖〚︵︷︹︻︽︿﹁﹃﹙﹛﹝（［｛｢"))
472
 
  (")" . ,(agda-input-to-string-list ")]}⁆⁾₎〉⎵⟧⟩⟫〉》」』】〕〗〛︶︸︺︼︾﹀﹂﹄﹚﹜﹞）］｝｣"))
 
481
  ("(" . ,(agda-input-to-string-list "([{⁅⁽₍〈⎴⟅⟦⟨⟪⦃〈《「『【〔〖〚︵︷︹︻︽︿﹁﹃﹙﹛﹝（［｛｢"))
 
482
  (")" . ,(agda-input-to-string-list ")]}⁆⁾₎〉⎵⟆⟧⟩⟫⦄〉》」』】〕〗〛︶︸︺︼︾﹀﹂﹄﹚﹜﹞）］｝｣"))
473
483
 
474
484
  ("[[" . ("⟦"))
475
485
  ("]]" . ("⟧"))
477
487
  (">"  . ("⟩"))
478
488
  ("<<" . ("⟪"))
479
489
  (">>" . ("⟫"))
 
490
  ("{{" . ("⦃"))
 
491
  ("}}" . ("⦄"))
 
492
 
 
493
  ("(b" . ("⟅"))
 
494
  (")b" . ("⟆"))
 
495
 
 
496
  ("lbag" . ("⟅"))
 
497
  ("rbag" . ("⟆"))
480
498
 
481
499
  ;; Primes.
482
500
 
520
538
                                               ⍜⍝⍞⍟⍠⍡⍢⍣⍤⍥⍦⍧⍨⍩⍪⍫⍬⍭⍮
521
539
                                               ⍯⍰⍱⍲⍳⍴⍵⍶⍷⍸⍹⍺⎕"))
522
540
 
 
541
  ;; Some combining characters.
 
542
  ;;
 
543
  ;; The following combining characters also have (other)
 
544
  ;; translations:
 
545
  ;; ̀ ́ ̂ ̃ ̄ ̆ ̇ ̈ ̋ ̌ ̣ ̧ ̱
 
546
 
 
547
  ("^--" . ,(agda-input-to-string-list"̅̿"))
 
548
  ("_--" . ,(agda-input-to-string-list"̲̳"))
 
549
  ("^~"  . ,(agda-input-to-string-list"̃͌"))
 
550
  ("_~"  .  (                         "̰"))
 
551
  ("^."  . ,(agda-input-to-string-list"̇̈⃛⃜"))
 
552
  ("_."  . ,(agda-input-to-string-list"̣̤"))
 
553
  ("^l"  . ,(agda-input-to-string-list"⃖⃐⃔"))
 
554
  ("^l-" .  (                         "⃖"))
 
555
  ("^r"  . ,(agda-input-to-string-list"⃗⃑⃕"))
 
556
  ("^r-" .  (                         "⃗"))
 
557
  ("^lr" .  (                         "⃡"))
 
558
  ("_lr" .  (                         "͍"))
 
559
  ("^^"  . ,(agda-input-to-string-list"̂̑͆"))
 
560
  ("_^"  . ,(agda-input-to-string-list"̭̯̪"))
 
561
  ("^v"  . ,(agda-input-to-string-list"̌̆"))
 
562
  ("_v"  . ,(agda-input-to-string-list"̬̮̺"))
 
563
 
523
564
  ;; Shorter forms of many greek letters plus ƛ.
524
565
 
525
566
  ("Ga"  . ("α"))  ("GA"  . ("Α"))