/usr/share/emacs/site-lisp/acl2/acl2-mode.el is in acl2-emacs 8.0dfsg-1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 | ;; Copyright (C) 1985 Free Software Foundation, Inc.
;; Copyright (C) 1994 Free Software Foundation, Inc.
;; Author : MKSmith (mksmith@cli.com)
;; Begun : Feb 27 94
;; Origin : lisp-mode.el
;; Keywords: acl2, languages
;; This file is for use with GNU Emacs.
;; GNU Emacs is free software; you can redistribute it and/or modify
;; it under the terms of the GNU General Public License as published by
;; the Free Software Foundation; either version 2, or (at your option)
;; any later version.
;; GNU Emacs is distributed in the hope that it will be useful,
;; but WITHOUT ANY WARRANTY; without even the implied warranty of
;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
;; GNU General Public License for more details.
;;; Commentary:
;; The base major mode for editing Acl2 code.
;; This mode extends very slightly lisp-mode.el (documented in the Emacs manual).
;; See also inf-acl2.el inf-acl2-mouse.el and inf-acl2-menu.el
;;; Code:
(require 'lisp-mode)
(defvar acl2-mode-syntax-table nil "")
(defvar acl2-mode-abbrev-table nil "")
(if (not acl2-mode-syntax-table)
(setq acl2-mode-syntax-table
(copy-syntax-table lisp-mode-syntax-table)))
(define-abbrev-table 'acl2-mode-abbrev-table ())
(defun acl2-mode-variables (acl2-syntax)
(lisp-mode-variables nil)
(cond (acl2-syntax
(set-syntax-table acl2-mode-syntax-table)))
(setq local-abbrev-table acl2-mode-abbrev-table)
(make-local-variable 'lisp-indent-function)
(setq lisp-indent-function 'acl2-indent-function))
(defun acl2-shared-lisp-mode-map ()
"Return the shared lisp-mode-map, independent of Emacs version."
(if (boundp 'shared-lisp-mode-map)
shared-lisp-mode-map
lisp-mode-shared-map))
(defvar acl2-mode-map nil
"Keymap for ordinary Acl2 mode. All commands in
`acl2-shared-lisp-mode-map' are inherited by this map.")
(if (not acl2-mode-map)
(progn
(setq acl2-mode-map (make-sparse-keymap))
(set-keymap-parent acl2-mode-map (acl2-shared-lisp-mode-map))))
(defvar acl2-mode-hook nil)
(defun acl2-mode ()
"Major mode for editing Acl2 code.
Commands:
Delete converts tabs to spaces as it moves back.
Blank lines separate paragraphs. Semicolons start comments.
\\{acl2-mode-map}
Note that `run-acl2' may be used either to start an inferior Acl2 job
or to switch back to an existing one.
Entry to this mode calls the value of `acl2-mode-hook'
if that value is non-nil."
(interactive)
(kill-all-local-variables)
(use-local-map acl2-mode-map)
(setq major-mode 'acl2-mode)
(setq mode-name "Acl2")
(acl2-mode-variables t)
(set-syntax-table acl2-mode-syntax-table)
(run-hooks 'acl2-mode-hook))
;; Trying this as a local variable
;; See last entry in ACL2-MODE-VARIABLES function.
;; (defconst lisp-indent-function 'acl2-indent-function "")
(defvar last-sexp nil)
;; Identical to LISP-INDENT-FUNCTION except checks acl2-indent-hook
;; first for indentation. Allows user to format Acl2 differently from
;; lisp.
(defun acl2-indent-function (indent-point state)
(let ((normal-indent (current-column))
(last-sexp (point)))
(goto-char (1+ (elt state 1)))
(parse-partial-sexp (point) last-sexp 0 t)
(if (and (elt state 2)
(not (looking-at "\\sw\\|\\s_")))
;; car of form doesn't seem to be a a symbol
(progn
(if (not (> (save-excursion (forward-line 1) (point))
last-sexp))
(progn (goto-char last-sexp)
(beginning-of-line)
(parse-partial-sexp (point) last-sexp 0 t)))
;; Indent under the list or under the first sexp on the
;; same line as last-sexp. Note that first thing on that
;; line has to be complete sexp since we are inside the
;; innermost containing sexp.
(backward-prefix-chars)
(current-column))
(let ((function (buffer-substring (point)
(progn (forward-sexp 1) (point))))
method)
(setq method (or (get (intern-soft function) 'acl2-indent-hook)
(get (intern-soft function) 'lisp-indent-function)
;; Why does -hook follow -function?
(get (intern-soft function) 'lisp-indent-hook)))
(cond ((or (eq method 'defun)
(and (null method)
(> (length function) 3)
(string-match "\\`def" function)))
(lisp-indent-defform state indent-point))
((integerp method)
(lisp-indent-specform method state
indent-point normal-indent))
(method
(funcall method state indent-point)))))))
;; (put 'progn 'lisp-indent-function 0), say, causes progn to be indented
;; like defun if the first form is placed on the next line, otherwise
;; it is indented like any other form (i.e. forms line up under first).
(put 'if 'acl2-indent-hook nil) ;changed from 2 in lisp.
(put 'mv-let 'acl2-indent-hook 2)
(provide 'acl2-mode)
;;; acl2-mode.el ends here
|