← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« 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: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/data/emacs-mode/agda-input.el
315
315
  ("surd4"     . ("∜"))
316
316
  ("increment" . ("∆"))
317
317
  ("inf"       . ("∞"))
 
318
  ("&"         . ("⅋"))
318
319
 
319
320
  ;; Circled operators.
320
321
 
348
349
 
349
350
  ;; Arrows.
350
351
 
351
 
  ("l"  . ,(agda-input-to-string-list "←⇐⇚⇇⇆↤⇦↞↼↽⇠⇺↜⇽⟵⟸↚⇍⇷ ↹     ↢↩↫⇋⇜⇤⟻⟽⤆↶↺⟲                                    "))
352
 
  ("r"  . ,(agda-input-to-string-list "→⇒⇛⇉⇄↦⇨↠⇀⇁⇢⇻↝⇾⟶⟹↛⇏⇸⇶ ↴    ↣↪↬⇌⇝⇥⟼⟾⤇↷↻⟳⇰⇴⟴⟿ ➵➸➙➔➛➜➝➞➟➠➡➢➣➤➧➨➩➪➫➬➭➮➯➱➲➳➺➻➼➽➾"))
353
 
  ("u"  . ,(agda-input-to-string-list "↑⇑⟰⇈⇅↥⇧↟↿↾⇡⇞          ↰↱➦ ⇪⇫⇬⇭⇮⇯                                          "))
354
 
  ("d"  . ,(agda-input-to-string-list "↓⇓⟱⇊⇵↧⇩↡⇃⇂⇣⇟         ↵↲↳➥ ↯                                               "))
355
 
  ("ud" . ,(agda-input-to-string-list "↕⇕   ↨⇳                                                                   "))
356
 
  ("lr" . ,(agda-input-to-string-list "↔⇔         ⇼↭⇿⟷⟺↮⇎⇹                                                       "))
357
 
  ("ul" . ,(agda-input-to-string-list "↖⇖                        ⇱↸                                              "))
358
 
  ("ur" . ,(agda-input-to-string-list "↗⇗                                         ➶➹➚                            "))
359
 
  ("dr" . ,(agda-input-to-string-list "↘⇘                        ⇲                ➴➷➘                            "))
360
 
  ("dl" . ,(agda-input-to-string-list "↙⇙                                                                        "))
 
352
  ("l"  . ,(agda-input-to-string-list "←⇐⇚⇇⇆↤⇦↞↼↽⇠⇺↜⇽⟵⟸↚⇍⇷ ↹     ↢↩↫⇋⇜⇤⟻⟽⤆↶↺⟲                                     "))
 
353
  ("r"  . ,(agda-input-to-string-list "→⇒⇛⇉⇄↦⇨↠⇀⇁⇢⇻↝⇾⟶⟹↛⇏⇸⇶ ↴    ↣↪↬⇌⇝⇥⟼⟾⤇↷↻⟳⇰⇴⟴⟿ ➵➸➙➔➛➜➝➞➟➠➡➢➣➤➧➨➩➪➫➬➭➮➯➱➲➳➺➻➼➽➾⊸"))
 
354
  ("u"  . ,(agda-input-to-string-list "↑⇑⟰⇈⇅↥⇧↟↿↾⇡⇞          ↰↱➦ ⇪⇫⇬⇭⇮⇯                                           "))
 
355
  ("d"  . ,(agda-input-to-string-list "↓⇓⟱⇊⇵↧⇩↡⇃⇂⇣⇟         ↵↲↳➥ ↯                                                "))
 
356
  ("ud" . ,(agda-input-to-string-list "↕⇕   ↨⇳                                                                    "))
 
357
  ("lr" . ,(agda-input-to-string-list "↔⇔         ⇼↭⇿⟷⟺↮⇎⇹                                                        "))
 
358
  ("ul" . ,(agda-input-to-string-list "↖⇖                        ⇱↸                                               "))
 
359
  ("ur" . ,(agda-input-to-string-list "↗⇗                                         ➶➹➚                             "))
 
360
  ("dr" . ,(agda-input-to-string-list "↘⇘                        ⇲                ➴➷➘                             "))
 
361
  ("dl" . ,(agda-input-to-string-list "↙⇙                                                                         "))
361
362
 
362
363
  ("l-"  . ("←"))  ("<-"  . ("←"))  ("l="  . ("⇐"))
363
364
  ("r-"  . ("→"))  ("->"  . ("→"))  ("r="  . ("⇒"))  ("=>"  . ("⇒"))
