From a54b7d394f92a9af32cff46e854eb4d37705439e Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Thu, 4 Oct 2012 15:38:05 -0700
Subject: Migrated a missing file from the old Boogie codeplex

---
 Util/Emacs/jennisys-mode.el | 113 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 113 insertions(+)
 create mode 100644 Util/Emacs/jennisys-mode.el

(limited to 'Util')

diff --git a/Util/Emacs/jennisys-mode.el b/Util/Emacs/jennisys-mode.el
new file mode 100644
index 00000000..d8f20a31
--- /dev/null
+++ b/Util/Emacs/jennisys-mode.el
@@ -0,0 +1,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)
-- 
cgit v1.2.3