Prevent many compile warnings

8 files changed, 165 insertions, 103 deletions

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."