392
393
  ("l->" . ("↢"))
393
394
  ("r->" . ("↣"))
394
395
 
 
396
  ("r-o" . ("⊸"))  ("-o"  . ("⊸"))
 
397
 
395
398
  ("dz" . ("↯"))
396
399
 
397
400
  ;; Ellipsis.
473
476
  ("br"   . ("ℝ"))
474
477
  ("bc"   . ("ℂ"))
475
478
  ("bp"   . ("ℙ"))
 
479
  ("bb"   . ("𝔹"))
476
480
  ("bsum" . ("⅀"))
477
481
 
 
482
  ;; Blackboard bold numbers.
 
483
 
 
484
  ("b0"   . ("𝟘"))
 
485
  ("b1"   . ("𝟙"))
 
486
  ("b2"   . ("𝟚"))
 
487
  ("b3"   . ("𝟛"))
 
488
  ("b4"   . ("𝟜"))
 
489
  ("b5"   . ("𝟝"))
 
490
  ("b6"   . ("𝟞"))
 
491
  ("b7"   . ("𝟟"))
 
492
  ("b8"   . ("𝟠"))
 
493
  ("b9"   . ("𝟡"))
 
494
 
478
495
  ;; Parentheses.
479
496
 
480
497
  ("(" . ,(agda-input-to-string-list "([{⁅⁽₍〈⎴⟅⟦⟨⟪⦃〈《「『【〔〖〚︵︷︹︻︽︿﹁﹃﹙﹛﹝（［｛｢"))
587
604
  ("Gp"  . ("ψ"))  ("GP"  . ("Ψ"))
588
605
  ("Go"  . ("ω"))  ("GO"  . ("Ω"))
589
606
 
 
607
  ;; Mathematical characters
 
608
 
 
609
  ("MiA" . ("𝐴"))
 
610
  ("MiB" . ("𝐵"))
 
611
  ("MiC" . ("𝐶"))
 
612
  ("MiD" . ("𝐷"))
 
613
  ("MiE" . ("𝐸"))
 
614
  ("MiF" . ("𝐹"))
 
615
  ("MiG" . ("𝐺"))
 
616
  ("MiH" . ("𝐻"))
 
617
  ("MiI" . ("𝐼"))
 
618
  ("MiJ" . ("𝐽"))
 
619
  ("MiK" . ("𝐾"))
 
620
  ("MiL" . ("𝐿"))
 
621
  ("MiM" . ("𝑀"))
 
622
  ("MiN" . ("𝑁"))
 
623
  ("MiO" . ("𝑂"))
 
624
  ("MiP" . ("𝑃"))
 
625
  ("MiQ" . ("𝑄"))
 
626
  ("MiR" . ("𝑅"))
 
627
  ("MiS" . ("𝑆"))
 
628
  ("MiT" . ("𝑇"))
 
629
  ("MiU" . ("𝑈"))
 
630
  ("MiV" . ("𝑉"))
 
631
  ("MiW" . ("𝑊"))
 
632
  ("MiX" . ("𝑋"))
 
633
  ("MiY" . ("𝑌"))
 
634
  ("MiZ" . ("𝑍"))
 
635
  ("Mia" . ("𝑎"))
 
636
  ("Mib" . ("𝑏"))
 
637
  ("Mic" . ("𝑐"))
 
638
  ("Mid" . ("𝑑"))
 
639
  ("Mie" . ("𝑒"))
 
640
  ("Mif" . ("𝑓"))
 
641
  ("Mig" . ("𝑔"))
 
642
  ("Mii" . ("𝑖"))
 
643
  ("Mij" . ("𝑗"))
 
644
  ("Mik" . ("𝑘"))
 
645
  ("Mil" . ("𝑙"))
 
646
  ("Mim" . ("𝑚"))
 
647
  ("Min" . ("𝑛"))
 
648
  ("Mio" . ("𝑜"))
 
649
  ("Mip" . ("𝑝"))
 
650
  ("Miq" . ("𝑞"))
 
651
  ("Mir" . ("𝑟"))
 
652
  ("Mis" . ("𝑠"))
 
653
  ("Mit" . ("𝑡"))
 
654
  ("Miu" . ("𝑢"))
 
655
  ("Miv" . ("𝑣"))
 
656
  ("Miw" . ("𝑤"))
 
657
  ("Mix" . ("𝑥"))
 
658
  ("Miy" . ("𝑦"))
 
659
  ("Miz" . ("𝑧"))
 
660
  ("MIA" . ("𝑨"))
 
