Extensive fixes for x-symbol and font-lock.

3 files changed, 9 insertions, 24 deletions

diff --git a/isa/isa-syntax.el b/isa/isa-syntax.el
index 861b6082..767df53a 100644
--- a/isa/isa-syntax.el
+++ b/isa/isa-syntax.el
@@ -297,7 +297,7 @@
    (cons (concat "\353\\?'" isa-idx "\350") 'isabelle-tvar-name-face)
    (cons (concat "\354" isa-id "\350") 'isabelle-free-name-face)
    (cons (concat "\355" isa-id "\350") 'isabelle-bound-name-face)
-   (cons (concat "\356" isa-idx "\350") 'isabelle-var-name-face)
+   (cons (concat "\356" "\\?" isa-idx "\350") 'isabelle-var-name-face)
    (cons (concat "\357" isa-idx "\350") 'proof-declaration-name-face)
    )
   "*Font-lock table for Isabelle terms.")
diff --git a/isa/isa.el b/isa/isa.el
index 849014c5..03cfaf22 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -313,7 +313,7 @@ proof-shell-retract-files-regexp."
 
 (eval-and-compile			; to define vars for byte comp.
 (define-derived-mode isa-pbp-mode pbp-mode
-  "Isabelle proofstate" nil
+  "Isabelle goals" nil
   (isa-pbp-mode-config)))
 
 (eval-and-compile			; to define vars for byte comp.
@@ -650,29 +650,16 @@ you will be asked to retract the file or process the remainder of it.
 ;; x-symbol support for Isabelle PG, provided by David von Oheimb.
 ;;
 ;; The following settings configure the generic PG package.
-;;
 ;; The token language "Isabelle Symbols" is in file x-symbol-isa.el
 ;;
 
-;; name of minor isa mode
-(defvar x-symbol-isa-name "Isabelle Symbols")
-
-(defvar x-symbol-isa-modes 
-  '(isasym-mode 
-    isa-proofscript-mode 
-    proof-response-mode			; should be isa-response-mode?
-    proofstate-mode			; isa-proofstate-mode?
-    isa-shell-mode 
-    isa-pbp-mode
-    thy-mode				; necessary?
-    isa-thy-mode
-    shell-mode				; necessary?
-    ))
-
-(defvar isasym-font-lock-keywords
-  '(("\\\\<[A-Za-z][A-Za-z0-9_']*>" (0 font-lock-type-face))))
-
-(setq proof-xsym-activate-command
+(setq proof-xsym-extra-modes
+      '(isasym-mode ; necessary?
+	thy-mode
+	shell-mode) ; necessary?
+      proof-xsym-font-lock-keywords
+      '(("\\\\<[A-Za-z][A-Za-z0-9_']*>" (0 font-lock-type-face)))
+      proof-xsym-activate-command
       "print_mode := (!print_mode union [\"xsymbols\",\"symbols\"])"
       proof-xsym-deactivate-command
       "print_mode := filter_out (fn x=>(rev (explode \"symbols\") prefix rev (explode x))) (!print_mode)")
diff --git a/isa/x-symbol-isa.el b/isa/x-symbol-isa.el
index d0cfbf81..5c38ced8 100644
--- a/isa/x-symbol-isa.el
+++ b/isa/x-symbol-isa.el
@@ -6,8 +6,6 @@
 (provide 'x-symbol-isa)
 (defvar x-symbol-isa-required-fonts nil)
 
-;(defvar x-symbol-isa-name "Isabelle Symbol")
-(defvar x-symbol-isa-modeline-name "isa")
 (defvar x-symbol-isa-header-groups-alist nil)
 ;'(("Operator" bigop operator)
 ;    ("Relation" relation)