From f09b14f4b3f3915343b1279da286351ab5348eac Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sun, 23 Aug 2015 04:23:51 -0700 Subject: Replace the Emacs mode files by a pointer to the boogie-friends repo. Does mercurial support submodules? That could be a good option too. --- Util/Emacs/README | 2 + Util/Emacs/dafny-mode.el | 121 -------------------------------------------- Util/Emacs/jennisys-mode.el | 113 ----------------------------------------- 3 files changed, 2 insertions(+), 234 deletions(-) create mode 100644 Util/Emacs/README delete mode 100644 Util/Emacs/dafny-mode.el delete mode 100644 Util/Emacs/jennisys-mode.el (limited to 'Util') 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) -- cgit v1.2.3