From 76d6b0b2b1f039549d308a0d2c478a6b05869af9 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 24 Jul 2008 09:51:53 +0000 Subject: Merge changes from Version4Branch. --- phox/phox-tags.el | 66 +++++---------- phox/phox.el | 47 ++--------- phox/x-symbol-phox.el | 230 -------------------------------------------------- 3 files changed, 29 insertions(+), 314 deletions(-) delete mode 100644 phox/x-symbol-phox.el (limited to 'phox') diff --git a/phox/phox-tags.el b/phox/phox-tags.el index c62fe331..4851eb8c 100644 --- a/phox/phox-tags.el +++ b/phox/phox-tags.el @@ -21,29 +21,15 @@ (defun phox-tags-add-table(table) "add tags table" (interactive "D directory, location of a file named TAGS to add : ") - (if (featurep 'xemacs) - (let ((association (cons buffer-file-name table))) - (if (member association tag-table-alist) - (message "%s already loaded." table) - (setq tag-table-alist (cons association tag-table-alist)))) - ; gnu emacs - (if (member table tags-table-list) - (message "%s already loaded." table) -; (make-local-variable 'tags-table-list) ; ne fonctionne pas - (setq tags-table-list (cons table tags-table-list)) - ) - ) - ) + (if (member table tags-table-list) + (message "%s already loaded." table) + ;; (make-local-variable 'tags-table-list) ; ne fonctionne pas + (setq tags-table-list (cons table tags-table-list)))) (defun phox-tags-reset-table() "Set tags-table-list to nil." (interactive) -; (make-local-variable 'tags-table-list) - (if (featurep 'xemacs) - (progn - (setq tag-table-alist (remassoc buffer-file-name tag-table-alist))) - (setq tags-table-list nil)) - ) + (setq tags-table-list nil)) (defun phox-tags-add-doc-table() "Add tags in text documentation." @@ -75,37 +61,25 @@ (defun phox-complete-tag() -"Complete symbol using tags table. Works with FSF emacs. - Problems with xemacs." -;; xemacs build a table for completion, tag-completion-table this table -;; donnot contains key words that use ".". There is a problem with -;; syntax-table. In xemacs you need to redefine -;; add-to-tag-completion-table, in order to add your file-type and -;; syntax-table. The modification is very simple, there should be an -;; hook for that. -;; -(interactive) -(if (featurep 'xemacs) - (tag-complete-symbol) - (complete-tag) - ) -) + "Complete symbol using tags table." + (interactive) + (complete-tag)) ;; menu (defvar phox-tags-menu - '("Tags" - ["create a tags table for local buffer" phox-tags-create-local-table t] - ["------------------" nil nil] - ["add table" phox-tags-add-table t] - ["add local table" phox-tags-add-local-table t] - ["add table for libraries" phox-tags-add-lib-table t] - ["add table for text doc" phox-tags-add-doc-table t] - ["reset tags table list" phox-tags-reset-table t] - ["------------------" nil nil] - ["Find theorem, definition ..." find-tag t] - ["complete theorem, definition ..." phox-complete-tag t] - ) + '("Tags" + ["create a tags table for local buffer" phox-tags-create-local-table t] + ["------------------" nil nil] + ["add table" phox-tags-add-table t] + ["add local table" phox-tags-add-local-table t] + ["add table for libraries" phox-tags-add-lib-table t] + ["add table for text doc" phox-tags-add-doc-table t] + ["reset tags table list" phox-tags-reset-table t] + ["------------------" nil nil] + ["Find theorem, definition ..." find-tag t] + ["complete theorem, definition ..." phox-complete-tag t] + ) "Phox menu for dealing with tags" ) 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) diff --git a/phox/x-symbol-phox.el b/phox/x-symbol-phox.el deleted file mode 100644 index 8590dd23..00000000 --- a/phox/x-symbol-phox.el +++ /dev/null @@ -1,230 +0,0 @@ -;; x-symbol-phox.el -;; Token language "PhoX Symbols" for package x-symbol -;; -;; ID: $Id$ -;; Author: C. Raffalli -;; Updates by Markus Wenzel, Christoph Wedler, David Aspinall. -;; Copyright 1998 Technische Universitaet Muenchen -;; License GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; Adapted from x-symbol-isabelle.el -;; NB: Part of Proof General distribution. -;; - -(require 'proof-utils) - -(defvar x-symbol-phox-required-fonts nil) - -;;;=========================================================================== -;;; General language accesses, see `x-symbol-language-access-alist' -;;;=========================================================================== - -;; NB da: these next two are also set in proof-x-symbol.el, but -;; it would be handy to be able to use this file away from PG. -;; FIXME: In future could fix things so just -;; (require 'proof-x-symbol) would be enough here. -(require 'proof-x-symbol) -;(defvar x-symbol-phox-name "phox") -;(defvar x-symbol-phox-modeline-name "phox") - - -(defcustom x-symbol-phox-header-groups-alist nil - "*If non-nil, used in isasym specific grid/menu. -See `x-symbol-header-groups-alist'." - :group 'x-symbol-phox - :group 'x-symbol-input-init - :type 'x-symbol-headers) - -(defcustom x-symbol-phox-electric-ignore - "/\\\\\\|\\\\/" - "*Additional Phox version of `x-symbol-electric-ignore'." - :group 'x-symbol-phox - :group 'x-symbol-input-control - :type 'x-symbol-function-or-regexp) - -(defvar x-symbol-phox-required-fonts nil - "List of features providing fonts for language `phox'.") - -(defvar x-symbol-phox-extra-menu-items nil - "Extra menu entries for language `phox'.") - -(defvar x-symbol-phox-token-grammar - ;; CW: for X-Symbol-4.4.3: - ;; '(x-symbol-make-grammar ...) - (if (fboundp 'x-symbol-make-grammar) ;; x-symbol >=4.3 versions - (x-symbol-make-grammar - :encode-spec '(((id . "[_'a-zA-Z0-9]") (op . "[]><=\\/~&+-*%!{}:-]")) . - ((id . "[_'a-zA-Z0-9]") (op . "[]><=\\/~&+-*%!{}:-]"))) - :decode-spec '(((id . "[_'a-zA-Z0-9]") (op . "[]><=\\/~&+-*%!{}:-]")) . - ((id . "[_'a-zA-Z0-9]") (op . "[]><=\\/~&+-*%!{}:-]"))) - :decode-regexp "\\([_'a-zA-Z0-9]+\\)\\|\\([]><=\\/~&+-*%!{}:-]+\\)" - :token-list #'x-symbol-phox-default-token-list - :input-spec '(((id . "[_'a-zA-Z0-9]") (op . "[]><=\\/~&+-*%!{}:-]")) . - ((id . "[_'a-zA-Z0-9]") (op . "[]><=\\/~&+-*%!{}:-]")))))) - -(defvar x-symbol-phox-input-token-grammar - '("\\([_'a-zA-Z0-9]+\\)\\|\\([]><=\\/~&+-*%!{}:-]+\\)" - ((id . "[A-Za-z_0-9]") (op . "[<>!+-*/|&]")) - (id . "[A-Za-z_0-9]") (op . "[<>!+-*/|&]")) - "Grammar of input method Token for language `phox'.") - -(defun x-symbol-phox-default-token-list (tokens) - (mapcar - (lambda (x) - (cons x - (cond - ;; the shapes `id' and `op' are used by x-symbol-phox-token-grammar - ((string-match "\\`[A-Za-z_][A-Za-z_0-9]+\\'" x) - 'id) - ((string-match "\\`[]><=\\/~&+-*%!{}:-]+\\'" x) - 'op)))) - tokens)) - -(defvar x-symbol-phox-user-table nil - "User table defining Phox commands, used in `x-symbol-phox-table'.") - -(defvar x-symbol-phox-generated-data nil - "Internal.") - - -;;;=========================================================================== -;;; No image support -;;;=========================================================================== - -(defvar x-symbol-phox-master-directory 'ignore) -(defvar x-symbol-phox-image-searchpath '("./")) -(defvar x-symbol-phox-image-cached-dirs '("images/" "pictures/")) -(defvar x-symbol-phox-image-file-truename-alist nil) -(defvar x-symbol-phox-image-keywords nil) - - -;;;=========================================================================== -;;; Charsym Info -;;;=========================================================================== - -(defcustom x-symbol-phox-class-alist - '((VALID "Phox Symbol" (x-symbol-info-face)) - (INVALID "no Phox Symbol" (red x-symbol-info-face))) - "Alist for Phox's token classes displayed by info in echo area. -See `x-symbol-language-access-alist' for details." - :group 'x-symbol-texi - :group 'x-symbol-info-strings - :set 'x-symbol-set-cache-variable - :type 'x-symbol-class-info) - - -(defcustom x-symbol-phox-class-face-alist nil - "Alist for Phox's color scheme in TeXinfo's grid and info. -See `x-symbol-language-access-alist' for details." - :group 'x-symbol-phox - :group 'x-symbol-input-init - :group 'x-symbol-info-general - :set 'x-symbol-set-cache-variable - :type 'x-symbol-class-faces) - - -(defvar x-symbol-phox-font-lock-keywords nil) - -(defvar x-symbol-phox-font-lock-allowed-faces t) - -;;;=========================================================================== -;;; The tables -;;;=========================================================================== - -(defvar x-symbol-phox-case-insensitive nil) -(defvar x-symbol-phox-token-shape nil) -(defvar x-symbol-phox-input-token-ignore nil) - -;; FIXME: next one not needed in X-Symbol 4, kept for back compat. -;;(defvar x-symbol-phox-exec-specs -;; '(nil ("\\`\\\\<[A-Za-z][A-Za-z0-9_']*>\\'" . -;; "\\\\<[A-Za-z][A-Za-z0-9_']*>"))) - -(defvar x-symbol-phox-token-list 'identity) - -(defvar x-symbol-phox-xsymb0-table ; symbols - '((greaterequal ">=") - (lessequal "<=") - (notequal "!=") - (element "in") - (notelement "notin") - (propersubset "subset") - (intersection "inter") - (union "union") - (backslash3 "minus") - (universal1 "/\\") - (existential1 "\\/") - (logicalor "or") - (logicaland "&") - (arrowboth "<->") - (arrowright "->") - (arrowdblright "=>") - (notsign "~") - (lambda "\\") -)) - -(defun x-symbol-phox-prepare-table (table) - "Prepar the table." - (mapcar (lambda (entry) - (progn - (list (car entry) nil - (cadr entry)))) - table)) - -(defvar x-symbol-phox-table - (x-symbol-phox-prepare-table - (append x-symbol-phox-user-table x-symbol-phox-xsymb0-table))) - -(provide 'x-symbol-phox) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; -;; User-level settings for X-Symbol -;; -;; this is MODE-ON CODING 8BITS UNIQUE SUBSCRIPTS IMAGE -(defcustom x-symbol-phox-auto-style - '(phox-x-symbol-enable ; MODE-ON: whether to turn on interactively - nil ;; x-symbol-coding - 'null ;; x-symbol-8bits [NEVER want it; null disables search] - nil ;; x-symbol-unique - nil ;; x-symbol-subscripts - nil) ;; x-symbol-image - "Variable used to document a language access. -See documentation of `x-symbol-auto-style'." - :group 'x-symbol-phox - :group 'x-symbol-mode - :type 'x-symbol-auto-style) - -;; CW: this sexpr can be deleted with X-Symbol 4.4.3 -(eval-when-compile - ;; Next lines should allow this file to work standalone - ;; without proof-x-symbol.el. See comments further below too. - (require 'cl) - (ignore-errors (require 'x-symbol-vars))) - - -;;;=========================================================================== -;;; Internal -;;;=========================================================================== -;; CW: all are not needed in X-Symbol >= v4.3 - -(defvar x-symbol-phox-menu-alist nil - "Internal. Alist used for Isasym specific menu.") -(defvar x-symbol-phox-grid-alist nil - "Internal. Alist used for Isasym specific grid.") - -(defvar x-symbol-phox-decode-atree nil - "Internal. Atree used by `x-symbol-token-input'.") -(defvar x-symbol-phox-decode-alist nil - "Internal. Alist used for decoding of Isasym macros.") -(defvar x-symbol-phox-encode-alist nil - "Internal. Alist used for encoding to Isasym macros.") - -;; FIXME: next two not needed for newer X-Symbol versions. -(defvar x-symbol-phox-nomule-decode-exec nil - "Internal. File name of Isasym decode executable.") -(defvar x-symbol-phox-nomule-encode-exec nil - "Internal. File name of Isasym encode executable.") - -(provide 'x-symbol-phox) - -- cgit v1.2.3