aboutsummaryrefslogtreecommitdiffhomepage
path: root/lego
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2008-07-24 09:51:53 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2008-07-24 09:51:53 +0000
commit76d6b0b2b1f039549d308a0d2c478a6b05869af9 (patch)
tree78cc7e13bf290a17e7006a6d4616a8a08e36ce8f /lego
parent8f8e9388b582ad6d3ee6e1eea842a8d443d4ce89 (diff)
Merge changes from Version4Branch.
Diffstat (limited to 'lego')
-rw-r--r--lego/lego.el4
-rw-r--r--lego/x-symbol-lego.el13
2 files changed, 2 insertions, 15 deletions
diff --git a/lego/lego.el b/lego/lego.el
index 0d138804..d6211edb 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -334,7 +334,7 @@ Checks the width in the `proof-goals-buffer'"
;; font-lock
- (setq font-lock-keywords lego-font-lock-keywords-1)
+ (set proof-script-font-lock-keywords lego-font-lock-keywords-1)
(proof-config-done)
@@ -357,7 +357,7 @@ Checks the width in the `proof-goals-buffer'"
("lego" . lego-tags))
tag-table-alist)))
- (setq blink-matching-paren-dont-ignore-comments t)
+ (set (make-local-variable 'blink-matching-paren-dont-ignore-comments) t)
;; hooks and callbacks
diff --git a/lego/x-symbol-lego.el b/lego/x-symbol-lego.el
deleted file mode 100644
index 86f6b185..00000000
--- a/lego/x-symbol-lego.el
+++ /dev/null
@@ -1,13 +0,0 @@
-;; x-symbol-lego.el
-;;
-;; David Aspinall, adapted from file supplied by David von Obheimb
-;; License: GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
-;;
-
-;; FIXME: to revitalise this, see coq/x-symbol-coq.el
-
-(error "LEGO support for X-Symbol has been removed in this release, sorry.")
-
-(provide 'x-symbol-lego)