-
Notifications
You must be signed in to change notification settings - Fork 0
/
insert_cases.el
70 lines (66 loc) · 2.08 KB
/
insert_cases.el
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
(defun insert-case ()
"Insert the proper Case tactic at cursor position."
(interactive)
(let (names tmpname spoint cont)
(setq names '("S11Case" "S10Case" "S9Case" "S8Case"
"S7Case" "SSSSSSSCase"
"S6Case" "SSSSSSCase"
"S5Case" "SSSSSCase"
"S4Case" "SSSSCase"
"S3Case" "SSSCase" "SSCase"
"SCase" "Case"))
(setq cont nil)
(with-current-buffer "*goals*"
(goto-char (point-min))
(while names
(setq tmpname (pop names))
(if (search-forward (concat " " tmpname) nil t)
(progn
(search-forward "\"")
(setq spoint (1- (point)))
(search-forward "\"")
(setq cont
(concat tmpname " "
(buffer-substring-no-properties spoint (point)) "."))
(setq names nil)
)
)
)
)
(if cont (insert cont)))
)
(global-set-key (kbd "C-c C-a C-z") 'insert-case)
(defun insert-all-cases ()
"Insert all the proper Case tactics at cursor position."
(interactive)
(let (names tmpname spoint cont)
(setq names '("Case" "SCase"
"SSCase" "S3Case" "SSSCase" "S4Case" "SSSSCase"
"S5Case" "SSSSSCase" "S6Case" "SSSSSSCase"
"S7Case" "SSSSSSSCase"
"S8Case" "S9Case" "S10Case" "S11Case" ))
(setq cont nil)
(with-current-buffer "*goals*"
(while names
(goto-char (point-min))
(setq tmpname (pop names))
(if (search-forward (concat " " tmpname) nil t)
(progn
(search-forward "\"")
(setq spoint (1- (point)))
(search-forward "\"")
(setq cont
(if cont
(concat cont "; " tmpname " "
(buffer-substring-no-properties spoint (point)))
(concat tmpname " "
(buffer-substring-no-properties spoint (point)))
)
)
)
)
)
)
(if cont (insert (concat cont ". "))))
)
(global-set-key (kbd "C-c C-a C-q") 'insert-all-cases)