blob: e4e3df33d2a89a20a86e6d556d67fed33af4bcb3 (
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-x-symbol.el Support for x-symbol package
;;
;; Copyright (C) 1998 LFCS Edinburgh.
;; Author: David Aspinall <da@dcs.ed.ac.uk>
;;
;; With thanks to David von Oheimb for providing original
;; patches for using x-symbol with Isabelle Proof General.
;;
;; Maintainer: Proof General maintainer <proofgen@dcs.ed.ac.uk>
;;
;; $Id$
;;
;; TODO: Move proof-x-symbol-support to proof-config.
;; Add autoloads for this file.
(defcustom proof-x-symbol-support nil
"*Whether to use x-symbol in Proof General buffers.
If you activate this variable, whether or not you get x-symbol support
depends on if your proof assistant supports it and it is enabled
inside your Emacs."
:type 'boolean
:group 'proof-general)
;; Idea is that Proof General will only let this next variable
;; become t if all the necessary infrastructure is in place.
(defvar proof-x-symbol-support-on nil
"Non-nil if x-symbol support is currently switched on.")
(defun proof-x-symbol-toggle (&optional arg)
"Toggle support for x-symbol. With optional ARG, force on if ARG<>0"
(interactive "p")
(let ((enable (or (and arg (> arg 0))
(if arg
(and (not (= arg 0))
(not proof-x-symbol-support-on))
(not proof-x-symbol-support-on)))))
(if enable
;; Check that support is correctly set up: exit if
;; some condition is not satisfied.
(cond
((not (featurep 'x-symbol))
(error "Proof General: x-symbol package must be loaded into Emacs."))
;; Check proof assistant specific settings here
))
;;
(if enable
;; Turn it on
(progn
(add-hook 'proof-shell-insert-hook
'proof-x-symbol-encode-shell-input))
;; Turn it off
(remove-hook 'proof-shell-insert-hook
'proof-x-symbol-encode-shell-input))
(setq proof-x-symbol-support-on enable)))
;; Initialize x-symbol-support.
;; (proof-x-symbol-toggle (if proof-x-symbol-support 1 0))
;(defun proof-x-symbol-mode
; (if proof-x-symbol-support-on
; (setq x-symbol-language
(defun proof-x-symbol-decode-region (start end)
"Decode region START to END using x-symbol-decode-all.
No action if proof-x-symbol-support-on is nil."
(if proof-x-symbol-support-on
(save-restriction
(narrow-to-region start end)
(x-symbol-decode-all)
(unless (featurep 'mule) (x-symbol-nomule-fontify-cstrings)))))
(defun proof-x-symbol-encode-shell-input ()
"Encode shell input in the variable STRING.
A value for proof-shell-insert-hook."
(and x-symbol-mode x-symbol-language
(setq string
(save-excursion
(let ((language x-symbol-language)
(coding x-symbol-coding)
(selective selective-display))
(set-buffer (get-buffer-create "x-symbol comint"))
(erase-buffer)
(insert string)
(setq x-symbol-language language)
(x-symbol-encode-all nil coding))
(prog1 (buffer-substring)
(kill-buffer (current-buffer)))))))
(defun proof-x-symbol-mode ()
(if proof-x-symbol-support-on
(progn
(setq x-symbol-language proof-assistant-symbol)
(if (not x-symbol-mode)
(x-symbol-mode))
;; Needed ? Should let users do this in the
;; usual way, if it works.
(if (not font-lock-mode)
(font-lock-mode)))))
;;
;;(setq comint-input-sender 'x-symbol-comint-send)
;; FIXME: where do we need the next function?
(defun proof-x-symbol-comint-send (proc string)
(and x-symbol-mode x-symbol-language
(setq string
(save-excursion
(let ((language x-symbol-language)
(coding x-symbol-coding)
(selective selective-display))
(set-buffer (get-buffer-create "x-symbol comint"))
(erase-buffer)
(insert string)
(setq x-symbol-language language)
(x-symbol-encode-all nil coding))
(prog1 (buffer-substring)
(kill-buffer (current-buffer))))))
(funcall x-symbol-orig-compint-input-sender proc string))
(provide 'proof-x-symbol)
;; End of proof-x-symbol.el
|
