|
| 1 | +;;; k3-mode.el -- Emacs mode for the K Framework |
| 2 | + |
| 3 | +;; Updated from k-mode.el to support the new keywords in K3 |
| 4 | + |
| 5 | +;; Usage: add the below to your .emacs file: |
| 6 | +;; (setq load-path (cons "path/to/this/file" load-path)) |
| 7 | +;; (load-library "k3-mode") |
| 8 | +;; (add-to-list 'auto-mode-alist '("\\.k$" . k3-mode)) ;; to launch k3-mode for .k files |
| 9 | + |
| 10 | +;; Currently has syntax highlighting for: |
| 11 | +;; - keywords |
| 12 | +;; - declarations (e.g. ops, syntax, etc) |
| 13 | +;; - Quoted identifiers (e.g. for terminals in the syntax) |
| 14 | +;; Also has a menu and compilation through C-c C-c |
| 15 | + |
| 16 | + |
| 17 | +;; Author: Michael Ilseman |
| 18 | + |
| 19 | +(require 'comint) |
| 20 | + |
| 21 | +;;;; Options ;;;; |
| 22 | +(defvar k-dash-comments nil |
| 23 | + "Set to make \"--\" be used as a beginning of a line comment |
| 24 | + (emacs's syntax table is unable to differentiate 3 character long comment beginners)" |
| 25 | +) |
| 26 | +(defvar k-path "~/k-framework" |
| 27 | + "Path to the k-framework. Set if you wish to use kompile from emacs. Defaults to ~/k-framework. |
| 28 | + Currently doesn't do anything." |
| 29 | +) |
| 30 | + |
| 31 | +;;;; Syntax Highlighting ;;;; |
| 32 | +(setq k-keywords |
| 33 | + '("syntax" "priorities" "left" "right" "non-assoc" "module" "endmodule" "imports" "::=" "|" |
| 34 | + "sort" "op" "subsort" "rule" "context" "eq" "ceq" "load" "when" "require" "configuration" "context" "requires" "ensures") |
| 35 | + k-syntax-terminals-regex |
| 36 | + "`\\w+" |
| 37 | + k-declarations ;; Syntax highlight the name after a declaration |
| 38 | + "\\(syntax\\|sort\\|op\\) \\([a-zA-Z{}\\-]+\\)" |
| 39 | +) |
| 40 | + |
| 41 | +;; Set up the regexes |
| 42 | +(setq k-keywords-regex |
| 43 | + (regexp-opt k-keywords 'words) |
| 44 | +) |
| 45 | + |
| 46 | +;; Put them all together |
| 47 | +(setq k-font-lock-keywords |
| 48 | + `((,k-declarations 2 font-lock-builtin-face) |
| 49 | + (,k-keywords-regex . font-lock-keyword-face) |
| 50 | + (,k-syntax-terminals-regex . font-lock-constant-face) |
| 51 | + ) |
| 52 | +) |
| 53 | + |
| 54 | +;; Handle comments |
| 55 | +(defun set-comment-highlighting () |
| 56 | + "Set up comment highlighting" |
| 57 | + |
| 58 | + ;; comment style "// ..." and "/* ... */" |
| 59 | + (modify-syntax-entry ?\/ ". 124b" k3-mode-syntax-table) |
| 60 | + (modify-syntax-entry ?\n "> b" k3-mode-syntax-table) |
| 61 | + (modify-syntax-entry ?* ". 23" k3-mode-syntax-table) |
| 62 | + |
| 63 | + ;; comment style "-- ..." |
| 64 | + (if k-dash-comments (modify-syntax-entry ?- ". 1b2b" k3-mode-syntax-table)) |
| 65 | +) |
| 66 | + |
| 67 | + |
| 68 | +;;;; K Bindings and menu ;;;; |
| 69 | +(defvar k-prev-load-file nil |
| 70 | + "Record the last directory and file used in loading or compiling" |
| 71 | +) |
| 72 | +(defcustom k-source-modes '(k3-mode) |
| 73 | + "Determine if a buffer represents a k file" |
| 74 | +) |
| 75 | +;; (defun k3-mode-kompile (cmd) |
| 76 | +;; ;; (interactive (comint-get-source "Kompile k file: " k-prev-load-file k-source-modes nil)) |
| 77 | +;; ;; (comint-check-source file-name) ; check to see if buffer has been modified and not saved |
| 78 | +;; ;; (setq k-prev-load-file (cons (file-name-directory file-name) |
| 79 | +;; ;; (file-name-nondirectory file-name))) |
| 80 | +;; ;; ;; (comint-send-string (inferior-lisp-proc) |
| 81 | +;; ;; ;; (format inferior-lisp-load-command file-name)) |
| 82 | +;; ;; ;; (switch-to-lisp t)) |
| 83 | +;; ;; (message file-name) |
| 84 | +;; ;; (setq kompile-buffer (make-comint "Kompile" "zsh" nil)) |
| 85 | +;; ;; (comint-send-string kompile-buffer "cd" nil (file-name-directory file-name)) |
| 86 | +;; ;; (comint-send-string kompile-buffer "~/k-framework/tools/kompile.pl" nil (file-name-nondirectory file-name)) |
| 87 | +;; (interactive "scmd") |
| 88 | +;; (compile cmd) |
| 89 | +;; nil |
| 90 | +;; ) |
| 91 | +(defun k3-mode-about () |
| 92 | + (interactive) |
| 93 | + (message "k3-mode for the K Framework") |
| 94 | +) |
| 95 | + |
| 96 | +(defun setup-k3-mode-map () |
| 97 | + (setq k3-mode-map (make-sparse-keymap)) |
| 98 | + |
| 99 | + ;; Keyboard shortcuts |
| 100 | + (define-key k3-mode-map (kbd "C-c C-c") 'compile) |
| 101 | + |
| 102 | + ;; Define the menu |
| 103 | + (define-key k3-mode-map [menu-bar] (make-sparse-keymap)) |
| 104 | + |
| 105 | + (let ((menuMap (make-sparse-keymap "K Framework"))) |
| 106 | + (define-key k3-mode-map [menu-bar k] (cons "K Framework" menuMap)) |
| 107 | + (define-key menuMap [about] |
| 108 | + '("About k3-mode" . k3-mode-about)) |
| 109 | + ;; (define-key menuMap [customize] |
| 110 | + ;; '("Customize k3-mode" . k-customize)) |
| 111 | + (define-key menuMap [separator] |
| 112 | + '("--")) |
| 113 | + (define-key menuMap [kompile] |
| 114 | + '("kompile" . compile))) |
| 115 | +) |
| 116 | + |
| 117 | + |
| 118 | + |
| 119 | + |
| 120 | + |
| 121 | +;;;; K Mode ;;;; |
| 122 | + |
| 123 | +(define-derived-mode k3-mode fundamental-mode |
| 124 | + "k3 mode" |
| 125 | + "Major Mode for the K3 framwork" |
| 126 | + (setq font-lock-defaults '((k-font-lock-keywords))) |
| 127 | + |
| 128 | + ;; Comment entries |
| 129 | + (set-comment-highlighting) |
| 130 | + |
| 131 | + ;; Set comment start characters |
| 132 | + (setq comment-start "//") |
| 133 | + |
| 134 | + ;; Shortcuts and menu |
| 135 | + (setup-k3-mode-map) |
| 136 | + (use-local-map k3-mode-map) |
| 137 | + |
| 138 | + ;; Clear up memory |
| 139 | + ;;(setq k-keywords nil k-keywords-regex nil) |
| 140 | +) |
| 141 | + |
| 142 | +(provide 'k3-mode) |
0 commit comments