diff options
| author |  mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
| commit | ce1c2de044c91624370411e23acab13b0381949b (patch) | |
| tree | 592539996fe08050ead5ee210c973801611dde40 /Util/Emacs/boogie-mode.el | |
Initial set of files.
Diffstat (limited to 'Util/Emacs/boogie-mode.el')
| -rw-r--r-- | Util/Emacs/boogie-mode.el | 120 |
1 files changed, 120 insertions, 0 deletions
diff --git a/Util/Emacs/boogie-mode.el b/Util/Emacs/boogie-mode.el new file mode 100644 index 00000000..1d8ffb05 --- /dev/null +++ b/Util/Emacs/boogie-mode.el @@ -0,0 +1,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)
|