diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-09-14 08:14:37 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-09-14 08:14:37 +0000 |
| commit | e596b43c84fbbf129aef175cf2029b213079d26a (patch) | |
| tree | b4230dea4f142ec03f310ed478af0017137e8986 /isar/isar.el | |
| parent | 6f132150739f94aaa70d92cc378195426f977aa7 (diff) | |
Add outline-heading-alist setting. Fix compilation.
Diffstat (limited to 'isar/isar.el')
| -rw-r--r-- | isar/isar.el | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/isar/isar.el b/isar/isar.el index e3ddbeb4..0455ec6d 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -15,19 +15,20 @@ ;; ;;; Code: -(require 'proof) +(require 'cl) -(eval-when-compile +(eval-when (compile) (require 'span) (require 'proof-syntax) (require 'pg-goals) (require 'pg-vars) - (defvar outline-heading-end-regexp nil) + (require 'outline) (defvar comment-quote-nested nil) (defvar isar-use-find-theorems-form nil) -; (proof-ready-for-assistant 'isar)) ; compile for isar -) + (defvar isar-use-linear-undo nil) + (proof-ready-for-assistant 'isar)) ; compile for isar +(require 'proof) (require 'isabelle-system) ; system code (require 'isar-find-theorems) ; "Find Theorems" search form @@ -612,7 +613,10 @@ Uses variables `string' and `scriptspan' passed by dynamic scoping." (setq proof-script-font-lock-keywords isar-font-lock-keywords-1) (set (make-local-variable 'comment-quote-nested) nil) ;; can cope with nested comments (set (make-local-variable 'outline-regexp) isar-outline-regexp) - (set (make-local-variable 'outline-heading-end-regexp) isar-outline-heading-end-regexp) + (set (make-local-variable 'outline-heading-end-regexp) + isar-outline-heading-end-regexp) + (set (make-local-variable 'outline-heading-alist) + isar-outline-heading-alist) (set (make-local-variable 'blink-matching-paren-dont-ignore-comments) t) (add-hook 'proof-shell-insert-hook 'isar-preprocessing) (proof-config-done)) |