Tuned x-symbol config, moved settings to isabelle-system.el

2 files changed, 25 insertions, 16 deletions

diff --git a/isa/isa.el b/isa/isa.el
index 58e6dc82..2ecad011 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -612,9 +612,6 @@ you will be asked to retract the file or process the remainder of it."
 ;;
 
 (setq proof-xsym-extra-modes '(thy-mode)
-      proof-xsym-font-lock-keywords
-      ;; fontification for tokens themselves  (FIXME: broken)
-      '(("\\\\<[A-Za-z][A-Za-z0-9_']*>" (0 font-lock-type-face)))
       proof-xsym-activate-command
       "print_mode := ([\"xsymbols\",\"symbols\"] @ ! print_mode);"
       proof-xsym-deactivate-command
@@ -724,19 +721,6 @@ you will be asked to retract the file or process the remainder of it."
     ;; that's it for now!
     ))
 
-(eval-after-load "x-symbol-isa"
- ;; Add x-symbol tokens to isa-completion-table and rebuild
- ;; internal completion table if completion is already active
-'(progn
-(defpgdefault completion-table
-  (append (proof-ass completion-table)
-	  (mapcar (lambda (xsym) (nth 2 xsym))
-		  x-symbol-isa-table)))
-(if (featurep 'completion)
-    (proof-add-completions))))
-
-
-
 
 
 
diff --git a/isa/isabelle-system.el b/isa/isabelle-system.el
index 2e6aa775..ef2e4c79 100644
--- a/isa/isabelle-system.el
+++ b/isa/isabelle-system.el
@@ -288,5 +288,30 @@ until Proof General is restarted."
 (defpgdefault help-menu-entries isabelle-docs-menu)
 
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; X-Symbol language configuration, and adding to completion table
+;;
+
+(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
+ ;; internal completion table if completion is already active
+'(progn
+   (defpgdefault completion-table
+     (append (proof-ass completion-table)
+	     (mapcar (lambda (xsym) (nth 2 xsym))
+		     x-symbol-isabelle-table)))
+   (if (featurep 'completion)
+       (proof-add-completions))))
+
+
+
+
 (provide 'isabelle-system)
 ;; End of isabelle-system.el