From 9e83dfaa67bb7614568fdbb388686f80bd08c05b Mon Sep 17 00:00:00 2001 From: Christophe Raffalli Date: Thu, 25 Jul 2002 08:58:54 +0000 Subject: change to support version 4.4 of x-symbol --- phox/phox-font.el | 4 +- phox/phox.el | 23 +++-- phox/x-symbol-phox.el | 232 ++++++++++++++++++++++++++++++++++++++------------ 3 files changed, 195 insertions(+), 64 deletions(-) (limited to 'phox') diff --git a/phox/phox-font.el b/phox/phox-font.el index 020417ac..f34b051a 100644 --- a/phox/phox-font.el +++ b/phox/phox-font.el @@ -3,10 +3,8 @@ ;; Font lock keywords ;;--------------------------------------------------------------------------;; -(require 'proof-x-symbol) - (defconst phox-font-lock-keywords - (list + (list ;commands '("(\\*\\([^*]\\|\\*+[^*)]\\)*\\(\\*+)\\|\\**$\\)" 0 'font-lock-comment-face t) diff --git a/phox/phox.el b/phox/phox.el index 07511184..8b22dafe 100644 --- a/phox/phox.el +++ b/phox/phox.el @@ -133,7 +133,7 @@ proof-find-and-forget-fn 'phox-find-and-forget proof-find-theorems-command "search \"%s\"." proof-auto-multiple-files nil - font-lock-keywords phox-font-lock-keywords + font-lock-keywords (append phox-font-lock-keywords proof-xsym-font-lock-keywords) ) (phox-init-syntax-table) ;; the following is only useful for xemacs @@ -203,7 +203,7 @@ (define-derived-mode phox-response-mode proof-response-mode "PhoX response" nil (setq - font-lock-keywords phox-font-lock-keywords + font-lock-keywords (append phox-font-lock-keywords proof-xsym-font-lock-keywords) proof-output-fontify-enable t) (phox-sym-lock-start) (add-hook 'proof-shell-handle-delayed-output-hook 'phox-sym-lock-font-lock-hook) @@ -212,14 +212,14 @@ (define-derived-mode phox-goals-mode proof-goals-mode "PhoX goals" nil (setq - font-lock-keywords phox-font-lock-keywords + font-lock-keywords (append phox-font-lock-keywords proof-xsym-font-lock-keywords) proof-output-fontify-enable t) (phox-sym-lock-start) (add-hook 'pg-before-fontify-output-hook 'phox-sym-lock-font-lock-hook) (proof-goals-config-done)) ;; The response buffer and goals buffer modes defined above are -;; trivial. In fact, we don't need to define them at all -- they +;; trivial. In fact, we don't need t²o define them at all -- they ;; would simply default to "proof-response-mode" and "pg-goals-mode". ;; A more sophisticated instantiation might set font-lock-keywords to @@ -248,9 +248,22 @@ ; (set-variable 'phox-completion-table (defpgdefault completion-table -(append phox-top-keywords phox-proof-keywords) + (append phox-top-keywords phox-proof-keywords) ) +(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 (proof-ass 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 index e67d8774..122ccf93 100644 --- a/phox/x-symbol-phox.el +++ b/phox/x-symbol-phox.el @@ -1,82 +1,202 @@ +;; 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. +;; - -(defvar x-symbol-phox-name "PhoX") -(defvar phox-xsym-extra-modes '('phox-response-mode 'phox-goals-mode)) -(x-symbol-register-language 'phox 'x-symbol-phox '(phox-mode phox-shell-mode)) - +;; 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))) (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. +(defvar x-symbol-phox-name "PhoX Symbol") (defvar x-symbol-phox-modeline-name "phox") -(defvar x-symbol-phox-class-alist - '((VALID "PhoX Symbol" (x-symbol-info-face)) - (INVALID "no PhoX Symbol" (red x-symbol-info-face)))) -(defvar x-symbol-phox-font-lock-keywords nil) + +(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 nil +;; "[:'][A-Za-z]\\|<=\\|\\[\\[\\|\\]\\]\\|~=" + "*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 nil + :decode-regexp "\\([_'a-zA-Z0-9]+\\)\\|\\([]><=\\/~&+-*%!{}:-]+\\)" + :token-list #'x-symbol-phox-default-token-list))) + +(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 + ;; CW: where are the shapes `id' and `op' used? + ((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) -(defvar x-symbol-phox-token-shape nil) -(defvar x-symbol-phox-exec-specs nil) -(defvar x-symbol-phox-decoding-regexp "\\([_'a-zA-Z0-9]+\\)\\|\\([]><=\\/~&+-*%!{}:-]+\\)") -(defvar x-symbol-phox-surrounding-regexp "[ \n\t\r]") +;;;=========================================================================== +;;; 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 x-symbol-nomule-font-lock-keywords) +(defvar x-symbol-phox-font-lock-allowed-faces t) + +;;;=========================================================================== +;;; The tables +;;;=========================================================================== -(defvar x-symbol-phox-input-token-ignore nil) -(defvar x-symbol-phox-header-groups-alist nil) -(defvar x-symbol-phox-class-face-alist nil) -(defvar x-symbol-phox-electric-ignore nil) (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 "<<") + (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) + (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) + +;;;=========================================================================== +;;; 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-ahash nil - "Internal. Ahash.") (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) - -(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) - - -(defun x-symbol-phox-default-token-list (tokens) tokens) - -(defvar x-symbol-phox-token-list 'x-symbol-phox-default-token-list) -(defvar x-symbol-phox-user-table nil) -(defvar x-symbol-phox-xsymb0-table - '((greaterequal () ">=") - (lessequal () "<=") - (notequal () "!=") - (element () "in") - (notelement () "notin") - (propersubset () "<<") - (intersection () "inter") - (union () "union") - (backslash3 () "minus") - (universal1 () "/\\") - (existential1 () "\\/") - (logicalor () "or") - (logicaland () "&") - (arrowboth () "<->") - (arrowright () "->") - (arrowdblright () "=>") - (notsign () "~") - (lambda () "\\") -)) - -(defvar x-symbol-phox-table - (append x-symbol-phox-user-table x-symbol-phox-xsymb0-table)) - -(provide 'x-symbol-phox) \ No newline at end of file -- cgit v1.2.3