aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/holes.el7
-rw-r--r--lib/pg-dev.el4
2 files changed, 5 insertions, 6 deletions
diff --git a/lib/holes.el b/lib/holes.el
index c0a864b0..38a90cfb 100644
--- a/lib/holes.el
+++ b/lib/holes.el
@@ -599,10 +599,9 @@ created. Return the number of holes created."
"Default hook after a skeleton insertion: put holes at each interesting position."
;; Not all versions of skeleton provide `skeleton-positions' and the
;; corresponding @ operation :-(
- (unless (boundp 'mmm-inside-insert-by-key) ; pc: this hack is ok for me
- (when (boundp 'skeleton-positions)
- (dolist (pos skeleton-positions) ;; put holes here
- (holes-set-make-active-hole pos pos)))))
+ (when (boundp 'skeleton-positions)
+ (dolist (pos skeleton-positions) ;; put holes here
+ (holes-set-make-active-hole pos pos))))
(defconst holes-jump-doc
(concat "Hit \\[holes-set-point-next-hole-destroy] to jump "
diff --git a/lib/pg-dev.el b/lib/pg-dev.el
index e11d15ff..758b3d51 100644
--- a/lib/pg-dev.el
+++ b/lib/pg-dev.el
@@ -101,13 +101,13 @@
'(proof-splash pg-assoc pg-xml proof-depends proof-indent proof-site
proof-shell proof-menu pg-pbrpm pg-pgip proof-script
proof-autoloads pg-response pg-goals proof-toolbar
- proof-easy-config proof-config proof-mmm proof
+ proof-easy-config proof-config proof
proof-utils proof-syntax pg-user pg-custom
proof-maths-menu proof-unicode-tokens
pg-thymodes pg-autotest
;;
isar-syntax isar-find-theorems isar-unicode-tokens
- isar-autotest interface-setup isabelle-system isar isar-mmm
+ isar-autotest interface-setup isabelle-system isar
isar-keywords
;;
coq-abbrev coq-db coq-unicode-tokens coq-local-vars coq coq-syntax