aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-indent.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2010-08-08 13:42:31 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2010-08-08 13:42:31 +0000
commit95d8a7f7364fde5af433ffa0e6c9f5bf664c5ebc (patch)
tree9be997d4d9af9c12882d53434d8dbbcb49cbdcb6 /generic/proof-indent.el
parent0877b91645ec1a824eba51cf0ad46eb4d76a138f (diff)
Checkdoc cleanups
Diffstat (limited to 'generic/proof-indent.el')
-rw-r--r--generic/proof-indent.el15
1 files changed, 12 insertions, 3 deletions
diff --git a/generic/proof-indent.el b/generic/proof-indent.el
index fc035aea..2ff6cf69 100644
--- a/generic/proof-indent.el
+++ b/generic/proof-indent.el
@@ -1,4 +1,4 @@
-;; proof-indent.el Generic Indentation for Proof Assistants
+;;; proof-indent.el --- Generic indentation for proof assistants
;;
;; Authors: Markus Wenzel, David Aspinall
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
@@ -6,11 +6,16 @@
;; $Id$
;;
+
+;;; Commentary:
+;;
+
(require 'proof-config) ; config variables
(require 'proof-utils) ; proof-ass
(require 'proof-syntax) ; p-looking-at-safe, p-re-search
(require 'proof-autoloads) ; p-locked-end
+;;; Code:
(defun proof-indent-indent ()
"Determine indentation caused by syntax element at current point."
(cond
@@ -21,7 +26,7 @@
(t 0)))
(defun proof-indent-offset ()
- "Determine offset of syntax element at current point"
+ "Determine offset of syntax element at current point."
(cond
((proof-looking-at-syntactic-context)
proof-indent)
@@ -54,7 +59,8 @@
(proof-indent-goto-prev))))
(defun proof-indent-calculate (indent inner) ; Note: may change point!
- "Calculate proper indentation level at current point"
+ "Calculate indentation level at point.
+INDENT is current indentation level, INNER a flag for inner indentation."
(let*
((current (point))
(found-prev (proof-indent-goto-prev)))
@@ -89,4 +95,7 @@
(if (< (current-column) (current-indentation))
(back-to-indentation)))))
+
(provide 'proof-indent)
+
+;;; proof-indent.el ends here