blob: 5f58fa1b30c52683494251e3a5eeeeacdfb378ff (
plain)
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
|
;; proof-indent.el Generic Indentation for Proof Assistants
;;
;; Authors: Markus Wenzel, David Aspinall
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;
;; $Id$
;;
(require 'proof) ; loader
(require 'proof-script) ; indent code is for script editing
(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
(proof-queue-or-locked-end) 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))))
(if proof-indent-pad-eol
(proof-indent-pad-eol)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Useless spaces
;;
(defun proof-indent-pad-eol (&optional col)
"Add padding to end of current line to match the previous line or COL.
This function adds useless space to buffers, but it cleans up the appearance
of locked regions in XEmacs."
;; A hook for TAB?
(interactive)
(save-excursion
(let ((descol (or col
(save-excursion
(end-of-line 0)
(current-column)))))
(save-excursion
(end-of-line 1)
(if (or (equal (current-column) 0) ;; special case for empty lines
(> descol (current-column)))
(progn
(insert-char ?\ (- descol (current-column)))))))))
(defun proof-indent-pad-eol-region (start end)
"Pad a region with extra spaces to the length of the longest line."
(interactive)
;; Find the longest line..
;; pad others to the same length
)
(provide 'proof-indent)
|