661
  ("MIB" . ("𝑩"))
 
662
  ("MIC" . ("𝑪"))
 
663
  ("MID" . ("𝑫"))
 
664
  ("MIE" . ("𝑬"))
 
665
  ("MIF" . ("𝑭"))
 
666
  ("MIG" . ("𝑮"))
 
667
  ("MIH" . ("𝑯"))
 
668
  ("MII" . ("𝑰"))
 
669
  ("MIJ" . ("𝑱"))
 
670
  ("MIK" . ("𝑲"))
 
671
  ("MIL" . ("𝑳"))
 
672
  ("MIM" . ("𝑴"))
 
673
  ("MIN" . ("𝑵"))
 
674
  ("MIO" . ("𝑶"))
 
675
  ("MIP" . ("𝑷"))
 
676
  ("MIQ" . ("𝑸"))
 
677
  ("MIR" . ("𝑹"))
 
678
  ("MIS" . ("𝑺"))
 
679
  ("MIT" . ("𝑻"))
 
680
  ("MIU" . ("𝑼"))
 
681
  ("MIV" . ("𝑽"))
 
682
  ("MIW" . ("𝑾"))
 
683
  ("MIX" . ("𝑿"))
 
684
  ("MIY" . ("𝒀"))
 
685
  ("MIZ" . ("𝒁"))
 
686
  ("MIa" . ("𝒂"))
 
687
  ("MIb" . ("𝒃"))
 
688
  ("MIc" . ("𝒄"))
 
689
  ("MId" . ("𝒅"))
 
690
  ("MIe" . ("𝒆"))
 
691
  ("MIf" . ("𝒇"))
 
692
  ("MIg" . ("𝒈"))
 
693
  ("MIh" . ("𝒉"))
 
694
  ("MIi" . ("𝒊"))
 
695
  ("MIj" . ("𝒋"))
 
696
  ("MIk" . ("𝒌"))
 
697
  ("MIl" . ("𝒍"))
 
698
  ("MIm" . ("𝒎"))
 
699
  ("MIn" . ("𝒏"))
 
700
  ("MIo" . ("𝒐"))
 
701
  ("MIp" . ("𝒑"))
 
702
  ("MIq" . ("𝒒"))
 
703
  ("MIr" . ("𝒓"))
 
704
  ("MIs" . ("𝒔"))
 
705
  ("MIt" . ("𝒕"))
 
706
  ("MIu" . ("𝒖"))
 
707
  ("MIv" . ("𝒗"))
 
708
  ("MIw" . ("𝒘"))
 
709
  ("MIx" . ("𝒙"))
 
710
  ("MIy" . ("𝒚"))
 
711
  ("MIz" . ("𝒛"))
 
712
  ("McA" . ("𝒜"))
 
713
  ("McC" . ("𝒞"))
 
714
  ("McD" . ("𝒟"))
 
715
  ("McG" . ("𝒢"))
 
716
  ("McJ" . ("𝒥"))
 
717
  ("McK" . ("𝒦"))
 
718
  ("McN" . ("𝒩"))
 
719
  ("McO" . ("𝒪"))
 
720
  ("McP" . ("𝒫"))
 
721
  ("McQ" . ("𝒬"))
 
722
  ("McS" . ("𝒮"))
 
723
  ("McT" . ("𝒯"))
 
724
  ("McU" . ("𝒰"))
 
725
  ("McV" . ("𝒱"))
 
726
  ("McW" . ("𝒲"))
 
727
  ("McX" . ("𝒳"))
 
728
  ("McY" . ("𝒴"))
 
729
  ("McZ" . ("𝒵"))
 
730
  ("Mca" . ("𝒶"))
 
731
  ("Mcb" . ("𝒷"))
 
732
  ("Mcc" . ("𝒸"))
 
733
  ("Mcd" . ("𝒹"))
 
734
  ("Mcf" . ("𝒻"))
 
735
  ("Mch" . ("𝒽"))
 
736
  ("Mci" . ("𝒾"))
 
737
  ("Mcj" . ("𝒿"))
 
738
  ("Mck" . ("𝓀"))
 
739
  ("Mcl" . ("𝓁"))
 
740
  ("Mcm" . ("𝓂"))
 
741
  ("Mcn" . ("𝓃"))
 
742
  ("Mcp" . ("𝓅"))
 
743
  ("Mcq" . ("𝓆"))
 
744
  ("Mcr" . ("𝓇"))
 
745
  ("Mcs" . ("𝓈"))
 
746
  ("Mct" . ("𝓉"))
 
