(1) (file-mode-spec/warning) Error in File mode specification: Wrong type argument: consp, latin-iso8859-2 Backtrace follows: specifier-matching-instance(# latin-iso8859-2 nil nil t) # bind (value no-fallback default domain matchspec property face) face-property-matching-instance(default font latin-iso8859-2 nil nil t) (and (null x-symbol-mule-change-default-face) (face-property-matching-instance (quote default) (quote font) (or (car left) (car right)) nil nil t)) (or default (null first) noninteractive (not (fboundp (quote face-property-matching-instance))) (and (null x-symbol-mule-change-default-face) (face-property-matching-instance (quote default) (quote font) (or (car left) (car right)) nil nil t)) (let ((origfont (x-symbol-mule-default-font))) (set-face-property (quote default) (quote font) first nil (quote (mule-fonts)) (quote prepend)) (set-face-property (quote default) (quote font) origfont))) # bind (right left registry default) (let ((default (eq (x-symbol-cset-coding cset) (or x-symbol-default-coding (quote iso-8859-1)))) (registry (x-symbol-cset-registry cset)) (left (x-symbol-cset-left cset)) (right (x-symbol-cset-right cset))) (x-symbol-mule-make-charset left 0 registry) (x-symbol-mule-make-charset right 1 registry) (or default (null first) noninteractive (not (fboundp (quote face-property-matching-instance))) (and (null x-symbol-mule-change-default-face) (face-property-matching-instance (quote default) (quote font) (or (car left) (car right)) nil nil t)) (let ((origfont (x-symbol-mule-default-font))) (set-face-property (quote default) (quote font) first nil (quote (mule-fonts)) (quote prepend)) (set-face-property (quote default) (quote font) origfont))) (if noninteractive (list nil) (let ((faces (quote (x-symbol-face x-symbol-sub-face x-symbol-sup-face))) (docstrings x-symbol-face-docstrings) (raise 0) font) (while faces (when (setq font (x-symbol-try-font-name (car fonts) raise)) (make-face (car faces) (car docstrings)) (x-symbol-set-face-font (car faces) font (list (car left) (car right)) default)) (setq fonts (cdr fonts) raise (1+ raise) faces (cdr faces) docstrings (cdr docstrings)))) (if first (quote (x-symbol-face)) (quote (default))))) (if (or first (and x-symbol-latin-force-use (x-symbol-cset-coding cset)) (and (find-charset (car (x-symbol-cset-left cset))) (find-charset (car (x-symbol-cset-right cset))))) (let ((default (eq (x-symbol-cset-coding cset) (or x-symbol-default-coding (quote iso-8859-1)))) (registry (x-symbol-cset-registry cset)) (left (x-symbol-cset-left cset)) (right (x-symbol-cset-right cset))) (x-symbol-mule-make-charset left 0 registry) (x-symbol-mule-make-charset right 1 registry) (or default (null first) noninteractive (not (fboundp (quote face-property-matching-instance))) (and (null x-symbol-mule-change-default-face) (face-property-matching-instance (quote default) (quote font) (or (car left) (car right)) nil nil t)) (let ((origfont (x-symbol-mule-default-font))) (set-face-property (quote default) (quote font) first nil (quote (mule-fonts)) (quote prepend)) (set-face-property (quote default) (quote font) origfont))) (if noninteractive (list nil) (let ((faces (quote (x-symbol-face x-symbol-sub-face x-symbol-sup-face))) (docstrings x-symbol-face-docstrings) (raise 0) font) (while faces (when (setq font (x-symbol-try-font-name (car fonts) raise)) (make-face (car faces) (car docstrings)) (x-symbol-set-face-font (car faces) font (list (car left) (car right)) default)) (setq fonts (cdr fonts) raise (1+ raise) faces (cdr faces) docstrings (cdr docstrings)))) (if first (quote (x-symbol-face)) (quote (default)))))) (when (or first (and x-symbol-latin-force-use (x-symbol-cset-coding cset)) (and (find-charset (car (x-symbol-cset-left cset))) (find-charset (car (x-symbol-cset-right cset))))) (let ((default (eq (x-symbol-cset-coding cset) (or x-symbol-default-coding (quote iso-8859-1)))) (registry (x-symbol-cset-registry cset)) (left (x-symbol-cset-left cset)) (right (x-symbol-cset-right cset))) (x-symbol-mule-make-charset left 0 registry) (x-symbol-mule-make-charset right 1 registry) (or default (null first) noninteractive (not (fboundp (quote face-property-matching-instance))) (and (null x-symbol-mule-change-default-face) (face-property-matching-instance (quote default) (quote font) (or (car left) (car right)) nil nil t)) (let ((origfont (x-symbol-mule-default-font))) (set-face-property (quote default) (quote font) first nil (quote (mule-fonts)) (quote prepend)) (set-face-property (quote default) (quote font) origfont))) (if noninteractive (list nil) (let ((faces (quote (x-symbol-face x-symbol-sub-face x-symbol-sup-face))) (docstrings x-symbol-face-docstrings) (raise 0) font) (while faces (when (setq font (x-symbol-try-font-name (car fonts) raise)) (make-face (car faces) (car docstrings)) (x-symbol-set-face-font (car faces) font (list (car left) (car right)) default)) (setq fonts (cdr fonts) raise (1+ raise) faces (cdr faces) docstrings (cdr docstrings)))) (if first (quote (x-symbol-face)) (quote (default)))))) # bind (first) (let ((first (if noninteractive (caar fonts) (x-symbol-try-font-name (car fonts))))) (when (or first (and x-symbol-latin-force-use (x-symbol-cset-coding cset)) (and (find-charset (car (x-symbol-cset-left cset))) (find-charset (car (x-symbol-cset-right cset))))) (let ((default (eq (x-symbol-cset-coding cset) (or x-symbol-default-coding (quote iso-8859-1)))) (registry (x-symbol-cset-registry cset)) (left (x-symbol-cset-left cset)) (right (x-symbol-cset-right cset))) (x-symbol-mule-make-charset left 0 registry) (x-symbol-mule-make-charset right 1 registry) (or default (null first) noninteractive (not (fboundp (quote face-property-matching-instance))) (and (null x-symbol-mule-change-default-face) (face-property-matching-instance (quote default) (quote font) (or (car left) (car right)) nil nil t)) (let ((origfont (x-symbol-mule-default-font))) (set-face-property (quote default) (quote font) first nil (quote (mule-fonts)) (quote prepend)) (set-face-property (quote default) (quote font) origfont))) (if noninteractive (list nil) (let ((faces (quote (x-symbol-face x-symbol-sub-face x-symbol-sup-face))) (docstrings x-symbol-face-docstrings) (raise 0) font) (while faces (when (setq font (x-symbol-try-font-name (car fonts) raise)) (make-face (car faces) (car docstrings)) (x-symbol-set-face-font (car faces) font (list (car left) (car right)) default)) (setq fonts (cdr fonts) raise (1+ raise) faces (cdr faces) docstrings (cdr docstrings)))) (if first (quote (x-symbol-face)) (quote (default))))))) # bind (fonts cset) x-symbol-make-cset(((("iso8859-2" . iso-8859-2) ?\^Þ -3750) nil latin-iso8859-2) (("-adobe-helvetica%s-medium-r-normal-*-%d-*-*-*-*-*-iso8859-2" "-etl-fixed%s-medium-r-normal--%d-%d0-72-72-c-*-iso8859-2") ("-adobe-helvetica%s-medium-r-normal-*-%d-*-*-*-*-*-iso8859-2" "-etl-fixed%s-medium-r-normal--%d-%d0-72-72-c-*-iso8859-2") ("-adobe-helvetica%s-medium-r-normal-*-%d-*-*-*-*-*-iso8859-2" "-etl-fixed%s-medium-r-normal--%d-%d0-72-72-c-*-iso8859-2"))) (let* ((faces (x-symbol-make-cset cset (if (stringp (car fonts)) (list fonts fonts fonts) fonts))) (cset-score (x-symbol-cset-score cset)) (coding (x-symbol-cset-coding cset)) (force-use (or x-symbol-latin-force-use (eq (or x-symbol-default-coding (quote iso-8859-1)) coding))) new-charsyms) (unless faces (when fonts (warn (if (and coding force-use) "X-Symbol characters with registry %S will look strange" "X-Symbol characters with registry %S are not used") (x-symbol-cset-registry cset)))) (dolist (entry table) (let ((charsym (car entry)) definition) (if (or faces (and coding force-use)) (x-symbol-make-char cset (cadr entry) charsym (car faces) coding)) (set (intern (symbol-name charsym) x-symbol-charsym-decode-obarray) (list charsym)) (if (memq (cddr entry) (quote (t unused))) (if coding (if (x-symbol-charsym-defined-p charsym) (if (eq (cddr entry) (quote unused)) (warn "X-Symbol charsym %s: redefinition as unused" charsym)) (if (eq (cddr entry) (quote unused)) (push charsym new-charsyms) (warn "X-Symbol charsym %s: alias without definition" charsym))) (warn "X-Symbol charsym %s: alias or unused without coding system" charsym)) (if (x-symbol-charsym-defined-p charsym) (progn (warn "X-Symbol charsym %s: redefinition (not used)" charsym) (or (assq charsym new-charsyms) (assq charsym x-symbol-all-charsyms) (push charsym new-charsyms))) (push charsym new-charsyms) (setq definition (cddr (or (assq charsym x-symbol-user-table) entry))) (when (x-symbol-table-junk definition) (warn "X-Symbol charsym %s: unused elements in definition" charsym)) (x-symbol-init-charsym-command charsym) (x-symbol-init-charsym-input charsym (x-symbol-table-grouping definition) (x-symbol-table-score definition) cset-score (x-symbol-table-input definition) (x-symbol-table-prefixes definition)) (x-symbol-init-charsym-aspects charsym (x-symbol-table-aspects definition)))))) (x-symbol-init-charsym-syntax new-charsyms) (setq x-symbol-all-charsyms (nconc x-symbol-all-charsyms (nreverse new-charsyms)))) # bind (table fonts cset) x-symbol-init-cset(((("iso8859-2" . iso-8859-2) ?\^Þ -3750) nil latin-iso8859-2) ("-adobe-helvetica%s-medium-r-normal-*-%d-*-*-*-*-*-iso8859-2" "-etl-fixed%s-medium-r-normal--%d-%d0-72-72-c-*-iso8859-2") ((nobreakspace 160 . t) (Aogonek 161 (ogonek "A" aogonek)) (breve 162 (breve accent)) (Lslash 163 (slash "L" lslash)) (currency 164 . t) (Lcaron 165 (caron "L" lcaron)) (Sacute 166 (acute "S" sacute)) (section 167 . t) (diaeresis 168 . t) (Scaron 169 (caron "S" scaron)) (Scedilla 170 (cedilla "S" scedilla)) (Tcaron 171 (caron "T" tcaron)) (Zacute 172 (acute "Z" zacute)) (hyphen 173 . t) (Zcaron 174 (caron "Z" zcaron)) (Zdotaccent 175 (dotaccent "Z" zdotaccent)) (degree 176 . t) (aogonek 177 (ogonek "a" Aogonek)) (ogonek 178 (ogonek accent)) (lslash 179 (slash "l" Lslash)) (acute 180 . t) (lcaron 181 (caron "l" Lcaron)) (sacute 182 (acute "s" Sacute)) (caron 183 (caron accent) (shift up)) (cedilla 184 . t) (scaron 185 (caron "s" Scaron)) (scedilla 186 (cedilla "s" Scedilla)) (tcaron 187 (caron "t" Tcaron)) (zacute 188 (acute "z" Zacute)) (hungarumlaut 189 (hungarumlaut accent)) (zcaron 190 (caron "z" Zcaron)) (zdotaccent 191 (dotaccent "z" Zdotaccent)) (Racute 192 (acute "R" racute)) (Aacute 193 . t) (Acircumflex 194 . t) (Abreve 195 (breve "A" abreve)) (Adiaeresis 196 . t) (Lacute 197 (acute "L" lacute)) (Cacute 198 (acute "C" cacute)) (Ccedilla 199 . t) (Ccaron 200 (caron "C" ccaron)) (Eacute 201 . t) (Eogonek 202 (ogonek "E" eogonek)) (Ediaeresis 203 . t) (Ecaron 204 (caron "E" ecaron)) (Iacute 205 . t) (Icircumflex 206 . t) (Dcaron 207 (caron "D" dcaron)) (Dbar 208 (slash "D" dbar)) (Nacute 209 (acute "N" nacute)) (Ncaron 210 (caron "N" ncaron)) (Oacute 211 . t) (Ocircumflex 212 . t) (Ohungarumlaut 213 (hungarumlaut "O" ohungarumlaut)) (Odiaeresis 214 . t) (multiply 215 . t) (Rcaron 216 (caron "R" rcaron)) (Uring 217 (ring "U" uring)) (Uacute 218 . t) (Uhungarumlaut 219 (hungarumlaut "U" uhungarumlaut)) (Udiaeresis 220 . t) (Yacute 221 . t) (Tcedilla 222 (cedilla "T" tcedilla)) (ssharp 223 . t) (racute 224 (acute "r" Racute)) (aacute 225 . t) (acircumflex 226 . t) (abreve 227 (breve "a" Abreve)) (adiaeresis 228 . t) (lacute 229 (acute "l" Lacute)) (cacute 230 (acute "c" Cacute)) (ccedilla 231 . t) (ccaron 232 (caron "c" Ccaron)) (eacute 233 . t) (eogonek 234 (ogonek "e" Eogonek)) (ediaeresis 235 . t) (ecaron 236 (caron "e" Ecaron)) (iacute 237 . t) (icircumflex 238 . t) (dcaron 239 (caron "d" Dcaron)) (dbar 240 (slash "d" Dbar)) (nacute 241 (acute "n" Nacute)) (ncaron 242 (caron "n" Ncaron)) (oacute 243 . t) (ocircumflex 244 . t) (ohungarumlaut 245 (hungarumlaut "o" Ohungarumlaut)) (odiaeresis 246 . t) (division 247 . t) (rcaron 248 (caron "r" Rcaron)) (uring 249 (ring "u" Uring)) (uacute 250 . t) (uhungarumlaut 251 (hungarumlaut "u" Uhungarumlaut)) (udiaeresis 252 . t) (yacute 253 . t) (tcedilla 254 (cedilla "t" Tcedilla)) (dotaccent 255 (dotaccent accent) (shift up)))) (if noninteractive nil (x-symbol-initialize) (setq x-symbol-all-charsyms nil) (cond ((not (console-type)) (unless x-symbol-default-coding (warn "X-Symbol: only limited support on a console")) (unless (eq x-symbol-latin-force-use (quote console-user)) (setq x-symbol-latin1-fonts nil) (setq x-symbol-latin2-fonts nil) (setq x-symbol-latin3-fonts nil) (setq x-symbol-latin5-fonts nil) (setq x-symbol-latin9-fonts nil) (setq x-symbol-xsymb0-fonts nil) (setq x-symbol-xsymb1-fonts nil))) (x-symbol-use-unicode (require (quote x-symbol-unicode)) (setq x-symbol-latin1-fonts nil) (setq x-symbol-latin2-fonts nil) (setq x-symbol-latin3-fonts nil) (setq x-symbol-latin5-fonts nil) (setq x-symbol-latin9-fonts nil) (setq x-symbol-xsymb0-fonts nil) (setq x-symbol-xsymb1-fonts nil))) (if (eq window-system (quote mac)) (x-symbol-mac-setup1)) (x-symbol-init-cset x-symbol-latin1-cset x-symbol-latin1-fonts x-symbol-latin1-table) (x-symbol-init-cset x-symbol-latin2-cset x-symbol-latin2-fonts x-symbol-latin2-table) (x-symbol-init-cset x-symbol-latin3-cset x-symbol-latin3-fonts x-symbol-latin3-table) (x-symbol-init-cset x-symbol-latin5-cset x-symbol-latin5-fonts x-symbol-latin5-table) (x-symbol-init-cset x-symbol-latin9-cset x-symbol-latin9-fonts x-symbol-latin9-table) (x-symbol-init-latin-decoding) (x-symbol-init-cset x-symbol-xsymb0-cset x-symbol-xsymb0-fonts x-symbol-xsymb0-table) (x-symbol-init-cset x-symbol-xsymb1-cset x-symbol-xsymb1-fonts x-symbol-xsymb1-table) (if (eq window-system (quote mac)) (x-symbol-mac-setup2))) (unless noninteractive (x-symbol-initialize) (setq x-symbol-all-charsyms nil) (cond ((not (console-type)) (unless x-symbol-default-coding (warn "X-Symbol: only limited support on a console")) (unless (eq x-symbol-latin-force-use (quote console-user)) (setq x-symbol-latin1-fonts nil) (setq x-symbol-latin2-fonts nil) (setq x-symbol-latin3-fonts nil) (setq x-symbol-latin5-fonts nil) (setq x-symbol-latin9-fonts nil) (setq x-symbol-xsymb0-fonts nil) (setq x-symbol-xsymb1-fonts nil))) (x-symbol-use-unicode (require (quote x-symbol-unicode)) (setq x-symbol-latin1-fonts nil) (setq x-symbol-latin2-fonts nil) (setq x-symbol-latin3-fonts nil) (setq x-symbol-latin5-fonts nil) (setq x-symbol-latin9-fonts nil) (setq x-symbol-xsymb0-fonts nil) (setq x-symbol-xsymb1-fonts nil))) (if (eq window-system (quote mac)) (x-symbol-mac-setup1)) (x-symbol-init-cset x-symbol-latin1-cset x-symbol-latin1-fonts x-symbol-latin1-table) (x-symbol-init-cset x-symbol-latin2-cset x-symbol-latin2-fonts x-symbol-latin2-table) (x-symbol-init-cset x-symbol-latin3-cset x-symbol-latin3-fonts x-symbol-latin3-table) (x-symbol-init-cset x-symbol-latin5-cset x-symbol-latin5-fonts x-symbol-latin5-table) (x-symbol-init-cset x-symbol-latin9-cset x-symbol-latin9-fonts x-symbol-latin9-table) (x-symbol-init-latin-decoding) (x-symbol-init-cset x-symbol-xsymb0-cset x-symbol-xsymb0-fonts x-symbol-xsymb0-table) (x-symbol-init-cset x-symbol-xsymb1-cset x-symbol-xsymb1-fonts x-symbol-xsymb1-table) (if (eq window-system (quote mac)) (x-symbol-mac-setup2))) # (unwind-protect ...) # (unwind-protect ...) # (unwind-protect ...) # (unwind-protect ...) # (unwind-protect ...) # (unwind-protect ...) # (unwind-protect ...) # (unwind-protect ...) load-internal("x-symbol" nil require nil undecided) # bind (path handler filename nosuffix nomessage noerror file) load("x-symbol" nil require nil) # (unwind-protect ...) require(x-symbol) # (condition-case ... . ((file-error nil))) (condition-case nil (require symbol) (file-error nil)) # bind (symbol) proof-try-require(x-symbol) (not (proof-try-require (quote x-symbol))) (and (not (featurep (quote x-symbol))) (not (proof-try-require (quote x-symbol)))) (cond ((and (not (featurep (quote x-symbol))) (not (proof-try-require (quote x-symbol)))) (funcall error-or-warn "Proof General: x-symbol package must be installed for x-symbol-support!\nThe package is available at http://x-symbol.sourceforge.net/")) ((not (pg-window-system)) (funcall error-or-warn "Proof General: x-symbol package only runs under a window system!")) ((or (not (fboundp (quote x-symbol-initialize))) (not (fboundp (quote x-symbol-register-language)))) (funcall error-or-warn "Proof General: x-symbol package installation faulty!")) ((not (proof-try-require (intern (proof-x-symbol-tokenlang-file)))) (funcall error-or-warn (format "Proof General: for x-symbol support, you must provide a library %s.el" xs-feature))) (t (require (quote x-symbol-vars)) (let* ((xs-xtra-modes proof-xsym-extra-modes) (xs-std-modes (list (or proof-mode-for-shell (intern (concat assistant "-shell-mode"))) (or proof-mode-for-response (intern (concat assistant "-response-mode"))) (or proof-mode-for-script (intern (concat assistant "-proofscript-mode"))) (or proof-mode-for-goals (intern (concat assistant "-goals-mode"))))) (all-xs-modes (append xs-std-modes xs-xtra-modes)) (am-entry (list proof-xsym-extra-modes t (backquote (quote (\, xs-lang))))) (symmode-nm (concat xs-lang-name "sym-mode")) (symmode (intern symmode-nm)) (symnamevar (intern (concat xs-feature "-name"))) (symname (concat (capitalize xs-lang-name) " Symbols")) (symmodelinevar (intern (concat xs-feature "-modeline-name"))) (symmodelinenm xs-lang-name) (flks proof-xsym-font-lock-keywords)) (x-symbol-initialize) (set symnamevar symname) (set symmodelinevar symmodelinenm) (x-symbol-register-language xs-lang xs-feature-sym all-xs-modes) (if flks (put symmode (quote font-lock-defaults) (list flks))) (setq proof-x-symbol-initialized t)))) # bind (error-or-warn xs-feature-sym xs-feature xs-lang-name xs-lang) (let* ((xs-lang (proof-ass x-symbol-language)) (xs-lang-name (symbol-name xs-lang)) (xs-feature (concat "x-symbol-" xs-lang-name)) (xs-feature-sym (intern xs-feature)) (error-or-warn (lambda (str) (progn (if error (error str) (warn str)))))) (cond ((and (not (featurep (quote x-symbol))) (not (proof-try-require (quote x-symbol)))) (funcall error-or-warn "Proof General: x-symbol package must be installed for x-symbol-support!\nThe package is available at http://x-symbol.sourceforge.net/")) ((not (pg-window-system)) (funcall error-or-warn "Proof General: x-symbol package only runs under a window system!")) ((or (not (fboundp (quote x-symbol-initialize))) (not (fboundp (quote x-symbol-register-language)))) (funcall error-or-warn "Proof General: x-symbol package installation faulty!")) ((not (proof-try-require (intern (proof-x-symbol-tokenlang-file)))) (funcall error-or-warn (format "Proof General: for x-symbol support, you must provide a library %s.el" xs-feature))) (t (require (quote x-symbol-vars)) (let* ((xs-xtra-modes proof-xsym-extra-modes) (xs-std-modes (list (or proof-mode-for-shell (intern (concat assistant "-shell-mode"))) (or proof-mode-for-response (intern (concat assistant "-response-mode"))) (or proof-mode-for-script (intern (concat assistant "-proofscript-mode"))) (or proof-mode-for-goals (intern (concat assistant "-goals-mode"))))) (all-xs-modes (append xs-std-modes xs-xtra-modes)) (am-entry (list proof-xsym-extra-modes t (backquote (quote (\, xs-lang))))) (symmode-nm (concat xs-lang-name "sym-mode")) (symmode (intern symmode-nm)) (symnamevar (intern (concat xs-feature "-name"))) (symname (concat (capitalize xs-lang-name) " Symbols")) (symmodelinevar (intern (concat xs-feature "-modeline-name"))) (symmodelinenm xs-lang-name) (flks proof-xsym-font-lock-keywords)) (x-symbol-initialize) (set symnamevar symname) (set symmodelinevar symmodelinenm) (x-symbol-register-language xs-lang xs-feature-sym all-xs-modes) (if flks (put symmode (quote font-lock-defaults) (list flks))) (setq proof-x-symbol-initialized t))))) (if (or proof-x-symbol-initialized (not (proof-x-symbol-support-maybe-available))) nil (let* ((xs-lang (proof-ass x-symbol-language)) (xs-lang-name (symbol-name xs-lang)) (xs-feature (concat "x-symbol-" xs-lang-name)) (xs-feature-sym (intern xs-feature)) (error-or-warn (lambda (str) (progn (if error (error str) (warn str)))))) (cond ((and (not (featurep (quote x-symbol))) (not (proof-try-require (quote x-symbol)))) (funcall error-or-warn "Proof General: x-symbol package must be installed for x-symbol-support!\nThe package is available at http://x-symbol.sourceforge.net/")) ((not (pg-window-system)) (funcall error-or-warn "Proof General: x-symbol package only runs under a window system!")) ((or (not (fboundp (quote x-symbol-initialize))) (not (fboundp (quote x-symbol-register-language)))) (funcall error-or-warn "Proof General: x-symbol package installation faulty!")) ((not (proof-try-require (intern (proof-x-symbol-tokenlang-file)))) (funcall error-or-warn (format "Proof General: for x-symbol support, you must provide a library %s.el" xs-feature))) (t (require (quote x-symbol-vars)) (let* ((xs-xtra-modes proof-xsym-extra-modes) (xs-std-modes (list (or proof-mode-for-shell (intern (concat assistant "-shell-mode"))) (or proof-mode-for-response (intern (concat assistant "-response-mode"))) (or proof-mode-for-script (intern (concat assistant "-proofscript-mode"))) (or proof-mode-for-goals (intern (concat assistant "-goals-mode"))))) (all-xs-modes (append xs-std-modes xs-xtra-modes)) (am-entry (list proof-xsym-extra-modes t (backquote (quote (\, xs-lang))))) (symmode-nm (concat xs-lang-name "sym-mode")) (symmode (intern symmode-nm)) (symnamevar (intern (concat xs-feature "-name"))) (symname (concat (capitalize xs-lang-name) " Symbols")) (symmodelinevar (intern (concat xs-feature "-modeline-name"))) (symmodelinenm xs-lang-name) (flks proof-xsym-font-lock-keywords)) (x-symbol-initialize) (set symnamevar symname) (set symmodelinevar symmodelinenm) (x-symbol-register-language xs-lang xs-feature-sym all-xs-modes) (if flks (put symmode (quote font-lock-defaults) (list flks))) (setq proof-x-symbol-initialized t)))))) (unless (or proof-x-symbol-initialized (not (proof-x-symbol-support-maybe-available))) (let* ((xs-lang (proof-ass x-symbol-language)) (xs-lang-name (symbol-name xs-lang)) (xs-feature (concat "x-symbol-" xs-lang-name)) (xs-feature-sym (intern xs-feature)) (error-or-warn (lambda (str) (progn (if error (error str) (warn str)))))) (cond ((and (not (featurep (quote x-symbol))) (not (proof-try-require (quote x-symbol)))) (funcall error-or-warn "Proof General: x-symbol package must be installed for x-symbol-support!\nThe package is available at http://x-symbol.sourceforge.net/")) ((not (pg-window-system)) (funcall error-or-warn "Proof General: x-symbol package only runs under a window system!")) ((or (not (fboundp (quote x-symbol-initialize))) (not (fboundp (quote x-symbol-register-language)))) (funcall error-or-warn "Proof General: x-symbol package installation faulty!")) ((not (proof-try-require (intern (proof-x-symbol-tokenlang-file)))) (funcall error-or-warn (format "Proof General: for x-symbol support, you must provide a library %s.el" xs-feature))) (t (require (quote x-symbol-vars)) (let* ((xs-xtra-modes proof-xsym-extra-modes) (xs-std-modes (list (or proof-mode-for-shell (intern (concat assistant "-shell-mode"))) (or proof-mode-for-response (intern (concat assistant "-response-mode"))) (or proof-mode-for-script (intern (concat assistant "-proofscript-mode"))) (or proof-mode-for-goals (intern (concat assistant "-goals-mode"))))) (all-xs-modes (append xs-std-modes xs-xtra-modes)) (am-entry (list proof-xsym-extra-modes t (backquote (quote (\, xs-lang))))) (symmode-nm (concat xs-lang-name "sym-mode")) (symmode (intern symmode-nm)) (symnamevar (intern (concat xs-feature "-name"))) (symname (concat (capitalize xs-lang-name) " Symbols")) (symmodelinevar (intern (concat xs-feature "-modeline-name"))) (symmodelinenm xs-lang-name) (flks proof-xsym-font-lock-keywords)) (x-symbol-initialize) (set symnamevar symname) (set symmodelinevar symmodelinenm) (x-symbol-register-language xs-lang xs-feature-sym all-xs-modes) (if flks (put symmode (quote font-lock-defaults) (list flks))) (setq proof-x-symbol-initialized t)))))) # bind (error) proof-x-symbol-initialize(giveerrors) (progn (set (proof-ass-sym x-symbol-enable) nil) (proof-x-symbol-initialize (quote giveerrors)) (set (proof-ass-sym x-symbol-enable) t)) (if (not proof-x-symbol-initialized) (progn (set (proof-ass-sym x-symbol-enable) nil) (proof-x-symbol-initialize (quote giveerrors)) (set (proof-ass-sym x-symbol-enable) t))) proof-x-symbol-enable() (if (proof-ass x-symbol-enable) (proof-x-symbol-enable)) proof-config-done() isar-mode-config() # bind (delay-mode-hooks) (let ((delay-mode-hooks t)) (proof-mode) (setq major-mode (quote isar-mode)) (setq mode-name "Isar script") (progn (if (get (quote proof-mode) (quote mode-class)) (put (quote isar-mode) (quote mode-class) (get (quote proof-mode) (quote mode-class)))) (unless (keymap-parent isar-mode-map) (set-keymap-parents isar-mode-map (list (current-local-map)))) (derived-mode-merge-syntax-tables (syntax-table) isar-mode-syntax-table)) (use-local-map isar-mode-map) (set-syntax-table isar-mode-syntax-table) (setq local-abbrev-table isar-mode-abbrev-table) (isar-mode-config)) (progn (make-local-variable (quote delay-mode-hooks)) (let ((delay-mode-hooks t)) (proof-mode) (setq major-mode (quote isar-mode)) (setq mode-name "Isar script") (progn (if (get (quote proof-mode) (quote mode-class)) (put (quote isar-mode) (quote mode-class) (get (quote proof-mode) (quote mode-class)))) (unless (keymap-parent isar-mode-map) (set-keymap-parents isar-mode-map (list (current-local-map)))) (derived-mode-merge-syntax-tables (syntax-table) isar-mode-syntax-table)) (use-local-map isar-mode-map) (set-syntax-table isar-mode-syntax-table) (setq local-abbrev-table isar-mode-abbrev-table) (isar-mode-config))) (delay-mode-hooks (proof-mode) (setq major-mode (quote isar-mode)) (setq mode-name "Isar script") (progn (if (get (quote proof-mode) (quote mode-class)) (put (quote isar-mode) (quote mode-class) (get (quote proof-mode) (quote mode-class)))) (unless (keymap-parent isar-mode-map) (set-keymap-parents isar-mode-map (list (current-local-map)))) (derived-mode-merge-syntax-tables (syntax-table) isar-mode-syntax-table)) (use-local-map isar-mode-map) (set-syntax-table isar-mode-syntax-table) (setq local-abbrev-table isar-mode-abbrev-table) (isar-mode-config)) isar-mode() (cond ((and (boundp (quote proof-assistant)) (not (string-equal proof-assistant ""))) (or (string-equal proof-assistant "Isabelle") (message (concat "Isabelle" " Proof General error: Proof General already in use for " proof-assistant)))) (t (proof-ready-for-assistant "Isabelle" (quote isar)) (load-library "isar") (isar-mode))) isar-mode() # bind (alist mode name keep-going) # (unwind-protect ...) # bind (just-from-file-name) set-auto-mode() #() # (unwind-protect ...) call-with-condition-handler(# #) # (condition-case ... . ((error))) # bind (find-file) normal-mode(t) # bind (nomodes after-find-file-from-revert-buffer noauto warn error) after-find-file(nil t) # (unwind-protect ...) # bind (inhibit-read-only error number truename rawfile nowarn filename buf) find-file-noselect-1(# "/home/berghofe/Scratch.thy" nil nil "/mnt/home/berghofe/Scratch.thy" (3758490783 20)) byte-code("..." [number truename rawfile nowarn filename buf set-buffer-major-mode find-file-noselect-1] 7) # (condition-case ... . ((t (byte-code "Â!ˆÃ @ A\"‡" [buf data kill-buffer signal] 3)))) # bind (number truename buf wildcards rawfile nowarn filename) find-file-noselect("/home/berghofe/Scratch.thy" nil nil nil) # bind (wildcards codesys filename) find-file("/home/berghofe/Scratch.thy") # bind (dir file-count line end-of-options file-p arg tem) command-line-1() # bind (command-line-args-left) command-line() # (condition-case ... . ((t (byte-code " ‡" [error-data data nil] 1)))) # bind (error-data) normal-top-level() # (condition-case ... . error) # (catch top-level ...)