diff options
| author | David Aspinall | 1999-08-23 18:38:40 +0000 |
|---|---|---|
| committer | David Aspinall | 1999-08-23 18:38:40 +0000 |
| commit | aace1c631be427c1a96baf758170c2aa6c6fe627 (patch) | |
| tree | 761a542c239ba5791f9db2c75498183f3cd846c3 | |
| parent | 676c801b1b80cbb07a5e9f837c8e3e5c713813d2 (diff) | |
Disable properly if x-symbol is not available.
| -rw-r--r-- | generic/proof-x-symbol.el | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/generic/proof-x-symbol.el b/generic/proof-x-symbol.el index 3c0538da..2f2c1721 100644 --- a/generic/proof-x-symbol.el +++ b/generic/proof-x-symbol.el @@ -54,9 +54,10 @@ inside your Emacs." ; (if proof-x-symbol-support-on ; (setq x-symbol-language -;;DvO to be removed, replaced by x-symbol-decode-region (defun proof-x-symbol-decode-region (start end) -(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. @@ -90,9 +91,6 @@ A value for proof-shell-insert-hook." ;;(setq comint-input-sender 'x-symbol-comint-send) - - - (defun proof-x-symbol-mode-all-buffers (enable);;;DvO (if enable (add-hook 'proof-shell-insert-hook @@ -127,15 +125,17 @@ A value for proof-shell-insert-hook." ;; 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)))) -(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)))) -; end added part ;;DvO +;; 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 |