747
  ("Mcu" . ("𝓊"))
 
748
  ("Mcv" . ("𝓋"))
 
749
  ("Mcw" . ("𝓌"))
 
750
  ("Mcx" . ("𝓍"))
 
751
  ("Mcy" . ("𝓎"))
 
752
  ("Mcz" . ("𝓏"))
 
753
  ("MCA" . ("𝓐"))
 
754
  ("MCB" . ("𝓑"))
 
755
  ("MCC" . ("𝓒"))
 
756
  ("MCD" . ("𝓓"))
 
757
  ("MCE" . ("𝓔"))
 
758
  ("MCF" . ("𝓕"))
 
759
  ("MCG" . ("𝓖"))
 
760
  ("MCH" . ("𝓗"))
 
761
  ("MCI" . ("𝓘"))
 
762
  ("MCJ" . ("𝓙"))
 
763
  ("MCK" . ("𝓚"))
 
764
  ("MCL" . ("𝓛"))
 
765
  ("MCM" . ("𝓜"))
 
766
  ("MCN" . ("𝓝"))
 
767
  ("MCO" . ("𝓞"))
 
768
  ("MCP" . ("𝓟"))
 
769
  ("MCQ" . ("𝓠"))
 
770
  ("MCR" . ("𝓡"))
 
771
  ("MCS" . ("𝓢"))
 
772
  ("MCT" . ("𝓣"))
 
773
  ("MCU" . ("𝓤"))
 
774
  ("MCV" . ("𝓥"))
 
775
  ("MCW" . ("𝓦"))
 
776
  ("MCX" . ("𝓧"))
 
777
  ("MCY" . ("𝓨"))
 
778
  ("MCZ" . ("𝓩"))
 
779
  ("MCa" . ("𝓪"))
 
780
  ("MCb" . ("𝓫"))
 
781
  ("MCc" . ("𝓬"))
 
782
  ("MCd" . ("𝓭"))
 
783
  ("MCe" . ("𝓮"))
 
784
  ("MCf" . ("𝓯"))
 
785
  ("MCg" . ("𝓰"))
 
786
  ("MCh" . ("𝓱"))
 
787
  ("MCi" . ("𝓲"))
 
788
  ("MCj" . ("𝓳"))
 
789
  ("MCk" . ("𝓴"))
 
790
  ("MCl" . ("𝓵"))
 
791
  ("MCm" . ("𝓶"))
 
792
  ("MCn" . ("𝓷"))
 
793
  ("MCo" . ("𝓸"))
 
794
  ("MCp" . ("𝓹"))
 
795
  ("MCq" . ("𝓺"))
 
796
  ("MCr" . ("𝓻"))
 
797
  ("MCs" . ("𝓼"))
 
798
  ("MCt" . ("𝓽"))
 
799
  ("MCu" . ("𝓾"))
 
800
  ("MCv" . ("𝓿"))
 
801
  ("MCw" . ("𝔀"))
 
802
  ("MCx" . ("𝔁"))
 
803
  ("MCy" . ("𝔂"))
 
804
  ("MCz" . ("𝔃"))
 
805
  ("MfA" . ("𝔄"))
 
806
  ("MfB" . ("𝔅"))
 
807
  ("MfD" . ("𝔇"))
 
808
  ("MfE" . ("𝔈"))
 
809
  ("MfF" . ("𝔉"))
 
810
  ("MfG" . ("𝔊"))
 
811
  ("MfJ" . ("𝔍"))
 
812
  ("MfK" . ("𝔎"))
 
813
  ("MfL" . ("𝔏"))
 
814
  ("MfM" . ("𝔐"))
 
815
  ("MfN" . ("𝔑"))
 
816
  ("MfO" . ("𝔒"))
 
817
  ("MfP" . ("𝔓"))
 
818
  ("MfQ" . ("𝔔"))
 
819
  ("MfS" . ("𝔖"))
 
820
  ("MfT" . ("𝔗"))
 
821
  ("MfU" . ("𝔘"))
 
822
  ("MfV" . ("𝔙"))
 
823
  ("MfW" . ("𝔚"))
 
824
  ("MfX" . ("𝔛"))
 
825
  ("MfY" . ("𝔜"))
 
826
  ("Mfa" . ("𝔞"))
 
827
  ("Mfb" . ("𝔟"))
 
828
  ("Mfc" . ("𝔠"))
 
829
  ("Mfd" . ("𝔡"))
 
830
  ("Mfe" . ("𝔢"))
 
831
  ("Mff" . ("𝔣"))
 
