From 044f48d423f2f6e33b9cf068be6ef87219ad55db Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 14 Dec 2007 14:13:22 +0000 Subject: Deleted file --- isar/x-symbol-isabelle.el | 510 ---------------------------------------------- 1 file changed, 510 deletions(-) delete mode 100644 isar/x-symbol-isabelle.el diff --git a/isar/x-symbol-isabelle.el b/isar/x-symbol-isabelle.el deleted file mode 100644 index 4411ef82..00000000 --- a/isar/x-symbol-isabelle.el +++ /dev/null @@ -1,510 +0,0 @@ -;; x-symbol-isabelle.el -;; Token language "Isabelle Symbols" for package x-symbol -;; -;; ID: $Id$ -;; Author: David von Oheimb -;; Updates by Markus Wenzel, Christoph Wedler, David Aspinall. -;; Copyright 1998 Technische Universitaet Muenchen -;; License GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; -;; NB: Part of Proof General distribution. -;; -;; This file accounts for differences between Isabelle and -;; Isabelle/Isar support of X-Symbol tokens, namely: -;; -;; Isabelle: \\ (inside ML strings) -;; Isabelle/Isar: \ -;; - -(defvar x-symbol-isabelle-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. -(defvar x-symbol-isabelle-name "Isabelle Symbol") -(defvar x-symbol-isabelle-modeline-name "isa") - -(defcustom x-symbol-isabelle-header-groups-alist nil - "*If non-nil, used in isasym specific grid/menu. -See `x-symbol-header-groups-alist'." - :group 'x-symbol-isabelle - :group 'x-symbol-input-init - :type 'x-symbol-headers) - -(defcustom x-symbol-isabelle-electric-ignore - "[:'][A-Za-z]\\|<=\\|\\[\\[\\|\\]\\]\\|~=" - "*Additional Isabelle version of `x-symbol-electric-ignore'." - :group 'x-symbol-isabelle - :group 'x-symbol-input-control - :type 'x-symbol-function-or-regexp) - - -(defvar x-symbol-isabelle-required-fonts nil - "List of features providing fonts for language `isabelle'.") - -(defvar x-symbol-isabelle-extra-menu-items nil - "Extra menu entries for language `isabelle'.") - - -(defvar x-symbol-isabelle-token-grammar - '(x-symbol-make-grammar - :encode-spec (((t . "\\\\"))) - :decode-regexp "\\\\+<[A-Za-z]+>" - :input-spec nil - :token-list x-symbol-isabelle-token-list)) - -(defun x-symbol-isabelle-token-list (tokens) - (mapcar (lambda (x) (cons x t)) tokens)) - -(defvar x-symbol-isabelle-user-table nil - "User table defining Isabelle commands, used in `x-symbol-isabelle-table'.") - -(defvar x-symbol-isabelle-generated-data nil - "Internal.") - - -;;;=========================================================================== -;;; No image support -;;;=========================================================================== - -(defvar x-symbol-isabelle-master-directory 'ignore) -(defvar x-symbol-isabelle-image-searchpath '("./")) -(defvar x-symbol-isabelle-image-cached-dirs '("images/" "pictures/")) -(defvar x-symbol-isabelle-image-file-truename-alist nil) -(defvar x-symbol-isabelle-image-keywords nil) - - -;;;=========================================================================== -;; super- and subscripts -;;;=========================================================================== - -;; one char: \<^sup>, \<^sub>, \<^isub>, and \<^isup> -;; spanning: \<^bsup>...\<^esup> and \<^bsub>..\<^esub> - -(defcustom x-symbol-isabelle-subscript-matcher 'x-symbol-isabelle-subscript-matcher - "Function matching super-/subscripts for language `isa'. -See language access `x-symbol-LANG-subscript-matcher'." - :group 'x-symbol-isabelle - :type 'function) - -(defcustom x-symbol-isabelle-font-lock-regexp "\\\\<\\^[ib]?su[bp]>" - "Regexp matching the start tag of Isabelle super- and subscripts." - :group 'x-symbol-isabelle - :type 'regexp) - -(defcustom x-symbol-isabelle-font-lock-limit-regexp "\n\\|\\\\<\\^[be]su[bp]>" - "Regexp matching the end of line and the start and end tags of Isabelle -spanning super- and subscripts." - :group 'x-symbol-isabelle - :type 'regexp) - -(defcustom x-symbol-isabelle-font-lock-contents-regexp "." - "*Regexp matching the spanning super- and subscript contents. -This regexp should match the text between the opening and closing super- -or subscript tag." - :group 'x-symbol-isabelle - :type 'regexp) - - -;; the [\350-\357].\350\\|\^A[A-H].\^AA part is there to enable single -;; char sub/super scripts with coloured Isabelle output. -(defcustom x-symbol-isabelle-single-char-regexp - "\\([^\\]\\|\\\\<[A-Za-z]+>\\)\\|[\350-\357]\\([^\\]\\|\\\\<[A-Za-z]+>\\)\350\\|\^A[A-H]\\([^\\]\\|\\\\<[A-Za-z]+>\\)\^AA" - "Return regexp matching \ or c for some char c." - :group 'x-symbol-isabelle - :type 'regexp) - -(defun x-symbol-isabelle-subscript-matcher (limit) - (block nil - (let (open-beg open-end close-end close-beg script-type) - (while (re-search-forward x-symbol-isabelle-font-lock-regexp limit t) - (setq open-beg (match-beginning 0) - open-end (match-end 0) - script-type (if (eq (char-after (- open-end 2)) ?b) - 'x-symbol-sub-face - 'x-symbol-sup-face)) - (when (not (proof-string-match "[ \t\n]" (string (char-after open-end)))) - (if (eq (char-after (- open-end 5)) ?b) ; if is spanning sup-/subscript - (let ((depth 1)) ; level of nesting - (while (and (not (eq depth 0)) - (re-search-forward x-symbol-isabelle-font-lock-limit-regexp - limit 'limit)) - (setq close-beg (match-beginning 0) - close-end (match-end 0)) - (if (eq (char-after (- close-end 1)) ?\n) ; if eol - (setq depth 0) - (if (eq (char-after (- close-end 5)) ?b) ; if end of span - (setq depth (+ depth 1)) - (setq depth (- depth 1))))) - (when (eq depth 0) - (when - (save-excursion - (goto-char open-end) - (re-search-forward x-symbol-isabelle-font-lock-contents-regexp - close-beg t)) - (store-match-data (list open-beg close-end - open-beg open-end - open-end close-beg - close-beg close-end)) - (return script-type))) - (goto-char close-beg)) - (when (re-search-forward x-symbol-isabelle-single-char-regexp - limit 'limit) - (setq close-end (match-end 0)) - (store-match-data (list open-beg close-end - open-beg open-end - open-end close-end)) - (return script-type)))))))) - -(defun isabelle-match-subscript (limit) - (if (proof-ass x-symbol-enable) - (setq x-symbol-isabelle-subscript-type - (funcall x-symbol-isabelle-subscript-matcher limit)))) - -;; these are used for Isabelle output only. x-symbol does its own -;; setup of font-lock-keywords for the theory buffer -;; (x-symbol-isabelle-font-lock-keywords does not belong to language -;; access any more) -(defvar x-symbol-isabelle-font-lock-keywords - '((isabelle-match-subscript - (1 x-symbol-invisible-face t) - (2 (progn x-symbol-isabelle-subscript-type) prepend) - (3 x-symbol-invisible-face t t))) - "Isabelle font-lock keywords for super- and subscripts.") - -(defvar x-symbol-isabelle-font-lock-allowed-faces t) - - -;;;=========================================================================== -;;; Charsym Info -;;;=========================================================================== - -(defcustom x-symbol-isabelle-class-alist - '((VALID "Isabelle Symbol" (x-symbol-info-face)) - (INVALID "no Isabelle Symbol" (red x-symbol-info-face))) - "Alist for Isabelle'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 [causes compile error] - :type 'x-symbol-class-info) - - -(defcustom x-symbol-isabelle-class-face-alist nil - "Alist for Isabelle's color scheme in TeXinfo's grid and info. -See `x-symbol-language-access-alist' for details." - :group 'x-symbol-isabelle - :group 'x-symbol-input-init - :group 'x-symbol-info-general -;; :set 'x-symbol-set-cache-variable [causes compile error] - :type 'x-symbol-class-faces) - - - -;;;=========================================================================== -;;; The tables -;;;=========================================================================== - -(defvar x-symbol-isabelle-case-insensitive nil) -(defvar x-symbol-isabelle-token-shape nil) -(defvar x-symbol-isabelle-input-token-ignore nil) -(defvar x-symbol-isabelle-token-list 'identity) - -(defvar x-symbol-isabelle-symbol-table ; symbols (isabelle font) - '((visiblespace "\\") - (Gamma "\\") - (Delta "\\") - (Theta "\\") - (Lambda "\\") - (Pi "\\") - (Sigma "\\") - (Phi "\\") - (Psi "\\") - (Omega "\\") - (alpha "\\") - (beta "\\") - (gamma "\\") - (delta "\\") - (epsilon1 "\\") - (zeta "\\") - (eta "\\") - (theta "\\") - (kappa1 "\\") - (lambda "\\") - (mu "\\") - (nu "\\") - (xi "\\") - (pi "\\") - (rho1 "\\") - (sigma "\\") - (tau "\\") - (phi1 "\\") - (chi "\\") - (psi "\\") - (omega "\\") - (notsign "\\") - (logicaland "\\") - (logicalor "\\") - (universal1 "\\") - (existential1 "\\") - (epsilon "\\") - (biglogicaland "\\") - (ceilingleft "\\") - (ceilingright "\\") - (floorleft "\\") - (floorright "\\") - (bardash "\\") - (bardashdbl "\\") - (semanticsleft "\\") - (semanticsright "\\") - (periodcentered "\\") - (element "\\") - (reflexsubset "\\") - (intersection "\\") - (union "\\") - (bigintersection "\\") - (bigunion "\\") - (sqintersection "\\") - (squnion "\\") - (bigsqintersection "\\") - (bigsqunion "\\") - (perpendicular "\\") - (dotequal "\\") - (wrong "\\") - (equivalence "\\") - (notequal "\\") - (propersqsubset "\\") - (reflexsqsubset "\\") - (properprec "\\") - (reflexprec "\\") - (propersucc "\\") - (approxequal "\\") - (similar "\\") - (simequal "\\") - (lessequal "\\") - (coloncolon "\\") - (arrowleft "\\") - (endash "\\") - (arrowright "\\") - (arrowdblleft "\\") -; (nil "\\") - (arrowdblright "\\") - (frown "\\") - (mapsto "\\") - (leadsto "\\") - (arrowup "\\") - (arrowdown "\\") - (notelement "\\") - (multiply "\\") - (circleplus "\\") - (circleminus "\\") - (circlemultiply "\\") - (circleslash "\\") - (propersubset "\\") - (infinity "\\") - (box "\\") - (lozenge1 "\\") - (circ "\\") - (bullet "\\") - (bardbl "\\") - (radical "\\") - (copyright "\\"))) - -(defvar x-symbol-isabelle-xsymbol-table ; xsymbols - '((Xi "\\") - (Upsilon1 "\\") - (iota "\\") - (upsilon "\\") - (plusminus "\\") - (division "\\
") - (longarrowright "\\") - (longarrowleft "\\") - (longarrowboth "\\") - (longarrowdblright "\\") - (longarrowdblleft "\\") - (longarrowdblboth "\\") - (brokenbar "\\") - (hyphen "\\") - (macron "\\") - (exclamdown "\\") - (questiondown "\\") - (guillemotleft "\\") - (guillemotright "\\") - (degree "\\") - (onesuperior "\\") - (onequarter "\\") - (twosuperior "\\") - (onehalf "\\") - (threesuperior "\\") - (threequarters "\\") - (paragraph "\\") - (registered "\\") - (ordfeminine "\\") - (masculine "\\") - (section "\\
") - (sterling "\\") - (yen "\\") - (cent "\\") - (currency "\\") - (braceleft2 "\\") - (braceright2 "\\") - (top "\\") - (congruent "\\") - (club "\\") - (diamond "\\") - (heart "\\") - (spade "\\") - (arrowboth "\\") - (greaterequal "\\") - (proportional "\\") - (partialdiff "\\") - (ellipsis "\\") - (aleph "\\") - (Ifraktur "\\") - (Rfraktur "\\") - (weierstrass "\\") - (emptyset "\\") - (angle "\\") - (gradient "\\") - (product "\\") - (arrowdblboth "\\") - (arrowdblup "\\") - (arrowdbldown "\\") - (angleleft "\\") - (angleright "\\") - (summation "\\") - (integral "\\") - (circleintegral "\\") - (dagger "\\") - (sharp "\\") - (star "\\") - (smltriangleright "\\") - (triangleleft "\\") - (triangle "\\") - (triangleright "\\") - (trianglelefteq "\\") - (trianglerighteq "\\") - (smltriangleleft "\\") - (natural "\\") - (flat "\\") - (amalg "\\") - (Mho "\\") - (arrowupdown "\\") - (longmapsto "\\") - (arrowdblupdown "\\") - (hookleftarrow "\\") - (hookrightarrow "\\") - (rightleftharpoons "\\") - (leftharpoondown "\\") - (rightharpoondown "\\") - (leftharpoonup "\\") - (rightharpoonup "\\") - (asym "\\") - (minusplus "\\") - (bowtie "\\") - (centraldots "\\") - (circledot "\\") - (propersuperset "\\") - (reflexsuperset "\\") - (propersqsuperset "\\") - (reflexsqsuperset "\\") - (lessless "\\") - (greatergreater "\\") - (unionplus "\\") - (backslash3 "\\") - (smile "\\") - (reflexsucc "\\") - (dashbar "\\") - (biglogicalor "\\") - (bigunionplus "\\") - (daggerdbl "\\") - (bigbowtie "\\") - (booleans "\\") - (complexnums "\\") - (natnums "\\") - (rationalnums "\\") - (realnums "\\") - (integers "\\") - (lesssim "\\") - (greatersim "\\") - (lessapprox "\\") - (greaterapprox "\\") - (definedas "\\") - (cataleft "\\") - (cataright "\\") - (bigcircledot "\\") - (bigcirclemultiply "\\") - (bigcircleplus "\\") - (coproduct "\\") - (cedilla "\\") - (diaeresis "\\") - (acute "\\") - (hungarumlaut "\\") - (lozenge "\\") - (smllozenge "\\") - (dotlessi "\\") - (euro "\\") - (zero1 "\\") - (one1 "\\") - (two1 "\\") - (three1 "\\") - (four1 "\\") - (five1 "\\") - (six1 "\\") - (seven1 "\\") - (eight1 "\\") - (nine1 "\\") - )) - -(defun x-symbol-isabelle-prepare-table (table) - "Prepare table for Isabelle/Isar." - (mapcar (lambda (entry) - (list (car entry) nil - (cadr entry) - (concat "\\" (cadr entry)))) - table)) - -(defvar x-symbol-isabelle-table - (x-symbol-isabelle-prepare-table - (append - x-symbol-isabelle-user-table - x-symbol-isabelle-symbol-table - x-symbol-isabelle-xsymbol-table))) - - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; -;; User-level settings for X-Symbol -;; -;; this is MODE-ON CODING 8BITS UNIQUE SUBSCRIPTS IMAGE -(defcustom x-symbol-isabelle-auto-style - '((proof-ass 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 - t ;; x-symbol-subscripts - nil) ;; x-symbol-image - "Variable used to document a language access. -See documentation of `x-symbol-auto-style'." - :group 'x-symbol-isabelle - :group 'x-symbol-mode - :type 'x-symbol-auto-style) - -;; FIXME da: is this needed? -(defcustom x-symbol-isabelle-auto-coding-alist nil - "*Alist used to determine the file coding of ISABELLE buffers. -Used in the default value of `x-symbol-auto-mode-alist'. See -variable `x-symbol-auto-coding-alist' for details." - :group 'x-symbol-isabelle - :group 'x-symbol-mode - :type 'x-symbol-auto-coding) - - - - -(provide 'x-symbol-isabelle) -- cgit v1.2.3