-
Notifications
You must be signed in to change notification settings - Fork 3
/
boole-mode.el
111 lines (99 loc) · 4.43 KB
/
boole-mode.el
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
;; Add this to your .emacs file for improved syntax coloring
;; and pretty printing of operators.
(defun unicode-symbol (name)
"Translate a symbolic name for a Unicode character -- e.g., LEFT-ARROW
or GREATER-THAN into an actual Unicode character code. "
(decode-char 'ucs (case name
;; arrows
('left-arrow 8592)
('up-arrow 8593)
('right-arrow 8594)
('down-arrow 8595)
;; boxes
('double-vertical-bar #X2551)
;; relational operators
('equal #X2243)
('not-equal #X2260)
('identical #X2261)
('not-identical #X2262)
('less-than #X003c)
('greater-than #X003e)
('less-than-or-equal-to #X2264)
('greater-than-or-equal-to #X2265)
;; logical operators
('logical-and #X2227)
('logical-or #X2228)
('logical-neg #X00AC)
;; misc
('nil #X2205)
('horizontal-ellipsis #X2026)
('double-exclamation #X203C)
('prime #X2032)
('double-prime #X2033)
('for-all #X2200)
('there-exists #X2203)
('element-of #X2208)
;; mathematical operators
('square-root #X221A)
('squared #X00B2)
('cubed #X00B3)
('times #X00D7)
;; letters
('lambda #X03BB)
('pi #X03A0)
('sigma #X03A3)
('alpha #X03B1)
('beta #X03B2)
('gamma #X03B3)
('delta #X03B4))))
(defun substitute-pattern-with-unicode (pattern symbol)
"Add a font lock hook to replace the matched part of PATTERN with the
Unicode symbol SYMBOL looked up with UNICODE-SYMBOL."
(interactive)
(font-lock-add-keywords
nil `((,pattern (0 (progn (compose-region (match-beginning 1) (match-end 1)
,(unicode-symbol symbol))
nil))))))
(defun substitute-patterns-with-unicode (patterns)
"Call SUBSTITUTE-PATTERN-WITH-UNICODE repeatedly."
(mapcar #'(lambda (x)
(substitute-pattern-with-unicode (car x)
(cdr x)))
patterns))
(defun python-unicode ()
(interactive)
(substitute-patterns-with-unicode
(list (cons "\\(>>\\)" 'right-arrow)
(cons "\\(==\\)" 'equal)
(cons "\\(!=\\)" 'not-equal)
;; (cons "\\(*\\)" 'times)
(cons "\\<\\(Not\\)\\>" 'logical-neg)
(cons "\\(>=\\)" 'greater-than-or-equal-to)
(cons "\\(<=\\)" 'less-than-or-equal-to)
(cons "\\<\\(abst\\)\\>" 'lambda)
(cons "\\<\\(pi\\)\\>" 'pi)
(cons "\\<\\(sig\\)\\>" 'sigma)
(cons "\\<\\(forall\\)\\>" 'for-all)
(cons "\\<\\(exists\\)\\>" 'there-exists))))
(add-hook 'python-mode-hook 'python-unicode)
;; adds keywords for boole mode
(font-lock-add-keywords 'python-mode
'(
("\\<\\(abst\\|pi\\|sig\\|forall\\|exists\\|cast\\|implies\\|And\\|Or\\|Not\\|\\)\\>"
0 py-builtins-face)
("\\<\\(Type\\|Bool\\|Kind\\|Real\\|Int\\)\\>" 0 'font-lock-type-face)
("\\<[\\+-]?[0-9]+\\(.[0-9]+\\)?\\>" 0 'font-lock-constant-face)
("\\<\\(true\\|false\\)\\>" 0 'font-lock-constant-face)
("\\<\\(deftype\\|defconst\\|defexpr\\|defhyp\\|defthm\\|defsub\\|defclass\\|definstance\\|defenum\\|defvar\\)\\>" 0 'font-lock-function-name-face)
))
(defun boole-eval-statement ()
(interactive)
(save-excursion
;; (move-beginning-of-line nil)
;; (py-goto-block-up nil)
(py-mark-block)
(py-execute-region (region-beginning) (region-end))))
(add-hook 'python-mode-hook
'(lambda () (local-set-key (kbd "C-c l") 'boole-eval-statement)))
(add-hook 'python-mode-hook
'(lambda () (setq py-shell-switch-buffers-on-execute nil)))