From 215664c12e191603a521e82a302cb97a962aacb8 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 15 Sep 2009 08:07:27 +0000 Subject: Prevent many compile warnings --- phox/phox-extraction.el | 6 ++- phox/phox-font.el | 5 +++ phox/phox-fun.el | 95 +++++++++++++++++++++------------------- phox/phox-outline.el | 25 ++++++++--- phox/phox-pbrpm.el | 12 +++++ phox/phox-sym-lock.el | 114 ++++++++++++++++++++++++++++++------------------ phox/phox-tags.el | 5 +++ phox/phox.el | 6 --- 8 files changed, 165 insertions(+), 103 deletions(-) (limited to 'phox') diff --git a/phox/phox-extraction.el b/phox/phox-extraction.el index 3ffbacbb..87ea70f6 100644 --- a/phox/phox-extraction.el +++ b/phox/phox-extraction.el @@ -8,9 +8,11 @@ ;;--------------------------------------------------------------------------;; (require 'cl) + (eval-when (compile) - (defvar phox-prog-name nil) - (declare-function proof-shell-invisible-command (str))) + (defvar phox-prog-name nil)) + +(declare-function proof-shell-invisible-command "proof-shell" (str)) ;; configuration : diff --git a/phox/phox-font.el b/phox/phox-font.el index 2eca2c5a..3e86dd28 100644 --- a/phox/phox-font.el +++ b/phox/phox-font.el @@ -1,3 +1,8 @@ +(defvar phox-sym-lock-enabled nil) ; da: for clean compile +(defvar phox-sym-lock-color nil) ; da: for clean compile +(defvar phox-sym-lock-keywords nil) ; da: for clean compile +(declare-function phox-sym-lock "phox-sym-lock") + ;;--------------------------------------------------------------------------;; ;;--------------------------------------------------------------------------;; ;; Font lock keywords diff --git a/phox/phox-fun.el b/phox/phox-fun.el index ded13ed0..fdc6c51e 100644 --- a/phox/phox-fun.el +++ b/phox/phox-fun.el @@ -1,68 +1,72 @@ ;; $State$ $Date$ $Revision$ ;; syntax -(setq - phox-forget-id-command "del %s.\n" - phox-forget-proof-command "del_proof %s.\n" - phox-forget-new-elim-command "edel elim %s.\n" - phox-forget-new-intro-command "edel intro %s.\n" - phox-forget-new-equation-command "edel equation %s.\n" - phox-forget-close-def-command "edel closed %s.\n" +(require 'span) +(require 'proof-syntax) +(require 'proof-script) + +(eval-when-compile + (require 'proof-utils)) + +(defconst phox-forget-id-command "del %s.\n") +(defconst phox-forget-proof-command "del_proof %s.\n") +(defconst phox-forget-new-elim-command "edel elim %s.\n") +(defconst phox-forget-new-intro-command "edel intro %s.\n") +(defconst phox-forget-new-equation-command "edel equation %s.\n") +(defconst phox-forget-close-def-command "edel closed %s.\n") ; phox-comments-regexp : a sequence of comments and white spaces - phox-comments-regexp "[ \n\t\r]*\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)*" +(defconst phox-comments-regexp "[ \n\t\r]*\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)*") ; phox-strict-comments-regexp : a not empty sequence of comments and white spaces - phox-strict-comments-regexp "\\([ \n\t\r]+\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)*\\|\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)+\\)" - phox-ident-regexp "\\(\\([^() \n\t\r=\\[.]\\|\\(\\.[^() \n\t\r]\\)\\)+\\)" - phox-inductive-option "\\(\\[[^]]*]\\)?" - phox-spaces-regexp "[ \n\t\r]*" - phox-sy-definition-regexp (concat +(defconst phox-strict-comments-regexp "\\([ \n\t\r]+\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)*\\|\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)+\\)") +(defconst phox-ident-regexp "\\(\\([^() \n\t\r=\\[.]\\|\\(\\.[^() \n\t\r]\\)\\)+\\)") +(defconst phox-inductive-option "\\(\\[[^]]*]\\)?") +(defconst phox-spaces-regexp "[ \n\t\r]*") +(defconst phox-sy-definition-regexp (concat "\\(Cst\\|\\(def\\(rec\\)?\\)\\)" phox-comments-regexp - "\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]+\"\\([^\"]+\\)\\)") - phox-sy-inductive-regexp (concat + "\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]+\"\\([^\"]+\\)\\)")) +(defconst phox-sy-inductive-regexp (concat "Inductive" phox-comments-regexp phox-inductive-option phox-comments-regexp - "\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]+\"\\([^\"]+\\)\\)") - phox-inductive-regexp (concat + "\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]+\"\\([^\"]+\\)\\)")) +(defconst phox-inductive-regexp (concat "Inductive" phox-comments-regexp phox-inductive-option phox-comments-regexp - phox-ident-regexp) - phox-data-regexp (concat + phox-ident-regexp)) +(defconst phox-data-regexp (concat "\\(Data\\|type\\)" phox-comments-regexp phox-inductive-option phox-comments-regexp - phox-ident-regexp) - phox-definition-regexp (concat + phox-ident-regexp)) +(defconst phox-definition-regexp (concat "\\(Cst\\|def\\(_thlist\\|rec\\)?\\|claim\\|Sort\\)" phox-comments-regexp - phox-ident-regexp) - phox-prove-claim-regexp (concat + phox-ident-regexp)) +(defconst phox-prove-claim-regexp (concat "prove_claim" phox-comments-regexp - phox-ident-regexp) - phox-new-elim-regexp (concat + phox-ident-regexp)) +(defconst phox-new-elim-regexp (concat "new_elim\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]" - phox-ident-regexp) - phox-new-intro-regexp (concat + phox-ident-regexp)) +(defconst phox-new-intro-regexp (concat "new_intro\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]" - phox-ident-regexp) - phox-new-rewrite-regexp (concat + phox-ident-regexp)) +(defconst phox-new-rewrite-regexp (concat "new_rewrite\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]" - phox-ident-regexp) - phox-new-equation-regexp (concat + phox-ident-regexp)) +(defconst phox-new-equation-regexp (concat "new_equation\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]" - phox-ident-regexp) - phox-close-def-regexp (concat + phox-ident-regexp)) +(defconst phox-close-def-regexp (concat "close_def" phox-comments-regexp - "\\(\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)+\\)[. \n\t\r]") -) - + "\\(\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)+\\)[. \n\t\r]")) (defun phox-init-syntax-table (&optional TABLE) "Set appropriate values for syntax table in current buffer, @@ -248,15 +252,16 @@ or for optional argument TABLE." ;; Doing commands ;; -(defun phox-assert-next-command-interactive () - "Process until the end of the next unprocessed command after point. -If inside a comment, just process until the start of the comment." - (interactive) -; (if (and (> (point) 1) (char-equal (char-before (point)) ?\.)) (insert "\n")) - (proof-with-script-buffer - (goto-char (proof-queue-or-locked-end)) - (proof-assert-next-command) - (proof-maybe-follow-locked-end))) +(defalias 'phox-assert-next-command-interactive 'proof-assert-next-command-interactive) +;; da: might be able to achieve commented out effect with proof-electric-terminator-noterminator +;; "Process until the end of the next unprocessed command after point. +;; If inside a comment, just process until the start of the comment." +;; (interactive) +;; ; (if (and (> (point) 1) (char-equal (char-before (point)) ?\.)) (insert "\n")) +;; (proof-with-script-buffer +;; (goto-char (proof-queue-or-locked-end)) +;; (proof-assert-next-command) +;; (proof-maybe-follow-locked-end))) ;;--------------------------------------------------------------------------;; ;; Obtaining some informations on the system. diff --git a/phox/phox-outline.el b/phox/phox-outline.el index 56530ed8..649c8363 100644 --- a/phox/phox-outline.el +++ b/phox/phox-outline.el @@ -6,17 +6,28 @@ (eval-when-compile (require 'outline)) -(setq phox-outline-title-regexp "\\((\\*[ \t\n]*title =\\)") -(setq phox-outline-section-regexp "\\((\\*\\*+\\)") -(setq phox-outline-save-regexp "\\((\\*#\\)") -(setq +(declare-function phox-lang-absurd "nofile") +(declare-function phox-lang-suppress "nofile") +(declare-function phox-lang-instance "nofile") +(declare-function phox-lang-open-instance "nofile") +(declare-function phox-lang-opendef "nofile") +(declare-function phox-lang-unlock "nofile") +(declare-function phox-lang-lock "nofile") +(declare-function phox-lang-prove "nofile") +(declare-function phox-lang-let "nofile") + + +(defconst phox-outline-title-regexp "\\((\\*[ \t\n]*title =\\)") +(defconst phox-outline-section-regexp "\\((\\*\\*+\\)") +(defconst phox-outline-save-regexp "\\((\\*#\\)") +(defconst phox-outline-theo-regexp "\\((\\*lem\\)\\|\\((\\*prop\\)\\|\\((\\*fact\\)\\|\\((\\*theo\\)\\|\\((\\*def\\)\\|\\((\\*cst\\)") -(setq +(defconst phox-outline-theo2-regexp "\\(lem\\)\\|\\(prop\\)\\|\\(fact\\)\\|\\(theo\\)\\|\\(def\\)\\|\\(cst\\)\\|\\(claim\\)\\|\\(new_\\)") -(setq +(defconst phox-outline-regexp (concat phox-outline-title-regexp "\\|" @@ -25,7 +36,7 @@ phox-outline-theo-regexp "\\|" phox-outline-theo2-regexp)) -(setq phox-outline-heading-end-regexp "\\(\\*)[ \t]*\n\\)\\|\\(\\.[ \t]*\n\\)") +(defconst phox-outline-heading-end-regexp "\\(\\*)[ \t]*\n\\)\\|\\(\\.[ \t]*\n\\)") ;(if phox-outline ; (add-hook 'phox-mode-hook '(lambda()(outline-minor-mode 1))) diff --git a/phox/phox-pbrpm.el b/phox/phox-pbrpm.el index 5e831938..544fa1c4 100644 --- a/phox/phox-pbrpm.el +++ b/phox/phox-pbrpm.el @@ -9,6 +9,18 @@ (require 'pg-pbrpm) +(declare-function phox-lang-absurd "nofile") +(declare-function phox-lang-suppress "nofile") +(declare-function phox-lang-instance "nofile") +(declare-function phox-lang-open-instance "nofile") +(declare-function phox-lang-opendef "nofile") +(declare-function phox-lang-unlock "nofile") +(declare-function phox-lang-lock "nofile") +(declare-function phox-lang-prove "nofile") +(declare-function phox-lang-let "nofile") +(declare-function int-char "nofile") +(declare-function char= "nofile") + ;;--------------------------------------------------------------------------;; ;; Syntactic functions ;;--------------------------------------------------------------------------;; diff --git a/phox/phox-sym-lock.el b/phox/phox-sym-lock.el index d29c03aa..6b3874fd 100644 --- a/phox/phox-sym-lock.el +++ b/phox/phox-sym-lock.el @@ -14,7 +14,30 @@ ;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the ;; GNU General Public License for more details. -(require 'proof-compat) ; compile warnings +(require 'proof-compat) ; avoid compile warnings + +(defcustom phox-sym-lock-enabled t + "*Whether to use yum symbol or not." + :type 'boolean + :group 'phox) + +;; DA: I have crudely hacked this file so that it compiles cleanly. +;; It won't work now, but I hope we can use Unicode Tokens instead. + +(declare-function map-extents "nofile") +(declare-function extent-face "nofile") +(declare-function face-property "nofile") +(declare-function set-extent-endpoints "nofile") +(declare-function extent-start-position "nofile") +(declare-function extent-end-position "nofile") +(declare-function set-extent-property "nofile") +(declare-function face-font-name "nofile") +(declare-function font-name "nofile") +(declare-function char-int "nofile") +(declare-function obj "nofile") +(declare-function set-face-property "nofile") +(declare-function add-menu-button "nofile") + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; History @@ -164,30 +187,31 @@ (put 'phox-sym-lock-font-name 'permanent-local t) (make-face 'phox-sym-lock-adobe-symbol-face) -(if phox-sym-lock-with-mule - (progn - (make-charset 'phox-sym-lock-cset-left "Char set for symbol font" - (list 'registry "adobe-fontspecific" - 'dimension 1 - 'chars 94 -;; 'final 53 -;; DA PG 3.7: above line doesn't work on XEmacs 21.5b28, gives -;; Character set already defined for this DIMENSION/CHARS/FINAL/DIRECTION combo (indian-is13194) -;; DA: Will 55 work? - 'final 55 - 'graphic 0)) - (make-charset 'phox-sym-lock-cset-right "Char set for symbol font" - (list 'registry "adobe-fontspecific" - 'dimension 1 - 'chars 94 - 'final 54 - 'graphic 1)) - (set-face-property 'phox-sym-lock-adobe-symbol-face - 'font phox-sym-lock-font-name nil - ;; DA: removed next line, it breaks "make magic" in doc - ;; '(mule-fonts) 'prepend, - )) - (set-face-font 'phox-sym-lock-adobe-symbol-face phox-sym-lock-font-name 'global)) +; DA: DISABLED THIS top level form (PG 4.0) +;; (if phox-sym-lock-with-mule +;; (progn +;; (make-charset 'phox-sym-lock-cset-left "Char set for symbol font" +;; (list 'registry "adobe-fontspecific" +;; 'dimension 1 +;; 'chars 94 +;; ;; 'final 53 +;; ;; DA PG 3.7: above line doesn't work on XEmacs 21.5b28, gives +;; ;; Character set already defined for this DIMENSION/CHARS/FINAL/DIRECTION combo (indian-is13194) +;; ;; DA: Will 55 work? +;; 'final 55 +;; 'graphic 0)) +;; (make-charset 'phox-sym-lock-cset-right "Char set for symbol font" +;; (list 'registry "adobe-fontspecific" +;; 'dimension 1 +;; 'chars 94 +;; 'final 54 +;; 'graphic 1)) +;; (set-face-property 'phox-sym-lock-adobe-symbol-face +;; 'font phox-sym-lock-font-name nil +;; ;; DA: removed next line, it breaks "make magic" in doc +;; ;; '(mule-fonts) 'prepend, +;; )) +;; (set-face-font 'phox-sym-lock-adobe-symbol-face phox-sym-lock-font-name 'global)) (defun phox-sym-lock-set-foreground () "Set foreground color of Phox-Sym-Lock faces." @@ -206,15 +230,16 @@ (defun phox-sym-lock-translate-char (char) (if phox-sym-lock-with-mule (let ((code (if (integerp char) char (char-int char)))) - (if (< code 128) - (make-char 'phox-sym-lock-cset-left obj) - (make-char 'phox-sym-lock-cset-right (- obj 128)))) + (with-no-warnings ;; da: dynamic scope obj + (if (< code 128) + (make-char 'phox-sym-lock-cset-left obj) + (make-char 'phox-sym-lock-cset-right (- obj 128))))) char)) (defun phox-sym-lock-translate-char-or-string (obj) (if (stringp obj) (if phox-sym-lock-with-mule - (concat (mapcar phox-sym-lock-translate-char obj)) + (concat (mapcar 'phox-sym-lock-translate-char obj)) (obj)) (make-string 1 (phox-sym-lock-translate-char obj)))) @@ -224,7 +249,7 @@ given OBJ under `phox-sym-lock-adobe-symbol-face' and all other characters to the empty string. OBJ may either be a string or a character." (let* ((name (phox-sym-lock-gen-symbol "face")) (table (make-display-table)) - (tface (make-face name "phox-sym-lock-remap-face" t))) + (tface (make-face name "phox-sym-lock-remap-face"))) (fillarray table "") (aset table (string-to-char (substring pat (1- pos) pos)) (phox-sym-lock-translate-char-or-string obj)) @@ -241,7 +266,7 @@ the empty string. OBJ may either be a string or a character." (defvar phox-sym-lock-clear-face (let* ((name (phox-sym-lock-gen-symbol "face")) (table (make-display-table)) - (tface (make-face name "phox-sym-lock-remap-face" t))) + (tface (make-face name "phox-sym-lock-remap-face"))) (fillarray table "") (set-face-property tface 'display-table table) (set-face-property tface 'phox-sym-lock-remap 1) ; mark it @@ -271,12 +296,14 @@ OBJ under `phox-sym-lock-adobe-symbol-face'. The face extent will become atomic. (list pat num (phox-sym-lock-remap-face pat pos obj t) override)) (defun phox-sym-lock-pre-idle-hook-first () - (condition-case nil - (if (and phox-sym-lock-enabled font-lock-old-extent) - (setq phox-sym-lock-ext-start (extent-start-position font-lock-old-extent) - phox-sym-lock-ext-end (extent-end-position font-lock-old-extent)) - (setq phox-sym-lock-ext-start nil)) - (error (setq phox-sym-lock-ext-start nil)))) + ;; da: XEmacs isms + ;; (condition-case nil + ;; (if (and phox-sym-lock-enabled font-lock-old-extent) + ;; (setq phox-sym-lock-ext-start (extent-start-position font-lock-old-extent) + ;; phox-sym-lock-ext-end (extent-end-position font-lock-old-extent)) + ;; (setq phox-sym-lock-ext-start nil)) + ;; (error (setq phox-sym-lock-ext-start nil)))) +) (defun phox-sym-lock-pre-idle-hook-last () (condition-case nil @@ -296,7 +323,7 @@ OBJ under `phox-sym-lock-adobe-symbol-face'. The face extent will become atomic. (if font-lock-mode (progn ; (setq font-lock-keywords nil) ; Font-Lock explicit-defaults bug! - (font-lock-set-defaults t) + (font-lock-set-defaults) (font-lock-fontify-buffer))) (message "Phox-Sym-Lock enabled."))) @@ -309,7 +336,7 @@ OBJ under `phox-sym-lock-adobe-symbol-face'. The face extent will become atomic. (if font-lock-mode (progn ; (setq font-lock-keywords nil) ; Font-Lock explicit-defaults bug! - (font-lock-set-defaults t) + (font-lock-set-defaults) (font-lock-fontify-buffer))) (message "Phox-Sym-Lock disabled."))) @@ -346,10 +373,11 @@ OBJ under `phox-sym-lock-adobe-symbol-face'. The face extent will become atomic. (when (and (featurep 'font-lock) - (if font-lock-auto-fontify - (not (memq major-mode font-lock-mode-disable-list)) - (memq major-mode font-lock-mode-enable-list)) - (font-lock-set-defaults-1 explicit-defaults) + ;; da: font-lock has changed: + ;; (if font-lock-auto-fontify + ;; (not (memq major-mode font-lock-mode-disable-list)) + ;; (memq major-mode font-lock-mode-enable-list)) + ;; (font-lock-set-defaults-1 explicit-defaults) (phox-sym-lock-patch-keywords)) (turn-on-font-lock))) diff --git a/phox/phox-tags.el b/phox/phox-tags.el index 8ff2848d..603622a6 100644 --- a/phox/phox-tags.el +++ b/phox/phox-tags.el @@ -17,6 +17,11 @@ (require 'etags) +(eval-when-compile + (defvar phox-doc-dir nil) + (defvar phox-lib-dir nil) + (defvar phox-etags nil)) + (defun phox-tags-add-table(table) "add tags table" diff --git a/phox/phox.el b/phox/phox.el index 44ab68b2..42a59316 100644 --- a/phox/phox.el +++ b/phox/phox.el @@ -34,12 +34,6 @@ :type 'file :group 'phox) -(defcustom phox-sym-lock-enabled t - "*Whether to use yum symbol or not." - :type 'boolean - :group 'phox) - - (defcustom phox-web-page "http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html" "URL of web page for PhoX." -- cgit v1.2.3