blob: c3717b6bcaf2692fa6655a9c4ce13f100e9537df (
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
134
135
136
137
138
|
;; 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>
;;
;; proof-x-symbol.el,v 2.4 1999/08/23 18:38:40 da Exp
;;
;; 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;;DvO to DA: why that difficult calculations?
(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
))
;;
(setq proof-x-symbol-support-on enable)))
;; Initialize x-symbol-support.
;; DvO: if uncommented here, i.e. invoked at initialization time,
;; it does not work because it cannot find x-symbol feature -- why?
;; calling it in proof-shell-start at least works
;; (proof-x-symbol-toggle (if proof-x-symbol-support 1 0))
(defun proof-x-symbol-decode-region (start end)
"Call (x-symbol-decode-region START END), if x-symbol support is enabled."
(if proof-x-symbol-support-on
(x-symbol-decode-region start end)))
(defun proof-x-symbol-encode-shell-input ()
"Encode shell input in the variable STRING.
A value for proof-shell-insert-hook."
(and 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)))))))
;; sets x-symbol mode for the current buffer
(defun proof-x-symbol-mode (enable)
(setq x-symbol-language proof-assistant-symbol)
(if (eq x-symbol-mode (not enable))
(x-symbol-mode)) ;; DvO: this is a toggle
;; Needed ? Should let users do this in the
;; usual way, if it works.
(if (and x-symbol-mode (not font-lock-mode));;DvO
(font-lock-mode)
(unless (featurep 'mule)(x-symbol-nomule-fontify-cstrings))));;DvO
;;DvO: where to invoke this?
;; calling it in proof-shell-start at least works
(defun proof-x-symbol-mode-all-buffers (enable)
(if enable
(add-hook 'proof-shell-insert-hook
'proof-x-symbol-encode-shell-input)
(remove-hook 'proof-shell-insert-hook
'proof-x-symbol-encode-shell-input)
)
(remove-hook 'comint-output-filter-functions
'x-symbol-comint-output-filter)
(save-excursion
(and proof-shell-buffer
(set-buffer proof-shell-buffer)
(proof-x-symbol-mode enable))
(and proof-goals-buffer
(set-buffer proof-goals-buffer)
(proof-x-symbol-mode enable))
(and proof-response-buffer
(set-buffer proof-response-buffer)
(proof-x-symbol-mode enable))))
;; FIXME da: shouldn't the next part be in x-symbol-isa.el ??
;; DvO: no, at least part of it has to remain outside x-symbol-isa.el, because
;; it is required to register x-symbol-isa s.th. it can be autoloaded
;; name of minor isa mode
(defvar x-symbol-isa-name "Isabelle Symbols")
(defvar proof-general-isabelle-modes '(thy-mode isa-proofscript-mode
proof-response-mode isa-shell-mode isa-pbp-mode isasym-mode))
(defvar isa-modes '(isa-thy-mode isa-mode proofstate-mode))
;; major modes that should invoke minor isa mode
(defvar x-symbol-isa-modes (cons 'shell-mode (cons 'isasym-mode
(append isa-modes proof-general-isabelle-modes))))
;; FIXME da: this (or something) needs to be put into a function with
;; a require on x-symbol, so we fail more gracefully.
(if (fboundp 'x-symbol-register-language)
(progn
(x-symbol-register-language 'isa 'x-symbol-isa x-symbol-isa-modes)
;; install auto-invocation
(push (list x-symbol-isa-modes t ''isa) x-symbol-auto-mode-alist)
(put 'isasym-mode 'font-lock-defaults '(isasym-font-lock-keywords))
(defvar isasym-font-lock-keywords
'(("\\\\<[A-Za-z][A-Za-z0-9_']*>" (0 font-lock-type-face))))))
(provide 'proof-x-symbol)
;; End of proof-x-symbol.el
|
