Fix sub/sups; defer loading x-symbol-isabelle.

2 files changed, 15 insertions, 25 deletions

diff --git a/isa/isabelle-system.el b/isa/isabelle-system.el
index 5faf6928..5199887b 100644
--- a/isa/isabelle-system.el
+++ b/isa/isabelle-system.el
@@ -383,9 +383,6 @@ until Proof General is restarted."
 
 (defpgdefault x-symbol-language 'isabelle)
 
-(setq proof-xsym-font-lock-keywords
-      ;; fontification for tokens themselves  (FIXME: broken)
-      '(("\\\\<[A-Za-z][A-Za-z0-9_']*>" (0 font-lock-type-face))))
 
 (eval-after-load "x-symbol-isabelle"
  ;; Add x-symbol tokens to isa-completion-table and rebuild
@@ -395,13 +392,11 @@ until Proof General is restarted."
      (append (proof-ass completion-table)
 	     (mapcar (lambda (xsym) (nth 2 xsym))
 		     x-symbol-isabelle-table)))
+   (setq proof-xsym-font-lock-keywords
+	 x-symbol-isabelle-font-lock-keywords)
    (if (featurep 'completion)
        (proof-add-completions))))
 
-;; FIXME: next setting is made properly in x-symbol-isabelle.el,
-;; but added here to avoid loading that file too early.
-
-(defvar x-symbol-isabelle-font-lock-keywords nil)
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
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