diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-07-18 15:30:21 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-07-18 15:30:21 +0000 |
| commit | e154c1151727bd20511aeb5a18ddbbb71d980ee6 (patch) | |
| tree | d15f40430ef94bb46dcc78414ee581af4c244eca /isar | |
| parent | 6f577f7a76aae1d0ff1100ec905c84c04a6ff47b (diff) | |
Fix sub/sups; defer loading x-symbol-isabelle.
Diffstat (limited to 'isar')
| -rw-r--r-- | isar/isar.el | 31 |
1 files changed, 13 insertions, 18 deletions
diff --git a/isar/isar.el b/isar/isar.el index 89832473..55a3b4f2 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -22,8 +22,6 @@ ;; (setq load-path (cons (concat proof-home-directory "isa/") load-path)) (require 'isabelle-system) -(require 'x-symbol-isabelle) ;; FIXME: ought to be auto-loaded later, - ;; and only if required. ;; ;; Load syntax @@ -556,44 +554,41 @@ proof-shell-retract-files-regexp." "Configure Proof General proof shell for Isabelle/Isar." (isar-init-output-syntax-table) (setq font-lock-keywords - ;; FIXME da: this is a bit broken; we should handle - ;; the x-symbol stuff by generic code, and also - ;; we should load x-symbol-isabelle later on. (append isar-output-font-lock-keywords-1 - x-symbol-isabelle-font-lock-keywords)) + (if (boundp 'x-symbol-isabelle-font-lock-keywords) + x-symbol-isabelle-font-lock-keywords))) (isar-shell-mode-config-set-variables) (proof-shell-config-done)) (defun isar-response-mode-config () (isar-init-output-syntax-table) (setq font-lock-keywords - ;; FIXME da: this is a bit broken; we should handle - ;; the x-symbol stuff by generic code, and also - ;; we should load x-symbol-isabelle later on. (append isar-output-font-lock-keywords-1 - x-symbol-isabelle-font-lock-keywords)) - ;; x-symbol-isabelle-font-lock-keywords)) + (if (boundp 'x-symbol-isabelle-font-lock-keywords) + x-symbol-isabelle-font-lock-keywords))) (proof-response-config-done)) (defun isar-goals-mode-config () ;; FIXME: next two broken, of course, as is PBP everywhere except LEGO. - (setq pg-goals-change-goal "Show %s.") + (setq pg-goals-change-goal "show %s.") (setq pg-goals-error-regexp proof-shell-error-regexp) (isar-init-output-syntax-table) - (setq font-lock-keywords ;FIXME handle x-symbol stuff by generic code!? - ;; (append - isar-goals-font-lock-keywords) - ;; x-symbol-isabelle-font-lock-keywords)) + (setq font-lock-keywords + (append + isar-output-font-lock-keywords-1 + (if (boundp 'x-symbol-isabelle-font-lock-keywords) + x-symbol-isabelle-font-lock-keywords))) (proof-goals-config-done)) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; x-symbol support ;; -;; The following settings configure the generic PG package; the main -;; part is in isa/x-symbol-isabelle.el +;; The following settings configure the generic PG package. +;; The token language "Isabelle Symbols" is in file isa/x-symbol-isabelle.el ;; (setq |