blob: 3f66f664a3aaec03c26fb5cbe747e501ce8a1612 (
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
|
;;; junk.el
;;;
;;; $Id$
;;;
;;; Bits and pieces of code
;;; removed from main PG (or never added).
;;; Left here in case they're useful later.
;;;
;;; Also some testing code.
;;;
;;; TESTING FRAGMENTS
;;; special display regexps
(setq special-display-regexps
(cons "\\*isabelle-\\(goals\\|response\\)\\*"
special-display-regexps))
;;; dump str to buffer ug for testing.
(defun ugit (str)
(save-excursion
(set-buffer (get-buffer-create "ug"))
(goto-char (point-max))
(insert str)
(newline)
(newline)))
;;; OLD CODE
(defun proof-set-toggle (sym value)
"Try to set a boolean variable <blah>-enable using function <blah>-toggle."
(save-match-data
(let* ((nm (symbol-name sym))
(i (string-match "-enable" nm))
(tgfn (if i (intern (concat (substring nm 0 i) "-toggle")))))
(if (and tgfn (fboundp tgfn))
(funcall tgfn (if value 1 0))))))
;; Was in proof-shell.el
(defun proof-shell-popup-eager-annotation ()
"Process urgent messages.
Eager annotations are annotations which the proof system produces
while it's doing something (e.g. loading libraries) to say how much
progress it's made. Obviously we need to display these as soon as they
arrive."
;; FIXME: highlight eager annotation-end : fix proof-shell-handle-output
;; to highlight whole string.
(let ((str (proof-shell-handle-output
proof-shell-eager-annotation-start
proof-shell-eager-annotation-end
'proof-eager-annotation-face))
(proof-shell-message str))))
; (cond
; ((string-match "FSF" emacs-version)
; ;; setting font-lock-defaults explicitly is required by FSF Emacs
; ;; 20.2's version of font-lock
; (make-local-variable 'font-lock-defaults)
; (setq font-lock-defaults '(font-lock-keywords)))
; ;; In XEmacs, we must make a new variable to hold
; ;; the defaults.
; ;; (FIXME: this makes toggling font-lock robust now, before
; ;; it was ropy. Should check whether this is the right
; ;; was for FSF too).
; (t
; (let
; ((flks (intern (concat (symbol-name major-mode)
; "-font-lock-defaults"))))
; ;; Take a copy of current font-lock-keywords to make them
; ;; the default in future. Then font-lock-mode can be
; ;; safely switched on and off.
; (set flks font-lock-keywords)
; (make-local-variable 'proof-font-lock-defaults)
; (setq proof-font-lock-defaults font-lock-keywords)
; (setq font-lock-defaults '(proof-font-lock-defaults)))))
; (put major-mode 'font-lock-defaults (list flks)))))
|
