Replace the Emacs mode files by a pointer to the boogie-friends repo.

Does mercurial support submodules? That could be a good option too.

3 files changed, 2 insertions, 234 deletions

diff --git a/Util/Emacs/README b/Util/Emacs/README
new file mode 100644
index 00000000..9140f20a
--- /dev/null
+++ b/Util/Emacs/README
@@ -0,0 +1,2 @@
+Emacs support for dafny is provided by the boogie-friends package, available from MELPA.
+See https://github.com/boogie-org/boogie-friends for setup instructions and tips.
\ No newline at end of file
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
deleted file mode 100644
index fd1bf369..00000000
--- a/Util/Emacs/dafny-mode.el
+++ /dev/null
@@ -1,121 +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" "trait" "datatype" "codatatype" "newtype" "type" "iterator"

-        "function" "predicate" "copredicate" "inductive"

-        "var" "method" "constructor" "lemma" "colemma"

-        "ghost" "static" "protected" "abstract"

-	"module" "import" "default" "as" "opened"

-	"include"

-        "extends" "refines" "returns" "yields"

-	"requires" "ensures" "modifies" "reads" "free" "invariant" "decreases"

-        )) . font-lock-builtin-face)

-   `(,(dafny-regexp-opt '(

-        "assert" "assume" "break" "then" "else" "if" "label" "return" "yield"

-        "while" "print" "where"

-        "old" "forall" "exists" "new" "calc" "modify" "in" "this" "fresh"

-        "match" "case" "false" "true" "null")) . font-lock-keyword-face)

-   `(,(dafny-regexp-opt '(

-        "bool" "char" "int" "nat" "real"

-        "set" "iset" "multiset" "seq" "string" "map" "imap"

-	"object" "array" "array2" "array3")) . 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 "dafny " 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)