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
|
;; proof-indent.el Generic Indentation for Proof Assistants
;;
;; Authors: Markus Wenzel, David Aspinall
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;
;; proof-indent.el,v 9.0 2008/01/30 15:22:16 da Exp
;;
(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
(defun proof-indent-indent ()
"Determine indentation caused by syntax element at current point."
(cond
((proof-looking-at-safe proof-indent-open-regexp)
proof-indent)
((proof-looking-at-safe proof-indent-close-regexp)
(- proof-indent))
(t 0)))
(defun proof-indent-offset ()
"Determine offset of syntax element at current point"
(cond
((proof-looking-at-syntactic-context)
proof-indent)
((proof-looking-at-safe proof-indent-inner-regexp)
proof-indent)
((proof-looking-at-safe proof-indent-enclose-regexp)
proof-indent-enclose-offset)
((proof-looking-at-safe proof-indent-open-regexp)
proof-indent-open-offset)
((proof-looking-at-safe proof-indent-close-regexp)
proof-indent-close-offset)
((proof-looking-at-safe proof-indent-any-regexp) 0)
((proof-looking-at-safe "\\s-*$") 0)
(t proof-indent)))
(defun proof-indent-inner-p ()
"Check if current point is between actual indentation elements."
(or
(proof-looking-at-syntactic-context)
(proof-looking-at-safe proof-indent-inner-regexp)
(not
(or (proof-looking-at-safe proof-indent-any-regexp)
(proof-looking-at-safe "\\s-*$")))))
(defun proof-indent-goto-prev () ; Note: may change point, even in case of failure!
"Goto to previous syntax element for script indentation, ignoring string/comment contexts."
(and
(proof-re-search-backward proof-indent-any-regexp nil t)
(or (not (proof-looking-at-syntactic-context))
(proof-indent-goto-prev))))
(defun proof-indent-calculate (indent inner) ; Note: may change point!
"Calculate proper indentation level at current point"
(let*
((current (point))
(found-prev (proof-indent-goto-prev)))
(if (not found-prev) (goto-char current)) ; recover position
(cond
((and found-prev (or proof-indent-hang
(= (current-indentation) (current-column))))
(+ indent
(current-column)
(if (and inner (not (proof-indent-inner-p))) 0 (proof-indent-indent))
(- (proof-indent-offset))))
((not found-prev) 0) ;FIXME mmw: improve this case!?
(t
(proof-indent-calculate
(+ indent (if inner 0 (proof-indent-indent))) inner)))))
;;;###autoload
(defun proof-indent-line ()
"Indent current line of proof script, if indentation enabled."
(interactive)
(unless (not (proof-ass script-indent))
(if (< (point) (proof-locked-end))
(if (< (current-column) (current-indentation))
(skip-chars-forward "\t "))
(save-excursion
(indent-line-to
(max 0 (save-excursion
(back-to-indentation)
(proof-indent-calculate
(proof-indent-offset) (proof-indent-inner-p))))))
(if (< (current-column) (current-indentation))
(back-to-indentation)))))
(provide 'proof-indent)
|
