From 50c5e88196ad1b7ab0483a9e23f9035733a89c2e Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 14 Apr 2004 17:25:52 +0000 Subject: Remove X-symbol support from secondary provers temporarily --- hol98/x-symbol-hol98.el | 77 ++--------------------------------------------- lego/x-symbol-lego.el | 74 ++------------------------------------------- twelf/x-symbol-twelf.el | 79 ++----------------------------------------------- 3 files changed, 6 insertions(+), 224 deletions(-) diff --git a/hol98/x-symbol-hol98.el b/hol98/x-symbol-hol98.el index 920af03d..38c06ac3 100644 --- a/hol98/x-symbol-hol98.el +++ b/hol98/x-symbol-hol98.el @@ -5,81 +5,8 @@ ;; $Id$ ;; -(defvar x-symbol-hol98-symbol-table - '((longarrowright () "->" "\\") - (longarrowdblright () "==>" "\\") - (logicaland () "/\\" "\\") - (logicalor () "\\/" "\\") - (equivalence () "<->" "\\") - (existential1 () "EX" "\\") - (universal1 () "ALL" "\\") - ;; some naughty ones, but probably what you'd like - ;; (a mess in words like "searching" "philosophy" etc!!) - (Gamma () "Gamma" "\\") - (Delta () "Delta" "\\") - (Theta () "Theta" "\\") - (Lambda () "Lambda" "\\") - (Pi () "Pi" "\\") - (Sigma () "Sigma" "\\") - (Phi () "Phi" "\\") - (Psi () "Psi" "\\") - (Omega () "Omega" "\\") - (alpha () "alpha" "\\") - (beta () "beta" "\\") - (gamma () "gamma" "\\") - (delta () "delta" "\\") - (epsilon1 () "epsilon" "\\") - (zeta () "zeta" "\\") - (eta () "eta" "\\") - (theta1 () "theta" "\\") - (kappa1 () "kappa" "\\") - (lambda () "lambda" "\\") -; (mu () "mu" "\\") -; (nu () "nu" "\\") -; (xi () "xi" "\\") -; (pi () "pi" "\\") - (rho () "rho" "\\") - (sigma () "sigma" "\\") - (tau () "tau" "\\") - (phi1 () "phi" "\\") -; (chi () "chi" "\\") - (psi () "psi" "\\") - (omega () "omega" "\\"))) - -;; All the stuff X-Symbol complains about -(defvar x-symbol-hol98-master-directory 'ignore) -(defvar x-symbol-hol98-image-searchpath '("./")) -(defvar x-symbol-hol98-image-cached-dirs '("images/" "pictures/")) -(defvar x-symbol-hol98-image-keywords nil) -(defvar x-symbol-hol98-font-lock-keywords nil) -(defvar x-symbol-hol98-header-groups-alist nil) -(defvar x-symbol-hol98-class-alist - '((VALID "Hol98 Symbol" (x-symbol-info-face)) - (INVALID "no Hol98 Symbol" (red x-symbol-info-face)))) -(defvar x-symbol-hol98-class-face-alist nil) -(defvar x-symbol-hol98-electric-ignore nil) -(defvar x-symbol-hol98-required-fonts nil) -(defvar x-symbol-hol98-case-insensitive nil) -;; Setting token shape prevents "philosophy" example, but still -;; problems, e.g. delphi, false1. (Pierre) -(defvar x-symbol-hol98-token-shape '(?_ "[A-Za-z]+" . "[A-Za-z_]")) -(defvar x-symbol-hol98-table x-symbol-hol98-symbol-table) -(defun x-symbol-hol98-default-token-list (tokens) tokens) -(defvar x-symbol-hol98-token-list 'x-symbol-hol98-default-token-list) -(defvar x-symbol-hol98-input-token-ignore nil) - -;; internal stuff -(defvar x-symbol-hol98-exec-specs nil) -(defvar x-symbol-hol98-menu-alist nil) -(defvar x-symbol-hol98-grid-alist nil) -(defvar x-symbol-hol98-decode-atree nil) -(defvar x-symbol-hol98-decode-alist nil) -(defvar x-symbol-hol98-encode-alist nil) -(defvar x-symbol-hol98-nomule-decode-exec nil) -(defvar x-symbol-hol98-nomule-encode-exec nil) - -(warn "Hol98 support for X-Symbol is highly incomplete! Please help improve it! -Send improvements to x-symbol-hol98.el to proofgen@dcs.ed.ac.uk") +;; FIXME: to revitalise this, see coq/x-symbol-coq.el +(error "X-Symbol support for HOL has been removed in this release, sorry.") (provide 'x-symbol-hol98) diff --git a/lego/x-symbol-lego.el b/lego/x-symbol-lego.el index c434ac46..86f6b185 100644 --- a/lego/x-symbol-lego.el +++ b/lego/x-symbol-lego.el @@ -6,78 +6,8 @@ ;; $Id$ ;; -(defvar x-symbol-lego-symbol-table - '((longarrowright () "->" "\\") - (logicaland () "/\\" "\\") - (logicalor () "\\/" "\\") - ;; Some naughty ones, but probably what you'd like. - ;; FIXME: can we set context to prevent accidental use, - ;; e.g. searng ? - (Gamma () "Gamma" "\\") - (Delta () "Delta" "\\") - (Theta () "Theta" "\\") - (Lambda () "Lambda" "\\") - (Pi () "Pi" "\\") - (Sigma () "Sigma" "\\") - (Phi () "Phi" "\\") - (Psi () "Psi" "\\") - (Omega () "Omega" "\\") - (alpha () "alpha" "\\") - (beta () "beta" "\\") - (gamma () "gamma" "\\") - (delta () "delta" "\\") - (epsilon1 () "epsilon" "\\") - (zeta () "zeta" "\\") - (eta () "eta" "\\") - (theta1 () "theta" "\\") - (kappa1 () "kappa" "\\") - (lambda () "lambda" "\\") - ; (mu () "mu" "\\") - ; (nu () "nu" "\\") - ; (xi () "xi" "\\") - ; (pi () "pi" "\\") - (rho () "rho" "\\") - (sigma () "sigma" "\\") - (tau () "tau" "\\") - (phi1 () "phi" "\\") - ; (chi () "chi" "\\") - (psi () "psi" "\\") - (omega () "omega" "\\"))) - -;; All the stuff X-Symbol complains about -(defvar x-symbol-lego-master-directory 'ignore) -(defvar x-symbol-lego-image-searchpath '("./")) -(defvar x-symbol-lego-image-cached-dirs '("images/" "pictures/")) -(defvar x-symbol-lego-image-keywords nil) -(defvar x-symbol-lego-font-lock-keywords nil) -(defvar x-symbol-lego-header-groups-alist nil) -(defvar x-symbol-lego-class-alist - '((VALID "Lego Symbol" (x-symbol-info-face)) - (INVALID "no Lego Symbol" (red x-symbol-info-face)))) -(defvar x-symbol-lego-class-face-alist nil) -(defvar x-symbol-lego-electric-ignore nil) -(defvar x-symbol-lego-required-fonts nil) -(defvar x-symbol-lego-case-insensitive nil) -;; Setting token shape prevents "philosophy" example, but still -;; problems, e.g. delphi, false1. (Pierre) -(defvar x-symbol-lego-token-shape '(?_ "[A-Za-z]+" . "[A-Za-z_]")) -(defvar x-symbol-lego-table x-symbol-lego-symbol-table) -(defun x-symbol-lego-default-token-list (tokens) tokens) -(defvar x-symbol-lego-token-list 'x-symbol-lego-default-token-list) -(defvar x-symbol-lego-input-token-ignore nil) - -;; internal stuff -(defvar x-symbol-lego-exec-specs nil) -(defvar x-symbol-lego-menu-alist nil) -(defvar x-symbol-lego-grid-alist nil) -(defvar x-symbol-lego-decode-atree nil) -(defvar x-symbol-lego-decode-alist nil) -(defvar x-symbol-lego-encode-alist nil) -(defvar x-symbol-lego-nomule-decode-exec nil) -(defvar x-symbol-lego-nomule-encode-exec nil) - -(warn "LEGO support for X-Symbol is highly incomplete! Please help improve it! -Send improvements to x-symbol-lego.el to proofgen@dcs.ed.ac.uk") +;; FIXME: to revitalise this, see coq/x-symbol-coq.el +(error "LEGO support for X-Symbol has been removed in this release, sorry.") (provide 'x-symbol-lego) diff --git a/twelf/x-symbol-twelf.el b/twelf/x-symbol-twelf.el index 58f3fa08..a448f4d1 100644 --- a/twelf/x-symbol-twelf.el +++ b/twelf/x-symbol-twelf.el @@ -5,83 +5,8 @@ ;; $Id$ ;; -(defvar x-symbol-twelf-symbol-table - '((arrowright () "->" "\\") - (longarrowright () "0->" "\\") - (longarrowdblright () "==>" "\\") - (logicaland () "/\\" "\\") - (logicalor () "\\/" "\\") - (equivalence () "<->" "\\") - (existential1 () "EX" "\\") - (universal1 () "ALL" "\\") - (bardash () "|-" "\\") - ;; some naughty ones, but probably what you'd like - ;; (a mess in words like "searching" "philosophy" etc!!) - (Gamma () "Gamma" "\\") - (Delta () "Delta" "\\") - (Theta () "Theta" "\\") - (Lambda () "Lambda" "\\") - (Pi () "Pi" "\\") - (Sigma () "Sigma" "\\") - (Phi () "Phi" "\\") - (Psi () "Psi" "\\") - (Omega () "Omega" "\\") - (alpha () "alpha" "\\") - (beta () "beta" "\\") - (gamma () "gamma" "\\") - (delta () "delta" "\\") - (epsilon1 () "epsilon" "\\") - (zeta () "zeta" "\\") - (eta () "eta" "\\") - (theta1 () "theta" "\\") - (kappa1 () "kappa" "\\") - (lambda () "lambda" "\\") -; (mu () "mu" "\\") -; (nu () "nu" "\\") -; (xi () "xi" "\\") -; (pi () "pi" "\\") - (rho () "rho" "\\") - (sigma () "sigma" "\\") - (tau () "tau" "\\") - (phi1 () "phi" "\\") -; (chi () "chi" "\\") - (psi () "psi" "\\") - (omega () "omega" "\\"))) - -;; All the stuff X-Symbol complains about -(defvar x-symbol-twelf-master-directory 'ignore) -(defvar x-symbol-twelf-image-searchpath '("./")) -(defvar x-symbol-twelf-image-cached-dirs '("images/" "pictures/")) -(defvar x-symbol-twelf-image-keywords nil) -(defvar x-symbol-twelf-font-lock-keywords nil) -(defvar x-symbol-twelf-header-groups-alist nil) -(defvar x-symbol-twelf-class-alist - '((VALID "Twelf Symbol" (x-symbol-info-face)) - (INVALID "no Twelf Symbol" (red x-symbol-info-face)))) -(defvar x-symbol-twelf-class-face-alist nil) -(defvar x-symbol-twelf-electric-ignore nil) -(defvar x-symbol-twelf-required-fonts nil) -(defvar x-symbol-twelf-case-insensitive nil) -;; Setting token shape prevents "philosophy" example, but still -;; problems, e.g. delphi, false1. (Pierre) -(defvar x-symbol-twelf-token-shape '(?_ "[A-Za-z]+" . "[A-Za-z_]")) -(defvar x-symbol-twelf-table x-symbol-twelf-symbol-table) -(defun x-symbol-twelf-default-token-list (tokens) tokens) -(defvar x-symbol-twelf-token-list 'x-symbol-twelf-default-token-list) -(defvar x-symbol-twelf-input-token-ignore nil) - -;; internal stuff -(defvar x-symbol-twelf-exec-specs nil) -(defvar x-symbol-twelf-menu-alist nil) -(defvar x-symbol-twelf-grid-alist nil) -(defvar x-symbol-twelf-decode-atree nil) -(defvar x-symbol-twelf-decode-alist nil) -(defvar x-symbol-twelf-encode-alist nil) -(defvar x-symbol-twelf-nomule-decode-exec nil) -(defvar x-symbol-twelf-nomule-encode-exec nil) - -(warn "Twelf support for X-Symbol is highly incomplete! Please help improve it! -Send improvements to x-symbol-twelf.el to proofgen@dcs.ed.ac.uk") +;; FIXME: to revitalise this, see coq/x-symbol-coq.el +(error "X-Symbol support for Twelf has been removed in this release, sorry.") (provide 'x-symbol-twelf) -- cgit v1.2.3