summaryrefslogtreecommitdiff
path: root/Util
diff options
context:
space:
mode:
Diffstat (limited to 'Util')
-rw-r--r--Util/Emacs/README2
-rw-r--r--Util/Emacs/dafny-mode.el121
-rw-r--r--Util/Emacs/jennisys-mode.el113
-rw-r--r--Util/latex/dafny.sty2
-rw-r--r--Util/vim/dafny.vim2
5 files changed, 4 insertions, 236 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 2846c824..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" "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 "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)
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index 44a55f70..76d2278a 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -6,7 +6,7 @@
\lstdefinelanguage{dafny}{
morekeywords={class,datatype,codatatype,newtype,type,iterator,trait,extends,
- bool,char,nat,int,real,object,set,multiset,seq,string,map,imap,array,array2,array3,
+ bool,char,nat,int,real,object,set,iset,multiset,seq,string,map,imap,array,array2,array3,
function,predicate,copredicate,inductive,
ghost,var,static,protected,refines,
method,lemma,constructor,colemma,
diff --git a/Util/vim/dafny.vim b/Util/vim/dafny.vim
index 65d7165f..d81872aa 100644
--- a/Util/vim/dafny.vim
+++ b/Util/vim/dafny.vim
@@ -13,7 +13,7 @@ syntax keyword dafnyConditional if then else match case
syntax keyword dafnyRepeat while
syntax keyword dafnyStatement assume assert return yield new print break label where calc modify
syntax keyword dafnyKeyword var ghost returns yields null static protected this refines include
-syntax keyword dafnyType bool char nat int real set multiset seq string map imap object array array2 array3
+syntax keyword dafnyType bool char nat int real set iset multiset seq string map imap object array array2 array3
syntax keyword dafnyLogic requires ensures modifies reads decreases invariant
syntax keyword dafnyOperator forall exists old fresh
syntax keyword dafnyBoolean true false
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 20:57:07 +0000