blob: d8f20a318fb56a550e1094096b7f44a31a8b4dc6 (
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
|
;; jennisys-mode.el - GNU Emacs mode for Jennisys
;; Adapted by Rustan Leino from Jean-Christophe FILLIATRE's GNU Emancs mode for Why
(defvar jennisys-mode-hook nil)
(defvar jennisys-mode-map nil
"Keymap for Jennisys major mode")
(if jennisys-mode-map nil
(setq jennisys-mode-map (make-keymap))
(define-key jennisys-mode-map "\C-c\C-c" 'jennisys-run-boogie)
(define-key jennisys-mode-map [(control return)] 'font-lock-fontify-buffer))
(setq auto-mode-alist
(append
'(("\\.jen" . jennisys-mode))
auto-mode-alist))
;; font-lock
(defun jennisys-regexp-opt (l)
(concat "\\<" (concat (regexp-opt l t) "\\>")))
(defconst jennisys-font-lock-keywords-1
(list
; comments have the form /* ... */
'("/\\*\\([^*]\\|\\*[^/]\\)*\\*/" . font-lock-comment-face)
; or // ...
'("//\\([^
]\\)*" . font-lock-comment-face)
`(,(jennisys-regexp-opt '(
"interface" "datamodel" "code"
"var" "constructor" "method"
"frame" "invariant" "returns" "requires" "ensures"
)) . font-lock-builtin-face)
`(,(jennisys-regexp-opt '(
"if" "then" "else"
"forall" "exists"
"this" "in"
"false" "true" "null")) . font-lock-keyword-face)
`(,(jennisys-regexp-opt '("array" "bool" "int" "set" "seq")) . font-lock-type-face)
)
"Minimal highlighting for Jennisys mode")
(defvar jennisys-font-lock-keywords jennisys-font-lock-keywords-1
"Default highlighting for Jennisys mode")
;; syntax
(defvar jennisys-mode-syntax-table nil
"Syntax table for jennisys-mode")
(defun jennisys-create-syntax-table ()
(if jennisys-mode-syntax-table
()
(setq jennisys-mode-syntax-table (make-syntax-table))
(set-syntax-table jennisys-mode-syntax-table)
(modify-syntax-entry ?' "w" jennisys-mode-syntax-table)
(modify-syntax-entry ?_ "w" jennisys-mode-syntax-table)))
;; menu
(require 'easymenu)
(defun jennisys-menu ()
(easy-menu-define
jennisys-mode-menu (list jennisys-mode-map)
"Jennisys Mode Menu."
'("Jennisys"
["Run Boogie" jennisys-run-boogie t]
"---"
["Recolor buffer" font-lock-fontify-buffer t]
"---"
))
(easy-menu-add jennisys-mode-menu))
;; commands
(defun jennisys-command-line (file)
(concat "boogie " file))
(defun jennisys-run-boogie ()
"run Boogie to check the Jennisys program"
(interactive)
(let ((f (buffer-name)))
(compile (jennisys-command-line f))))
;; setting the mode
(defun jennisys-mode ()
"Major mode for editing Jennisys programs.
\\{jennisys-mode-map}"
(interactive)
(kill-all-local-variables)
(jennisys-create-syntax-table)
; hilight
(make-local-variable 'font-lock-defaults)
(setq font-lock-defaults '(jennisys-font-lock-keywords))
; indentation
; (make-local-variable 'indent-line-function)
; (setq indent-line-function 'jennisys-indent-line)
; menu
; providing the mode
(setq major-mode 'jennisys-mode)
(setq mode-name "Jennisys")
(use-local-map jennisys-mode-map)
(font-lock-mode 1)
(jennisys-menu)
(run-hooks 'jennisys-mode-hook))
(provide 'jennisys-mode)
|
