blob: deb40e56ae64e3292fa9063631e607b54eb1536d (
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
|
;; pg-assoc.el Functions for associated buffers
;;
;; Copyright (C) 1994-2002 LFCS Edinburgh.
;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen,
;; Thomas Kleymann and Dilip Sequeira
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;
;; $Id$
;;
;; A sub-module of proof-shell; assumes proof-script loaded.
(require 'proof-script)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Defines an empty mode inherited by modes of the associated buffers.
;;
(eval-and-compile
(define-derived-mode proof-universal-keys-only-mode fundamental-mode
proof-general-name "Universal keymaps only"
;; Doesn't seem to supress TAB, RET
(suppress-keymap proof-universal-keys-only-mode-map 'all)
(proof-define-keys proof-universal-keys-only-mode-map
proof-universal-keys)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Return a list of associated buffers
;;
(defun proof-associated-buffers ()
"Return a list of the associated buffers.
Some may be dead/nil."
(list proof-goals-buffer
proof-response-buffer
proof-trace-buffer
proof-thms-buffer))
(defun proof-associated-windows ()
"Return a list of the associated buffers windows.
dead or nil buffers are not represented in the list."
(let ((lwin (mapcar '(lambda (b) (and b (get-buffer-window b)))
(proof-associated-buffers))))
(proof-list-filter lwin '(lambda (x) (not (null x))))
))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Manipulating prover output
;;
(defun pg-assoc-strip-subterm-markup (string)
"Return STRING with subterm and pbp annotations removed.
Special annotations are characters with codes higher than
'pg-subterm-first-special-char'.
If pg-subterm-first-special-char is unset, return STRING unchanged."
(if pg-subterm-first-special-char
(let* ((ip 0) (op 0) (l (length string)) (out (make-string l ?x )))
(while (< ip l)
(if (>= (aref string ip) pg-subterm-first-special-char)
(if (and pg-subterm-start-char
(char-equal (aref string ip) pg-subterm-start-char))
(progn (incf ip)
;; da: this relies on annotations being
;; characters between \200 and first special
;; char (e.g. \360). Why not just look for
;; the sep char??
(while
(< (aref string ip)
pg-subterm-first-special-char)
(incf ip))))
(aset out op (aref string ip))
(incf op))
(incf ip))
(substring out 0 op))
string))
(defun pg-assoc-strip-subterm-markup-buf (start end)
"Remove subterm and pbp annotations from region."
;; FIXME: create these regexps ahead of time.
(if pg-subterm-start-char
(let ((ann-regexp
(concat
(regexp-quote (char-to-string pg-subterm-start-char))
"[^"
(regexp-quote (char-to-string pg-subterm-sep-char))
"]*"
(regexp-quote (char-to-string pg-subterm-sep-char)))))
(save-restriction
(narrow-to-region start end)
(goto-char start)
(proof-replace-regexp ann-regexp "")
(goto-char start)
(proof-replace-string (char-to-string pg-subterm-end-char) "")
(goto-char start)
(if pg-topterm-char
(proof-replace-string (char-to-string pg-topterm-char) ""))))))
(defun pg-assoc-strip-subterm-markup-buf-old (start end)
"Remove subterm and pbp annotations from region."
(let (c)
(goto-char start)
(while (< (point) end)
;; FIXME: small OBO here: if char at end is special
;; it won't be removed.
(if (>= (setq c (char-after (point)))
pg-subterm-first-special-char)
(progn
(delete-char 1)
(decf end)
(if (char-equal c pg-subterm-start-char)
(progn
;; FIXME: could simply replace this by replace
;; match, matching on sep-char??
(while (and (< (point) end)
(< (char-after (point))
pg-subterm-first-special-char))
(delete-char 1)
(decf end)))))
(forward-char)))
end))
(provide 'pg-assoc)
;; pg-assoc.el ends here.
|
