blob: 34a95a87e16adb54bccc7929592f0d17e6aafb48 (
plain)
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
112
113
114
115
116
|
;; chalice-mode.el - GNU Emacs mode for Chalice
;; Adapted by Rustan Leino from Jean-Christophe FILLIATRE's GNU Emancs mode for Why
(defvar chalice-mode-hook nil)
(defvar chalice-mode-map nil
"Keymap for Chalice major mode")
(if chalice-mode-map nil
(setq chalice-mode-map (make-keymap))
(define-key chalice-mode-map "\C-c\C-c" 'chalice-run-boogie)
(define-key chalice-mode-map [(control return)] 'font-lock-fontify-buffer))
(setq auto-mode-alist
(append
'(("\\.chalice" . chalice-mode))
auto-mode-alist))
;; font-lock
(defun chalice-regexp-opt (l)
(concat "\\<" (concat (regexp-opt l t) "\\>")))
(defconst chalice-font-lock-keywords-1
(list
; comments have the form /* ... */
'("/\\*\\([^*]\\|\\*[^/]\\)*\\*/" . font-lock-comment-face)
; or // ...
'("//\\([^
]\\)*" . font-lock-comment-face)
`(,(chalice-regexp-opt '(
"class" "ghost" "var" "const" "external" "function" "method"
"predicate" "returns" "requires" "ensures" "lockchange"
"invariant" "channel" "condition" "where"
)) . font-lock-builtin-face)
`(,(chalice-regexp-opt '(
"above" "acc" "acquire" "and" "assert" "assigned" "assume"
"below" "between" "call" "credit"
"downgrade" "else" "eval" "exists" "fold" "forall" "fork" "free" "havoc" "holds"
"if" "in" "ite" "join" "lock" "lockbottom" "waitlevel" "module" "new" "nil"
"old" "rd" "receive" "release" "reorder" "result" "send" "share"
"this" "unfold" "unfolding" "unshare" "while"
"false" "true" "null")) . font-lock-keyword-face)
`(,(chalice-regexp-opt '("bool" "int" "seq" "token")) . font-lock-type-face)
)
"Minimal highlighting for Chalice mode")
(defvar chalice-font-lock-keywords chalice-font-lock-keywords-1
"Default highlighting for Chalice mode")
;; syntax
(defvar chalice-mode-syntax-table nil
"Syntax table for chalice-mode")
(defun chalice-create-syntax-table ()
(if chalice-mode-syntax-table
()
(setq chalice-mode-syntax-table (make-syntax-table))
(set-syntax-table chalice-mode-syntax-table)
(modify-syntax-entry ?' "w" chalice-mode-syntax-table)
(modify-syntax-entry ?_ "w" chalice-mode-syntax-table)))
;; menu
(require 'easymenu)
(defun chalice-menu ()
(easy-menu-define
chalice-mode-menu (list chalice-mode-map)
"Chalice Mode Menu."
'("Chalice"
["Run Boogie" chalice-run-boogie t]
"---"
["Recolor buffer" font-lock-fontify-buffer t]
"---"
))
(easy-menu-add chalice-mode-menu))
;; commands
(defun chalice-command-line (file)
(concat "boogie " file))
(defun chalice-run-boogie ()
"run Boogie to check the Chalice program"
(interactive)
(let ((f (buffer-name)))
(compile (chalice-command-line f))))
;; setting the mode
(defun chalice-mode ()
"Major mode for editing Chalice programs.
\\{chalice-mode-map}"
(interactive)
(kill-all-local-variables)
(chalice-create-syntax-table)
; hilight
(make-local-variable 'font-lock-defaults)
(setq font-lock-defaults '(chalice-font-lock-keywords))
; indentation
; (make-local-variable 'indent-line-function)
; (setq indent-line-function 'chalice-indent-line)
; menu
; providing the mode
(setq major-mode 'chalice-mode)
(setq mode-name "Chalice")
(use-local-map chalice-mode-map)
(font-lock-mode 1)
(chalice-menu)
(run-hooks 'chalice-mode-hook))
(provide 'chalice-mode)
|
