1;;;; /*! 2;;;; * \file cvc-mode.el 3;;;; * \brief Emacs mode for CVC programs in presentation language 4;;;; * 5;;;; * Author: Sergey Berezin 6;;;; * 7;;;; * Created: Mon Aug 11 12:29:32 2003 8;;;; * 9;;;; * <hr> 10;;;; * 11;;;; * License to use, copy, modify, sell and/or distribute this software 12;;;; * and its documentation for any purpose is hereby granted without 13;;;; * royalty, subject to the terms and conditions defined in the \ref 14;;;; * LICENSE file provided with this distribution. 15;;;; * 16;;;; * <hr> 17;;;; * 18;;;; */ 19 20;;;; To use this library, place the following lines into your ~/.emacs file: 21;;;; 22;;;; ;;; CVC mode 23;;;; (autoload 'cvc-mode "cvc-mode" "CVC specifications editing mode." t) 24;;;; (setq auto-mode-alist 25;;;; (append (list '("\\.cvc$" . cvc-mode)) auto-mode-alist)) 26;;;; 27;;;; Of course, the file cvc-mode.el must be in one of the directories in your 28;;;; `load-path'. C-h v load-path to see the list, or `cons' your own path: 29;;;; (setq load-path (cons "/the/full/path/to-your/dir" load-path)) 30;;;; 31;;;; To turn the font-lock on by default, put in .emacs 32;;;; (global-font-lock-mode t) ;; if you use gnu-emacs, or 33;;;; (setq-default font-lock-auto-fontify t) ;; if you use xemacs. 34;;;; 35;;;; In GNU emacs faces `font-lock-preprocessor-face' and 36;;;; `font-lock-variable-name-face' may not be predefined. 37;;;; In this case they are defined automatically when smv-mode.el 38;;;; is loaded the first time. You can also define them yourself in .emacs: 39;;;; 40;;;; ;;; Make faces that are not in gnu-emacs font-lock by default 41;;;; (defvar font-lock-preprocessor-face 'font-lock-preprocessor-face) 42;;;; (defvar font-lock-variable-name-face 'font-lock-variable-name-face) 43;;;; (make-face 'font-lock-preprocessor-face) 44;;;; (make-face 'font-lock-variable-name-face) 45 46(require 'font-lock) 47(require 'compile) 48 49(defvar cvc-font-lock-mode-on t 50 "If not nil, turn the fontification on.") 51 52(defvar cvc-running-xemacs (string-match "XEmacs\\|Lucid" emacs-version)) 53 54;;;; Syntax definitions 55 56(defvar cvc-mode-syntax-table nil "Syntax table used while in CVC mode.") 57 58(if cvc-mode-syntax-table () 59 (let ((st (syntax-table))) 60 (unwind-protect 61 (progn 62 (setq cvc-mode-syntax-table (make-syntax-table)) 63 (set-syntax-table cvc-mode-syntax-table) 64 (modify-syntax-entry ?_ "w") 65 (modify-syntax-entry ?- "w") 66 (modify-syntax-entry ?\? "w") 67 (modify-syntax-entry ?: "." ) 68 (modify-syntax-entry ?% "<") 69 (modify-syntax-entry ?\f ">") 70 (modify-syntax-entry ?\n ">")) 71 (set-syntax-table st)))) 72 73;;;; Fontification stuff 74 75(defun cvc-keyword-match (keyword) 76; "Convert a string into a regexp matching any capitalization of that string." 77 "Convert a string into a regexp matching that string as a separate word." 78; (let ((regexp "") 79; (index 0) 80; (len (length keyword))) 81; (while (< index len) 82; (let ((c (aref keyword index))) 83; (setq regexp 84; (concat regexp (format "[%c%c]" (downcase c) (upcase c)))) 85; (setq index (+ index 1)))) 86 (format "\\b%s\\b" keyword)) 87;) 88 89(defvar cvc-font-lock-separator-face 'cvc-font-lock-separator-face) 90(defvar font-lock-preprocessor-face 'font-lock-preprocessor-face) 91(defvar font-lock-variable-name-face 'font-lock-variable-name-face) 92 93(if (facep 'font-lock-preprocessor-face) () 94 (progn 95 (make-face 'font-lock-preprocessor-face) 96 (set-face-foreground 'font-lock-preprocessor-face "green4"))) 97 98(if (facep 'font-lock-variable-name-face) () 99 (progn 100 (make-face 'font-lock-variable-name-face) 101 (set-face-foreground 'font-lock-variable-name-face "deeppink"))) 102 103(if (facep 'cvc-font-lock-separator-face) () 104 (progn 105 (make-face 'cvc-font-lock-separator-face) 106 (set-face-foreground 'cvc-font-lock-separator-face "indianred"))) 107 108(defvar cvc-mode-hook nil 109 "Functions to run when loading an CVC file.") 110 111(defconst cvc-keywords 112 '("ASSERT" "QUERY" "TRACE" "UNTRACE" "OPTION" "HELP" "TRANSFORM" 113 "PRINT" "ECHO" "INCLUDE" "DUMP_ASSUMPTIONS" "DUMP_PROOF" "DUMP_SIG" 114 "WHERE" "COUNTEREXAMPLE" "PUSH" "POP" "POP_SCOPE" "POPTO" "RESET" 115 "CONTEXT" 116 "TYPE" "DATATYPE" "SUBTYPE" 117 "REAL" "INT" "BOOLEAN" "ARRAY" "OF" 118 "TRUE" "FALSE" "FLOOR" 119 "IF" "THEN" "ELSIF" "ELSE" "ENDIF" "LET" "IN" "END" "LAMBDA" "WITH" 120 "FORALL" "EXISTS" 121 "AND" "OR" "XOR" "NOT" ) 122 "The list of CVC keywords.") 123 124(defconst cvc-declaration-keywords 125 '("ASSERT" "QUERY" "TRACE" "UNTRACE" "OPTION" "HELP" "TRANSFORM" 126 "PRINT" "ECHO" "INCLUDE" "DUMP_ASSUMPTIONS" "DUMP_PROOF" "DUMP_SIG" 127 "WHERE" "COUNTEREXAMPLE" "PUSH" "POP" "POP_SCOPE" "POPTO" "RESET" 128 "CONTEXT") 129 "The list of keywords that open a declaration. Used for indentation.") 130 131(defconst cvc-declaration-regexp 132 (mapconcat 'cvc-keyword-match cvc-declaration-keywords "\\|")) 133 134(defconst cvc-opening-keywords 135 '("case" "for" "next" "init" "(") 136 "The list of keywords that open a subexpression. Used for indentation.") 137 138(defconst cvc-opening-keywords-regexp 139 (mapconcat 'cvc-keyword-match cvc-opening-keywords "\\|")) 140 141(defconst cvc-closing-keywords 142 '("esac" ")") 143 "The list of keywords that close a subexpression. Used for indentation.") 144 145(defconst cvc-closing-keywords-regexp 146 (mapconcat 'cvc-keyword-match cvc-closing-keywords "\\|")) 147 148(defconst cvc-opening-paren-regexp 149 (concat cvc-opening-keywords-regexp "\\|\\s(")) 150 151(defconst cvc-closing-paren-regexp 152 (concat cvc-closing-keywords-regexp "\\|\\s)")) 153 154(defconst cvc-infix-operators 155 '("<->" "<-" "->" ":=" "<=w\\>" ">=w\\>" "<w\\>" ">w\\>" "=w\\>" 156 "+w\\>" "-w\\>" "*w\\>" "<=" ">=" "!=" "=" "\\[" "\\]" 157 "\\b-\\b" "+" "|" "&" "<" ">") 158 "The list of regexps that match CVC infix operators. The distinction 159is made primarily for indentation purposes.") 160 161(defconst cvc-infix-operators-regexp 162 (mapconcat 'identity cvc-infix-operators "\\|")) 163 164(defconst cvc-other-operators 165 '("!" "(#" "#)") 166 "Non-infix CVC operators that are not listed in `cvc-infix-operators'.") 167 168(defconst cvc-other-operators-regexp 169 (mapconcat 'identity cvc-other-operators "\\|")) 170 171(defconst cvc-operators (append cvc-infix-operators cvc-other-operators) 172 "The list of regexps that match CVC operators. It is set to the 173concatenation of `cvc-infix-operators' and `cvc-other-operators'.") 174 175(defconst cvc-separator-regexp "[,.;():]" 176 "A regexp that matches any separator in CVC mode.") 177 178(defconst cvc-font-lock-keywords-1 179 (purecopy 180 (list 181 (list (concat (cvc-keyword-match "MODULE") " *\\([-_?A-Za-z0-9]+\\)") 182 1 'font-lock-preprocessor-face) 183 (list (concat "\\(" (cvc-keyword-match "init") "\\|" 184 (cvc-keyword-match "next") 185 "\\)(\\s-*\\([][_?.A-Za-z0-9-]+\\)\\s-*)\\s-*:=") 186 2 'font-lock-variable-name-face) 187 ;;; For DEFINE and invar assignments 188 (list "\\([][_?.A-Za-z0-9-]+\\)\\s-*:=" 189 1 'font-lock-variable-name-face) 190 (list "\\<\\([Aa]\\|[Ee]\\)\\[" 1 'font-lock-keyword-face) 191 (list (concat "\\(" 192 (mapconcat 'identity cvc-operators "\\|") 193 "\\)") 194 1 'font-lock-function-name-face 'prepend) 195 (mapconcat 'cvc-keyword-match cvc-keywords "\\|") 196;; Fix the `%' comments 197 (list "\\(%.*$\\)" 1 'font-lock-comment-face t) )) 198 "Additional expressions to highlight in CVC mode.") 199 200(defconst cvc-font-lock-keywords-2 201 (purecopy 202 (append cvc-font-lock-keywords-1 203 (list 204 (list "\\([{}]\\)" 1 'font-lock-type-face) 205 (list (concat "\\(" cvc-separator-regexp "\\)") 206 1 'cvc-font-lock-separator-face 'prepend)))) 207 "Additional expressions to highlight in CVC mode.") 208 209(defconst cvc-font-lock-keywords 210 (if font-lock-maximum-decoration 211 cvc-font-lock-keywords-2 212 cvc-font-lock-keywords-1)) 213 214(defun cvc-minimal-decoration () 215 (interactive) 216 (setq font-lock-keywords cvc-font-lock-keywords-1)) 217 218(defun cvc-maximal-decoration () 219 (interactive) 220 (setq font-lock-keywords cvc-font-lock-keywords-2)) 221 222;;;; Running CVC 223 224(defvar cvc-command "cvc3" 225 "The command name to run CVC. The default is usually \"cvc3\"") 226 227(defvar cvc-sat-option nil 228 "Search Engine choice in CVC. Valid values are nil, 229\"default\", \"simple\", and \"fast\", or any other values reported by 230cvc3 -h.") 231 232(defvar cvc-trace-flags nil 233 "List of trace flags given on the command line as +trace options") 234 235(defvar cvc-verbose-level nil 236"The verbose mode of CVC. Valid values are nil and \"quiet\". This 237value is passed to the CVC process as +/-quiet opton.") 238 239(defvar cvc-command-line-args nil 240 "Miscellaneous CVC command line args. 241Must be a single string or nil.") 242 243(defvar cvc-compile-buffer nil 244 "The buffer associated with inferior CVC process. 245This variable is updated automatically each time CVC process takes off.") 246 247(defvar cvc-options-changed nil) 248 249(defvar cvc-current-buffer nil 250 "The current CVC editing buffer. 251This variable is buffer-local.") 252(make-local-variable 'cvc-current-buffer) 253 254(defun cvc-args (file &optional args) 255 "Compiles the string of CVC command line args from various variables." 256 (mapconcat 'identity 257 (append 258 (if cvc-sat-option (list "-sat" cvc-sat-option) nil) 259 (if (eq cvc-verbose-level "quiet") (list "+quiet") nil) 260 (mapcar '(lambda (str) (format "+trace \"%s\"" str)) cvc-trace-flags) 261 (if cvc-command-line-args (list cvc-command-line-args)) 262 (if args (list args) nil) 263 (list "<" file)) 264 " ")) 265 266(defun cvc-run () 267 "Runs CVC on the current buffer." 268 (interactive) 269 (let ((buffer (current-buffer))) 270 (if (buffer-file-name) 271 (progn 272 (if (buffer-modified-p) (cvc-save-buffer)) 273 (setq cvc-compile-buffer 274 (compile-internal 275 (concat "time " cvc-command " " (cvc-args (buffer-file-name))) 276 "No more errors" 277 "CVC")) 278 (set-buffer cvc-compile-buffer) ;;; Doesn't work??? 279 (end-of-buffer) 280 (set-buffer buffer) 281 ) 282 (error "Buffer does not seem to be associated with any file"))) ) 283 284 285(defun cvc-save-options () 286 "Saves current options in *.opt file." 287 (interactive) 288 (let* ((buffer (current-buffer)) 289 (opt-file-name 290 (let ((match (string-match "\\.cvc$" 291 (buffer-file-name)))) 292 (if match 293 (concat (substring (buffer-file-name) 294 0 match) 295 ".opt") 296 (concat (buffer-file-name) ".opt")))) 297 (opt-buffer-name 298 (let ((match (string-match "\\.cvc$" 299 (buffer-name)))) 300 (if match 301 (concat (substring (buffer-name) 302 0 match) 303 ".opt") 304 (concat (buffer-name) ".opt")))) 305 (opt-buffer-exists (get-buffer opt-buffer-name)) 306 (opt-buffer (get-buffer-create opt-buffer-name)) 307 (save-options-from-buffer 308 (and opt-buffer-exists 309 (buffer-modified-p opt-buffer) 310 (y-or-n-p (format "buffer %s is modified. Save options from that buffer?" 311 (buffer-name opt-buffer))))) 312 (options (format ";;;; This file is generated automatically.\n(setq cvc-sat-option %S)\n(setq cvc-verbose-level %S)\n(setq cvc-trace-flags '%S)\n(setq cvc-command-line-args %S)\n" 313 cvc-sat-option 314 cvc-verbose-level 315 cvc-trace-flags 316 cvc-command-line-args))) 317 (set-buffer opt-buffer) 318 (if save-options-from-buffer (cvc-save-and-load-options) 319 (progn 320 (erase-buffer) 321 (insert options) 322 (write-file opt-file-name) 323 (kill-buffer opt-buffer))) 324 (set-buffer buffer) 325 (setq cvc-options-changed nil) 326 (message "Options are saved."))) 327 328(defun cvc-save-and-load-options () 329 "Saves the current buffer and updates CVC options in the associated 330buffer. This buffer is either the value of `cvc-current-buffer', or 331it tries to make a few reasonable guesses. If no CVC buffer is found, 332only saves the current buffer. 333 334Normally is called from the *.opt file while editing options for CVC 335specification." 336 (interactive) 337 (let* ((buffer (current-buffer)) 338 (buffer-file (buffer-file-name)) 339 (cvc-buffer-name 340 (let* ((match (string-match "\\.[^.]*$" (buffer-name)))) 341 (if match 342 (concat (substring (buffer-name) 0 match) ".cvc") 343 (concat (buffer-name) ".cvc")))) 344 (cvc-buffer (get-buffer cvc-buffer-name)) 345 (cvc-buffer 346 (cond (cvc-buffer cvc-buffer) 347 ((and (boundp 'cvc-current-buffer) 348 (buffer-live-p cvc-current-buffer)) 349 cvc-current-buffer) 350 (t nil)))) 351 (save-buffer) 352 (if cvc-buffer 353 (let ((cvc-window (get-buffer-window cvc-buffer)) 354 (window (get-buffer-window buffer))) 355 (set-buffer cvc-buffer) 356 (load buffer-file) 357 (setq cvc-current-buffer cvc-buffer) 358 (if cvc-window 359 (select-window cvc-window) 360 (switch-to-buffer cvc-buffer)) 361 (if window 362 (delete-window window)) 363 (setq cvc-options-changed nil)))) ) 364 365(defun cvc-save-and-return () 366 "Saves the current buffer and returns back to the associated CVC 367buffer. The CVC buffer is either the value of `cvc-current-buffer', or 368it tries to make a few reasonable guesses. If no CVC buffer is found, 369only saves the current buffer. 370 371Normally is called from the *.ord buffer while editing variable ordering 372for CVC specification. Bound to \\[cvc-save-and-return]" 373 (interactive) 374 (let* ((buffer (current-buffer)) 375 (cvc-buffer-name 376 (let* ((match (string-match "\\.[^.]*$" (buffer-name)))) 377 (if match 378 (concat (substring (buffer-name) 0 match) ".cvc") 379 (concat (buffer-name) ".cvc")))) 380 (cvc-buffer (get-buffer cvc-buffer-name)) 381 (cvc-buffer 382 (cond (cvc-buffer cvc-buffer) 383 ((and (boundp 'cvc-current-buffer) 384 (buffer-live-p cvc-current-buffer)) 385 cvc-current-buffer) 386 (t nil)))) 387 (save-buffer) 388 (if cvc-buffer 389 (let ((cvc-window (get-buffer-window cvc-buffer))) 390 (setq cvc-current-buffer cvc-buffer) 391 (if cvc-window 392 (select-window cvc-window) 393 (switch-to-buffer cvc-buffer)) 394 (if (get-buffer-window buffer) 395 (delete-window (get-buffer-window buffer)))))) ) 396 397(defun cvc-edit-options () 398 "Loads current options in a new buffer and lets the user edit it. 399Run \\[eval-buffer] when done." 400 (interactive) 401 (let* ((buffer (current-buffer)) 402 (opt-buffer-name 403 (let ((match (string-match "\\.cvc$" 404 (buffer-name)))) 405 (if match 406 (concat (substring (buffer-name) 407 0 match) 408 ".opt") 409 (concat (buffer-name) ".opt")))) 410 (opt-buffer (get-buffer-create opt-buffer-name)) 411 (options (format ";;;; This file is generated automatically.\n(setq cvc-sat-option %S)\n(setq cvc-verbose-level %S)\n(setq cvc-trace-flags '%S)\n(setq cvc-command-line-args %S)\n" 412 cvc-sat-option 413 cvc-verbose-level 414 cvc-trace-flags 415 cvc-command-line-args))) 416 (setq cvc-options-changed t) 417 (switch-to-buffer-other-window opt-buffer) 418 (set-visited-file-name opt-buffer-name) 419 (erase-buffer) 420 (insert options) 421 (make-local-variable 'cvc-currect-buffer) 422 (setq cvc-current-buffer buffer) 423 (cvc-options-edit-mode))) 424 425(defun cvc-interrupt () 426 "Kills current CVC process." 427 (interactive) 428 (quit-process (get-buffer-process cvc-compile-buffer) t)) 429 430(defun cvc-send-signal (sig) 431 "Sends signal SIG to the CVC process. SIG must be an integer." 432 (if (get-buffer-process cvc-compile-buffer) 433 (if (file-exists-p ".cvc-pid") 434 (save-excursion 435 (let ((buf (get-buffer-create ".cvc-pid"))) 436 (set-buffer buf) 437 (erase-buffer) 438 (insert-file-contents ".cvc-pid") 439 (let ((pid (read buf))) 440 (if (integerp pid) 441 (signal-process pid sig) 442 (error "The file .cvc-pid is screwed up: %s" pid))) 443 (kill-buffer buf))) 444 (error "Your CVC version does not support signal handling")) 445 (error "CVC is not running"))) 446 447(defun cvc-send-usr1 () 448 "Sends SIGUSR1 to the current CVC process. I have a version of CVC 449that uses it to toggle dynamic variable ordering." 450 (interactive) 451 (cvc-send-signal 10)) 452 453(defun cvc-send-usr2 () 454 "Sends SIGUSR2 to the current CVC process. I have a version of CVC 455that uses it to force garbage collection." 456 (interactive) 457 (cvc-send-signal 12)) 458 459(defun cvc-set-verbose-level (arg) 460 "Sets CVC verbose level to use in command line option +/-quiet. 461If empty line is given, use the default." 462 (interactive (list (read-from-minibuffer "Set verbose level to: " 463 cvc-verbose-level))) 464 (if (stringp arg) 465 (progn 466 (if (string= arg "") (setq cvc-verbose-level nil) 467 (setq cvc-verbose-level arg)) 468 (setq cvc-options-changed t)) 469 (error "Not a string. The value is not set."))) 470 471(defun cvc-set-command (arg) 472 "Sets the name of the CVC executable to run." 473 (interactive (list (read-file-name "CVC binary: " 474 "" cvc-command nil cvc-command))) 475 (if (stringp arg) 476 (progn 477 (if (string= arg "") nil 478 (setq cvc-command arg)) 479 (setq cvc-options-changed t)) 480 (error "Not a string. The value is not set."))) 481 482(defun cvc-trace (arg) 483 "Adds a CVC tracing flag to be given in the +trace command line option." 484 (interactive (list (read-from-minibuffer "Add trace flag: " 485 cvc-verbose-level))) 486 (if (stringp arg) 487 (progn 488 (if (string= arg "") (error "Empty flag is not allowed") 489 (setq cvc-trace-flags (add-to-list 'cvc-trace-flags arg))) 490 (setq cvc-options-changed t) 491 (message "%S" cvc-trace-flags)) 492 (error "Not a string. The value is not set."))) 493 494(defun cvc-untrace (arg) 495 "Removes a CVC tracing flag given in the +trace command line option." 496 (interactive (list (completing-read "Remove trace flag: " 497 (mapcar '(lambda (x) (cons x t)) cvc-trace-flags) 498 nil t))) 499 (if (stringp arg) 500 (progn 501 (if (string= arg "") nil ; don't do anything on empty input 502 (setq cvc-trace-flags (delete arg cvc-trace-flags))) 503 (setq cvc-options-changed t) 504 (message "%S" cvc-trace-flags)) 505 (error "Not a string. The value is not set."))) 506 507(defun cvc-set-command-line-args (arg) 508 "Sets CVC command line options. Don't set -sat and +quiet 509options here, use corresponding special variables for that." 510 (interactive (list (read-from-minibuffer "Other arguments: " 511 cvc-command-line-args))) 512 (if (stringp arg) 513 (progn 514 (if (string= arg "") (setq cvc-command-line-args nil) 515 (setq cvc-command-line-args arg)) 516 (setq cvc-options-changed t)) 517 (error "Not a string. The value is not set."))) 518 519;;;; Saving file 520(defun cvc-save-buffer () 521 "Saves CVC file together with options. Prompts the user whether to 522override the *.opt file if the options have changed." 523 (interactive) 524 (let ((opt-file-name 525 (let ((match (string-match "\\.cvc$" 526 (buffer-file-name)))) 527 (if match 528 (concat (substring (buffer-file-name) 529 0 match) 530 ".opt") 531 (concat (buffer-file-name) ".opt"))))) 532 (cond ((and (file-exists-p opt-file-name) 533 cvc-options-changed) 534 (if (y-or-n-p "Options have changed. Save them?") 535 (progn 536 (cvc-save-options) 537 (setq cvc-options-changed nil)))) 538 (cvc-options-changed 539 (cvc-save-options) 540 (setq cvc-options-changed nil)))) 541 (save-buffer)) 542 543;;;; Indentation 544 545;; Definitions 546;; - A balanced expression is a matching-paren string or a command 547;; (with the semicolon serving as the close-paren) 548;; - An enclosing expression for line N is a balanced expression that 549;; includes the beginning of line N. 550 551;; Indentation rules: 552;; - The indentation of the first line of the buffer or a command is 0. 553;; - If the current line has the same innermost enclosing expression as 554;; the line before it, it has the same indentation as the line before it. 555;; - Otherwise, the indentation of a line is cvc-basic-offset to the right 556;; of the first character of its innermost enclosing expression. 557;; 558;; NOTE: In keeping with Emacs terminology, we consider 559;; opening/closing keywords and other paired delimiters as "parens." 560;; For simplicity's sake, we treat all such delimiters as parens and 561;; make no attempt to enforce true matching (e.g., we will treat "( [ ) ]" 562;; as a balanced expression). 563 564(defcustom cvc-basic-offset 2 565 "Amount of basic offset used when indenting CVC code.") 566 567(defun cvc-previous-line () 568 "Moves the point to the first non-comment non-blank string before 569the current one and positions the cursor on the first non-blank character. 570Returns nil if there is no previous non-comment non-blank line in the buffer." 571 (interactive) 572 (beginning-of-line) 573 (skip-chars-forward " \t") 574 (let ((starting-point (point))) 575 (forward-line -1) 576 (beginning-of-line) 577 (while (and (not (bobp)) (looking-at "\\s-*\\(?:$\\|%\\)")) 578 (forward-line -1) 579 (beginning-of-line)) 580 (cond ((bobp) 581 (goto-char starting-point) 582 nil) 583 (t (skip-chars-forward " \t"))))) 584 585(defun cvc-goto-indentation-anchor () 586 "Moves the point to the \"indentation anchor\" of the current line, 587i.e., the beginning of the innermost enclosing expression or command." 588 (let ((starting-point 589 ;; Find the beginning of the enclosing declaration 590 (save-excursion 591 (while (and (cvc-previous-line) 592 (not (looking-at cvc-declaration-regexp)))) 593 (point))) 594 (depth 1)) 595 (while (and (> depth 0) 596 (search-backward-regexp 597 (concat cvc-opening-paren-regexp "\\|" 598 cvc-closing-paren-regexp) 599 starting-point t)) 600 (if (looking-at cvc-opening-paren-regexp) 601 (setq depth (1- depth)) 602 (setq depth (1+ depth)))) 603 (if (> depth 0) 604 (goto-char starting-point)))) 605 606(defun cvc-current-indentation () 607 "Find the current indentation at point. The current indentation is 608cvc-basic-offset to the right of where the innermost enclosing expression 609or command starts, unless the previous line has the same indentation 610anchor and a customized indentation, in which case the customized 611indentation is used." 612 (let (anchor anchor-column previous-line previous-anchor previous-column) 613 (save-excursion 614 (cvc-goto-indentation-anchor) 615 (setq anchor (point)) 616 (setq anchor-column (current-column))) 617 (save-excursion 618 (cvc-previous-line) 619 (setq previous-line (point)) 620 (setq previous-column (current-column)) 621 (cvc-goto-indentation-anchor) 622 (setq previous-anchor (point))) 623 (if (and (eq anchor previous-anchor) 624 (not (eq anchor previous-line))) 625 previous-column 626 (+ anchor-column cvc-basic-offset)))) 627 628(defun cvc-compute-indentation () 629 "Computes the indentation for the current string based on the 630previous string." 631 (save-excursion 632 (beginning-of-line) 633 (skip-chars-forward " \t") 634 (if (looking-at cvc-declaration-regexp) 0 635 (let ((indent (cvc-current-indentation))) 636 (if (looking-at cvc-closing-keywords-regexp) 637 (if (< indent cvc-basic-offset) 0 638 (- indent cvc-basic-offset)) 639 indent))))) 640 ;; ((or (eq type 'opening) (eq type 'declaration)) 641 ;; (+ indent cvc-basic-offset)) 642 ;; (t indent)))))) 643 644(defun cvc-indent-line () 645 "Indent the current line relative to the previous meaningful line." 646 (interactive) 647 (let* ((initial (point)) 648 (final (let ((case-fold-search nil)) (cvc-compute-indentation))) 649 (offset0 (save-excursion 650 (beginning-of-line) 651 (skip-chars-forward " \t") 652 (- initial (point)))) 653 (offset (if (< offset0 0) 0 offset0))) 654 (indent-line-to final) 655 (goto-char (+ (point) offset)))) 656 657;; TODO: What's wrong with M-;? 658 659 660;;;; Now define the keymap 661 662(defconst cvc-mode-map nil "CVC keymap") 663 664(if cvc-mode-map () 665 (progn 666 (setq cvc-mode-map (make-sparse-keymap)) 667 (define-key cvc-mode-map [delete] 'backward-delete-char-untabify) 668 (define-key cvc-mode-map [backspace] 'backward-delete-char-untabify) 669 (define-key cvc-mode-map "\C-x\C-s" 'cvc-save-buffer) 670 (define-key cvc-mode-map "\C-c\C-e" 'cvc-edit-options) 671 (define-key cvc-mode-map "\C-c\C-f" 'cvc-run) 672 (define-key cvc-mode-map "\C-c\C-t" 'cvc-trace) 673 (define-key cvc-mode-map "\C-c\C-u" 'cvc-untrace) 674 (define-key cvc-mode-map "\C-c\C-r" 'cvc-set-command) 675 (define-key cvc-mode-map "\C-c\C-c" 'cvc-interrupt) 676 ;; (define-key cvc-mode-map "\C-c\C-r" 'cvc-send-usr1) 677 ;; (define-key cvc-mode-map "\C-c\C-s" 'cvc-send-usr2) 678 (define-key cvc-mode-map "\C-c;" 'comment-region) 679 (define-key cvc-mode-map "\t" 'cvc-indent-line))) 680 681(defun cvc-make-local-vars () 682 "Create buffer-local variables for CVC modes" 683 (make-local-variable 'cvc-command) 684 (make-local-variable 'cvc-sat-option) 685 (make-local-variable 'cvc-verbose-level) 686 (make-local-variable 'cvc-trace-flags) 687 (make-local-variable 'cvc-command-line-args) 688 (make-local-variable 'cvc-options-changed) 689 (make-local-variable 'cvc-options-changed)) 690 691(defun cvc-mode () 692 "Major mode for CVC specification files. 693 694\\{cvc-mode-map} 695 696\\[cvc-run] runs CVC on buffer, \\[cvc-interrupt] interrupts already 697running CVC process. 698 699\\[cvc-send-usr1] and \\[cvc-send-usr2] are used to send UNIX signals 700to CVC process to toggle dynamic variable ordering and force garbage 701collection respectively. Available only for a new (experimental) CVC 702version. 703 704Running CVC (\\[cvc-run]) creates a separate buffer where inferior CVC 705process will leave its output. Currently, each run of CVC clears the 706compilation buffer. If you need to save multiple runs, save them one 707at a time. 708 709Please report bugs to barrett@cs.nyu.edu." 710 (interactive) 711 (use-local-map cvc-mode-map) 712;;; Disable asking for the compile command 713 (make-local-variable 'compilation-read-command) 714 (setq compilation-read-command nil) 715;;; Make all the variables with CVC options local to the current buffer 716 (cvc-make-local-vars) 717 (setq cvc-options-changed nil) 718;;; Change the regexp search to be case sensitive 719;; (setq case-fold-search nil) 720;;; Set syntax table 721 (set-syntax-table cvc-mode-syntax-table) 722;; fix up comment handling 723 (set (make-local-variable 'comment-start) "%") 724 (set (make-local-variable 'comment-end) "") 725 (set (make-local-variable 'comment-start-skip) "%+\\s-*") 726 (setq require-final-newline t) 727 (set (make-local-variable 'indent-line-function) 'cvc-indent-line) 728;;; Define the major mode 729 (setq major-mode 'cvc-mode) 730 (setq mode-name "CVC") 731;;; Load command line options for CVC process 732 (let ((opt-file-name 733 (let ((match (string-match "\\.cvc$" 734 (buffer-file-name)))) 735 (if match 736 (concat (substring (buffer-file-name) 737 0 match) 738 ".opt") 739 (concat (buffer-file-name) ".opt"))))) 740 (if (file-exists-p opt-file-name) 741 (load opt-file-name))) 742;;; Do fontification, if necessary 743 (setq font-lock-keywords 744 (if font-lock-maximum-decoration 745 cvc-font-lock-keywords-2 746 cvc-font-lock-keywords-1)) 747 (if cvc-running-xemacs 748 (put 'cvc-mode 'font-lock-defaults 749 '(cvc-font-lock-keywords nil nil nil nil)) 750 (setq font-lock-defaults '(cvc-font-lock-keywords nil nil nil nil))) 751 (if (and cvc-font-lock-mode-on 752 (or cvc-running-xemacs font-lock-global-modes) 753 window-system) 754 (font-lock-mode 1)) 755 (setq mode-line-process nil) ; put 'cvc-status when hooked up to inferior CVC 756 (run-hooks 'cvc-mode-hook)) 757 758(defun cvc-options-edit-mode () 759 "Major mode for editing CVC options. Actually, this is Emacs Lisp 760mode with a few changes. In particular, \\[cvc-save-and-load-options] will save the file, 761find the associated CVC file and updates its options accordingly. See 762`\\[describe-bindings]' for key bindings. " 763 (interactive) 764 (emacs-lisp-mode) 765;;; Make all the variables with CVC options local to the current buffer 766;;; to avoid accidental override of the global values 767 (cvc-make-local-vars) 768 (setq major-mode 'cvc-options-edit-mode) 769 (setq mode-name "CVC Options") 770 (if (and cvc-font-lock-mode-on (or cvc-running-xemacs font-lock-global-modes) 771 window-system) 772 (font-lock-mode t)) 773 (use-local-map (copy-keymap (current-local-map))) 774 (local-set-key "\C-c\C-c" 'cvc-save-and-load-options)) 775 776(provide 'cvc-mode) 777