blob: 1d8ffb05c7a0d2539af384b5a8e20e5c16eb0d15 (
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
117
118
119
120
|
;; boogie-mode.el - GNU Emacs mode for Boogie 2
;; Adapted by Rustan Leino from Jean-Christophe FILLIATRE's GNU Emancs mode for Why
(defvar boogie-mode-hook nil)
(defvar boogie-mode-map nil
"Keymap for Boogie major mode")
(if boogie-mode-map nil
(setq boogie-mode-map (make-keymap))
(define-key boogie-mode-map "\C-c\C-c" 'boogie-run-boogie)
(define-key boogie-mode-map [(control return)] 'font-lock-fontify-buffer))
(setq auto-mode-alist
(append
'(("\\.bpl" . boogie-mode))
auto-mode-alist))
;; font-lock
(defun boogie-regexp-opt (l)
(concat "\\<" (concat (regexp-opt l t) "\\>")))
(defconst boogie-font-lock-keywords-1
(list
; comments have the form /* ... */
'("/\\*\\([^*]\\|\\*[^/]\\)*\\*/" . font-lock-comment-face)
; or // ...
'("//\\([^
]\\)*" . font-lock-comment-face)
`(,(boogie-regexp-opt '(
"type" "const" "function" "axiom" "var" "procedure" "implementation"
"returns" "where" "requires" "ensures" "modifies" "free" "unique"
"invariant" "extends" "complete"
)) . font-lock-builtin-face)
`(,(boogie-regexp-opt '(
"assert" "assume" "break" "call" "else" "havoc" "if" "goto" "return" "while"
"old" "forall" "exists" "cast"
"false" "true")) . font-lock-keyword-face)
`(,(boogie-regexp-opt '("bool" "int"
"bv0" "bv1" "bv2" "bv3" "bv4" "bv5" "bv6" "bv7" "bv8" "bv9"
"bv10" "bv11" "bv12" "bv13" "bv14" "bv15" "bv16" "bv17" "bv18" "bv19"
"bv20" "bv21" "bv22" "bv23" "bv24" "bv25" "bv26" "bv27" "bv28" "bv29"
"bv30" "bv31" "bv32" "bv33" "bv34" "bv35" "bv36" "bv37" "bv38" "bv39"
"bv40" "bv41" "bv42" "bv43" "bv44" "bv45" "bv46" "bv47" "bv48" "bv49"
"bv50" "bv51" "bv52" "bv53" "bv54" "bv55" "bv56" "bv57" "bv58" "bv59"
"bv60" "bv61" "bv62" "bv63" "bv64" ; and so on
)) . font-lock-type-face)
)
"Minimal highlighting for Boogie mode")
(defvar boogie-font-lock-keywords boogie-font-lock-keywords-1
"Default highlighting for Boogie mode")
;; syntax
(defvar boogie-mode-syntax-table nil
"Syntax table for boogie-mode")
(defun boogie-create-syntax-table ()
(if boogie-mode-syntax-table
()
(setq boogie-mode-syntax-table (make-syntax-table))
(set-syntax-table boogie-mode-syntax-table)
(modify-syntax-entry ?' "w" boogie-mode-syntax-table)
(modify-syntax-entry ?_ "w" boogie-mode-syntax-table)))
;; menu
(require 'easymenu)
(defun boogie-menu ()
(easy-menu-define
boogie-mode-menu (list boogie-mode-map)
"Boogie Mode Menu."
'("Boogie"
["Run Boogie" boogie-run-boogie t]
"---"
["Recolor buffer" font-lock-fontify-buffer t]
"---"
))
(easy-menu-add boogie-mode-menu))
;; commands
(defun boogie-command-line (file)
(concat "boogie -nologo -abbrevOutput " file))
(defun boogie-run-boogie ()
"run Boogie to check the Boogie program"
(interactive)
(let ((f (buffer-name)))
(compile (boogie-command-line f))))
;; setting the mode
(defun boogie-mode ()
"Major mode for editing Boogie programs.
\\{boogie-mode-map}"
(interactive)
(kill-all-local-variables)
(boogie-create-syntax-table)
; hilight
(make-local-variable 'font-lock-defaults)
(setq font-lock-defaults '(boogie-font-lock-keywords))
; indentation
; (make-local-variable 'indent-line-function)
; (setq indent-line-function 'boogie-indent-line)
; menu
; providing the mode
(setq major-mode 'boogie-mode)
(setq mode-name "Boogie")
(use-local-map boogie-mode-map)
(font-lock-mode 1)
(boogie-menu)
(run-hooks 'boogie-mode-hook))
(provide 'boogie-mode)
|
