diff options
Diffstat (limited to 'phox/phox.el')
-rw-r--r-- | phox/phox.el | 47 |
1 files changed, 9 insertions, 38 deletions
diff --git a/phox/phox.el b/phox/phox.el index 7f54c5a8..1f8c2ef1 100644 --- a/phox/phox.el +++ b/phox/phox.el @@ -7,7 +7,7 @@ (eval-after-load "pg-custom" '(setq phox-toolbar-entries - (remassoc 'context phox-toolbar-entries))) + (assq-delete-all 'context phox-toolbar-entries))) ;; ======== User settings for PhoX ======== @@ -34,7 +34,7 @@ :group 'phox) (defcustom phox-sym-lock-enabled t - "*Whether to use x-symbol or not." + "*Whether to use yum symbol or not." :type 'boolean :group 'phox) @@ -107,9 +107,7 @@ (defun phox-config () "Configure Proof General scripting for PhoX." (if phox-sym-lock-enabled - (progn - (phox-sym-lock-start) - (setq phox-x-symbol-enable nil))) + (phox-sym-lock-start)) (setq proof-terminal-char ?\. ; ends every command proof-script-command-end-regexp "[.]\\([ \t\n\r]\\)" @@ -145,10 +143,7 @@ ) (phox-init-syntax-table) (setq pbp-goal-command "intro %s;") - (setq pbp-hyp-command "elim %s;") -;; the following is only useful for xemacs - (define-key phox-mode-map [(meta ?.)] 'phox-complete-tag) -) + (setq pbp-hyp-command "elim %s;")) (defun phox-shell-config () "Configure Proof General shell for PhoX." @@ -189,14 +184,7 @@ ;; it is nice to do : xmodmap -e "keysym KP_Enter = Linefeed" (define-key phox-mode-map [(control c) (meta d)] - 'phox-delete-symbol-on-cursor) - ;(if phox-x-symbol-enable -; (progn - ; (setq x-symbol-language 'phox) - ; (x-symbol-mode t))) ; just to be sure -; (font-lock-mode t) ; just to be sure (not always activated on OSX ??) - -) + 'phox-delete-symbol-on-cursor)) (define-derived-mode phox-shell-mode proof-shell-mode "PhoX shell" nil @@ -206,7 +194,8 @@ (define-derived-mode phox-response-mode proof-response-mode "PhoX response" nil (setq - font-lock-keywords (append phox-font-lock-keywords proof-xsym-font-lock-keywords) + proof-resp-font-lock-keywords + (append phox-font-lock-keywords proof-xsym-font-lock-keywords) proof-output-fontify-enable t) (phox-sym-lock-start) (if (and (featurep 'phox-sym-lock) phox-sym-lock-enabled) @@ -218,7 +207,8 @@ (define-derived-mode phox-goals-mode proof-goals-mode "PhoX goals" nil (setq - font-lock-keywords (append phox-font-lock-keywords proof-xsym-font-lock-keywords) + proof-goals-font-lock-keywords + (append phox-font-lock-keywords proof-xsym-font-lock-keywords) proof-output-fontify-enable t) (phox-sym-lock-start) (if (and (featurep 'phox-sym-lock) phox-sym-lock-enabled) @@ -244,25 +234,6 @@ (append phox-top-keywords phox-proof-keywords) ) -;;; -;;; X-Symbol -;;; - -(defpgdefault x-symbol-language 'phox) - -(eval-after-load "x-symbol-phox" - ;; Add x-symbol tokens to phox-completion-table and rebuild - ;; internal completion table if completion is already active -'(progn - (defpgdefault completion-table - (append phox-completion-table - (mapcar (lambda (xsym) (nth 2 xsym)) - x-symbol-phox-table))) - (setq proof-xsym-font-lock-keywords - x-symbol-phox-font-lock-keywords) - (if (featurep 'completion) - (proof-add-completions)))) - (provide 'phox) |