blob: f212fbc35d2ec49af680c1e673eda00382530ad9 (
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
130
131
132
133
|
;; 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))
(defvar pg-assoc-ann-regexp nil
"Cache of regexp for `pg-assoc-strip-subterm-markup-buf'.")
(defun pg-assoc-strip-subterm-markup-buf (start end)
"Remove subterm and pbp annotations from region."
(if pg-subterm-start-char
(progn
(unless pg-assoc-ann-regexp
(setq pg-assoc-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 pg-assoc-ann-regexp "")
(goto-char start)
(proof-replace-string (char-to-string pg-subterm-end-char) "")
(goto-char start)
(if pg-topterm-regexp
(proof-replace-regexp pg-topterm-regexp ""))))))
(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.
|
