3 files changed, 0 insertions, 347 deletions
diff --git a/Util/Emacs/chalice-mode.el b/Util/Emacs/chalice-mode.el
deleted file mode 100644
index c8cef685..00000000
--- a/Util/Emacs/chalice-mode.el
+++ /dev/null
@@ -1,118 +0,0 @@
-;; 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" "channel" "condition" "where"
-        "refines" "transforms"
-        )) . font-lock-builtin-face)
-   `(,(chalice-regexp-opt '(
-        "above" "acc" "acquire" "and" "assert" "assigned" "assume"
-        "below" "between" "call" "credit"
-        "downgrade" "else" "eval" "exists" "fold" "forall" "fork" "free" "havoc" "holds"
-        "spec" "replaces" "by"
-        "if" "in" "ite" "join" "lock" "lockbottom" "waitlevel" "module" "new" "nil"
-        "old" "rd" "receive" "release" "reorder" "result" "send" "share"
-        "this" "unfold" "unfolding" "unshare" "while"
-        "false" "true" "null")) . font-lock-keyword-face)
-   `(,(chalice-regexp-opt '("bool" "int" "string" "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
deleted file mode 100644
index 1ba6186b..00000000
--- a/Util/Emacs/dafny-mode.el
+++ /dev/null
@@ -1,116 +0,0 @@
-;; 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-verifier)
-  (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" "datatype" "codatatype" "type" "function" "predicate" "copredicate"
-        "iterator"
-        "ghost" "var" "method" "constructor"
-        "module" "import" "default" "as" "opened" "static" "refines"
-        "returns" "yields" "requires" "ensures" "modifies" "reads" "free"
-        "invariant" "decreases"
-        )) . font-lock-builtin-face)
-   `(,(dafny-regexp-opt '(
-        "assert" "assume" "break" "choose" "then" "else" "if" "label" "return" "yield"
-        "while" "print" "where"
-        "old" "forall" "exists" "new" "parallel" "calc" "in" "this" "fresh"
-        "match" "case" "false" "true" "null")) . font-lock-keyword-face)
-   `(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "multiset" "map" "nat" "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 Dafny" dafny-run-verifier 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-verifier ()
-  "run Dafny verifier"
-  (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)
diff --git a/Util/Emacs/jennisys-mode.el b/Util/Emacs/jennisys-mode.el
deleted file mode 100644
index d8f20a31..00000000
--- a/Util/Emacs/jennisys-mode.el
+++ /dev/null
@@ -1,113 +0,0 @@
-;; 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)