832
  ("Mfg" . ("𝔤"))
 
833
  ("Mfh" . ("𝔥"))
 
834
  ("Mfi" . ("𝔦"))
 
835
  ("Mfj" . ("𝔧"))
 
836
  ("Mfk" . ("𝔨"))
 
837
  ("Mfl" . ("𝔩"))
 
838
  ("Mfm" . ("𝔪"))
 
839
  ("Mfn" . ("𝔫"))
 
840
  ("Mfo" . ("𝔬"))
 
841
  ("Mfp" . ("𝔭"))
 
842
  ("Mfq" . ("𝔮"))
 
843
  ("Mfr" . ("𝔯"))
 
844
  ("Mfs" . ("𝔰"))
 
845
  ("Mft" . ("𝔱"))
 
846
  ("Mfu" . ("𝔲"))
 
847
  ("Mfv" . ("𝔳"))
 
848
  ("Mfw" . ("𝔴"))
 
849
  ("Mfx" . ("𝔵"))
 
850
  ("Mfy" . ("𝔶"))
 
851
  ("Mfz" . ("𝔷"))
 
852
 
 
853
  ;; (Sub / Super) scripts
 
854
 
 
855
  ("_a" . ("ₐ"))
 
856
  ("_e" . ("ₑ"))
 
857
  ("_h" . ("ₕ"))
 
858
  ("_i" . ("ᵢ"))
 
859
  ("_j" . ("ⱼ"))
 
860
  ("_k" . ("ₖ"))
 
861
  ("_l" . ("ₗ"))
 
862
  ("_m" . ("ₘ"))
 
863
  ("_n" . ("ₙ"))
 
864
  ("_o" . ("ₒ"))
 
865
  ("_p" . ("ₚ"))
 
866
  ("_r" . ("ᵣ"))
 
867
  ("_s" . ("ₛ"))
 
868
  ("_t" . ("ₜ"))
 
869
  ("_u" . ("ᵤ"))
 
870
  ("_v" . ("ᵥ"))
 
871
  ("_x" . ("ₓ"))
 
872
 
 
873
  ("^a" . ("ᵃ"))
 
874
  ("^b" . ("ᵇ"))
 
875
  ("^c" . ("ᶜ"))
 
876
  ("^d" . ("ᵈ"))
 
877
  ("^e" . ("ᵉ"))
 
878
  ("^f" . ("ᶠ"))
 
879
  ("^g" . ("ᵍ"))
 
880
  ("^h" . ("ʰ"))
 
881
  ("^i" . ("ⁱ"))
 
882
  ("^j" . ("ʲ"))
 
883
  ("^k" . ("ᵏ"))
 
884
  ("^l" . ("ˡ"))
 
885
  ("^m" . ("ᵐ"))
 
886
  ("^n" . ("ⁿ"))
 
887
  ("^o" . ("ᵒ"))
 
888
  ("^p" . ("ᵖ"))
 
889
  ("^r" . ("ʳ"))
 
890
  ("^s" . ("ˢ"))
 
891
  ("^t" . ("ᵗ"))
 
892
  ("^u" . ("ᵘ"))
 
893
  ("^v" . ("ᵛ"))
 
894
  ("^w" . ("ʷ"))
 
895
  ("^x" . ("ˣ"))
 
896
  ("^y" . ("ʸ"))
 
897
  ("^z" . ("ᶻ"))
 
898
 
 
899
  ("^A" . ("ᴬ"))
 
900
  ("^B" . ("ᴮ"))
 
901
  ("^D" . ("ᴰ"))
 
902
  ("^E" . ("ᴱ"))
 
903
  ("^G" . ("ᴳ"))
 
904
  ("^H" . ("ᴴ"))
 
905
  ("^I" . ("ᴵ"))
 
906
  ("^J" . ("ᴶ"))
 
907
  ("^K" . ("ᴷ"))
 
908
  ("^L" . ("ᴸ"))
 
909
  ("^M" . ("ᴹ"))
 
910
  ("^N" . ("ᴺ"))
 
911
  ("^O" . ("ᴼ"))
 
912
  ("^P" . ("ᴾ"))
 
913
  ("^R" . ("ᴿ"))
 
914
  ("^T" . ("ᵀ"))
 
915
  ("^U" . ("ᵁ"))
 
916
  ("^V" . ("ⱽ"))
 
917
  ("^W" . ("ᵂ"))
 
918
 
590
919
  ;; Some ISO8859-1 characters.
591
920
 
592
921
  (" "         . (" "))