diff options
Diffstat (limited to 'Util/Emacs')
| -rw-r--r-- | Util/Emacs/boogie-mode.el | 120 | ||||
| -rw-r--r-- | Util/Emacs/chalice-mode.el | 115 | ||||
| -rw-r--r-- | Util/Emacs/dafny-mode.el | 112 |
3 files changed, 347 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)
diff --git a/Util/Emacs/chalice-mode.el b/Util/Emacs/chalice-mode.el new file mode 100644 index 00000000..91c69120 --- /dev/null +++ b/Util/Emacs/chalice-mode.el @@ -0,0 +1,115 @@ +;; 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"
+ )) . font-lock-builtin-face)
+ `(,(chalice-regexp-opt '(
+ "above" "acc" "acquire" "and" "assert" "assigned" "assume"
+ "below" "between" "call"
+ "downgrade" "else" "eval" "exists" "fold" "forall" "fork" "free" "havoc" "holds"
+ "if" "in" "install" "ite" "join" "lock" "lockbottom" "maxlock" "module" "new" "nil"
+ "old" "rd" "release" "result" "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)
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el new file mode 100644 index 00000000..508ffbaf --- /dev/null +++ b/Util/Emacs/dafny-mode.el @@ -0,0 +1,112 @@ +;; dafny-mode.el - GNU Emacs mode for Dafny
+;; Adapted by Rustan Leino from Jean-Christophe FILLIATRE's GNU Emancs mode for Why
+
+(defvar dafny-mode-hook nil)
+
+(defvar dafny-mode-map nil
+ "Keymap for Dafny major mode")
+
+(if dafny-mode-map nil
+ (setq dafny-mode-map (make-keymap))
+ (define-key dafny-mode-map "\C-c\C-c" 'dafny-run-boogie)
+ (define-key dafny-mode-map [(control return)] 'font-lock-fontify-buffer))
+
+(setq auto-mode-alist
+ (append
+ '(("\\.dfy" . dafny-mode))
+ auto-mode-alist))
+
+;; font-lock
+
+(defun dafny-regexp-opt (l)
+ (concat "\\<" (concat (regexp-opt l t) "\\>")))
+
+(defconst dafny-font-lock-keywords-1
+ (list
+ ; comments have the form /* ... */
+ '("/\\*\\([^*]\\|\\*[^/]\\)*\\*/" . font-lock-comment-face)
+ ; or // ...
+ '("//\\([^
+]\\)*" . font-lock-comment-face)
+
+ `(,(dafny-regexp-opt '(
+ "class" "function" "frame" "var" "method"
+ "returns" "requires" "ensures" "modifies" "reads" "free"
+ "invariant" "decreases"
+ )) . font-lock-builtin-face)
+ `(,(dafny-regexp-opt '(
+ "assert" "assume" "break" "call" "else" "havoc" "if" "label" "return" "while"
+ "old" "forall" "exists" "new" "foreach" "in" "this" "fresh" "use"
+ "false" "true" "null")) . font-lock-keyword-face)
+ `(,(dafny-regexp-opt '("bool" "int" "object" "set" "seq")) . font-lock-type-face)
+ )
+ "Minimal highlighting for Dafny mode")
+
+(defvar dafny-font-lock-keywords dafny-font-lock-keywords-1
+ "Default highlighting for Dafny mode")
+
+;; syntax
+
+(defvar dafny-mode-syntax-table nil
+ "Syntax table for dafny-mode")
+
+(defun dafny-create-syntax-table ()
+ (if dafny-mode-syntax-table
+ ()
+ (setq dafny-mode-syntax-table (make-syntax-table))
+ (set-syntax-table dafny-mode-syntax-table)
+ (modify-syntax-entry ?' "w" dafny-mode-syntax-table)
+ (modify-syntax-entry ?_ "w" dafny-mode-syntax-table)))
+
+;; menu
+
+(require 'easymenu)
+
+(defun dafny-menu ()
+ (easy-menu-define
+ dafny-mode-menu (list dafny-mode-map)
+ "Dafny Mode Menu."
+ '("Dafny"
+ ["Run Boogie" dafny-run-boogie t]
+ "---"
+ ["Recolor buffer" font-lock-fontify-buffer t]
+ "---"
+ ))
+ (easy-menu-add dafny-mode-menu))
+
+;; commands
+
+(defun dafny-command-line (file)
+ (concat "boogie " file))
+
+(defun dafny-run-boogie ()
+ "run Boogie to check the Dafny program"
+ (interactive)
+ (let ((f (buffer-name)))
+ (compile (dafny-command-line f))))
+
+;; setting the mode
+
+(defun dafny-mode ()
+ "Major mode for editing Dafny programs.
+
+\\{dafny-mode-map}"
+ (interactive)
+ (kill-all-local-variables)
+ (dafny-create-syntax-table)
+ ; hilight
+ (make-local-variable 'font-lock-defaults)
+ (setq font-lock-defaults '(dafny-font-lock-keywords))
+ ; indentation
+ ; (make-local-variable 'indent-line-function)
+ ; (setq indent-line-function 'dafny-indent-line)
+ ; menu
+ ; providing the mode
+ (setq major-mode 'dafny-mode)
+ (setq mode-name "Dafny")
+ (use-local-map dafny-mode-map)
+ (font-lock-mode 1)
+ (dafny-menu)
+ (run-hooks 'dafny-mode-hook))
+
+(provide 'dafny-mode)
|