contrib/cvc-mode.el

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