From 3563de3849c59f7b97fc9406960629a7258c8a84 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Mon, 24 Feb 2003 10:38:01 +0000 Subject: Fix some compile errors --- coq/coq-syntax.el | 46 +++++++++++++++++---------- coq/coq.el | 4 ++- generic/pg-metadata.el | 4 +-- generic/pg-pgip.el | 9 +++--- generic/pg-response.el | 3 +- generic/pg-user.el | 4 +-- generic/proof-script.el | 7 ++--- generic/proof-site.el | 6 ++-- generic/proof-utils.el | 2 +- generic/span-overlay.el | 2 +- isa/x-symbol-isabelle.el | 2 ++ lego/lego.el | 4 +-- plastic/plastic.el | 81 +++++++++++++++++++++++------------------------- 13 files changed, 94 insertions(+), 80 deletions(-) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index cc6ecc60..e54822ef 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -51,27 +51,41 @@ is set to t, then ProofGeneral guesses the version of coq by doing ;; only coq-version-is-V74 and coq-version-is-V7 are used later (V6 ;; corresponds to v7=nil and v74=nil) +(unless (noninteractive) ;; DA: evaluating here gives error during compile (let* ((seedoc " (to force another version, do for example C-h v coq-version-is-V7)") (v74 (concat "proofgeneral is in coq >= 7.4 mode" seedoc)) (v7 (concat "proofgeneral is in coq =< 7.3 mode" seedoc)) (v6 (concat "proofgeneral is in coq V6 mode" seedoc))) (cond - (coq-version-is-V74 (message v74) (setq coq-version-is-V7 t)) - (coq-version-is-V7 (message v7) (setq coq-version-is-V74 nil)) - (coq-version-is-V6 (message v6) (setq coq-version-is-V74 nil) (setq coq-version-is-V7 nil)) - (t - (let* ((str (shell-command-to-string (concat coq-prog-name " -v"))) - (x (string-match "version \\([.0-9]*\\)" str)) - (num (match-string 1 str))) - (cond - ((string-match num "\\<6.") (message msgv6) - (setq coq-version-is-V7 nil) (setq coq-version-is-V74 nil)) - ((or (string-match num "\\<7.0") (string-match num "\\<7.1") - (string-match num "\\<7.2") (string-match num "\\<7.3")) - (message v7) - (setq coq-version-is-V7 t) (setq coq-version-is-V74 nil)) - ;default: 7.3.1 and above ---> 7.4 - (t (message v74) (setq coq-version-is-V7 t) (setq coq-version-is-V74 t))))))) + (coq-version-is-V74 + (message v74) + (setq coq-version-is-V7 t)) + (coq-version-is-V7 + (message v7) + (setq coq-version-is-V74 nil)) + (coq-version-is-V6 + (message v6) + (setq coq-version-is-V74 nil) + (setq coq-version-is-V7 nil)) + (t + (let* ((str (shell-command-to-string (concat coq-prog-name " -v"))) + (x (string-match "version \\([.0-9]*\\)" str)) + (num (match-string 1 str))) + (cond + ((string-match num "\\<6.") + (message v6) + (setq coq-version-is-V7 nil) + (setq coq-version-is-V74 nil)) + ((or (string-match num "\\<7.0") (string-match num "\\<7.1") + (string-match num "\\<7.2") (string-match num "\\<7.3")) + (message v7) + (setq coq-version-is-V7 t) + (setq coq-version-is-V74 nil)) + ;;default: 7.3.1 and above ---> 7.4 + (t + (message v74) + (setq coq-version-is-V7 t) + (setq coq-version-is-V74 t)))))))) ;; ----- keywords for font-lock. diff --git a/coq/coq.el b/coq/coq.el index fd008ec8..810db4b4 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -847,7 +847,6 @@ This is specific to coq-mode." proof-shell-process-file nil proof-shell-inform-file-retracted-cmd nil))) -(provide 'coq) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; @@ -896,6 +895,9 @@ mouse activation." ,(format "Check %s." thm)))))) ) +(provide 'coq) + + ;;; Local Variables: *** ;;; tab-width:2 *** ;;; fill-column: 85 *** diff --git a/generic/pg-metadata.el b/generic/pg-metadata.el index d8563199..5dcfb276 100644 --- a/generic/pg-metadata.el +++ b/generic/pg-metadata.el @@ -59,7 +59,7 @@ (modtime (nth 5 (file-attributes scriptfile))) (metadatafile (pg-metadata-filename-for scriptfile)) (metadatabuf (find-file-noselect metadatafile 'nowarn)) - (span (span-at (point-min) 'type))) + (span (span-at (point-min) 'type)) type) (pg-xml-begin-write) (pg-xml-openelt 'script-file @@ -86,7 +86,7 @@ (with-current-buffer metadatabuf (delete-region (point-min) (point-max)) (insert (pg-xml-doc)) - (write-file metadatafile)))) + (write-file metadatafile))))) ;(defun pg-read-metadata-file (buffer) diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el index 7ff79d00..7842063d 100644 --- a/generic/pg-pgip.el +++ b/generic/pg-pgip.el @@ -247,15 +247,16 @@ (or (string-equal value "true") (string-equal value "false"))) (pg-pgip-interpret-value value 'boolean)) ((and - (memq 'integer (cdr type)) + (memq 'integer choices) (string-match "[0-9]+$" value)) (pg-pgip-interpret-value value 'integer)) - ((memq 'string (cdr type)) + ((memq 'string choices) ;; FIXME: No special syntax for string inside PGIP yet, should be? (pg-pgip-interpret-value value 'string)) (t - (pg-pgip-error "pg-pgip-interpret-choice: mismatching value %s for choices %s" - value choices)))) + (pg-pgip-error + "pg-pgip-interpret-choice: mismatching value %s for choices %s" + value choices)))) (defun pg-pgip-interpret-value (value type) (cond diff --git a/generic/pg-response.el b/generic/pg-response.el index 6f555513..1591ad1a 100644 --- a/generic/pg-response.el +++ b/generic/pg-response.el @@ -325,13 +325,14 @@ and start at the first error." (defun pg-thms-buffer-clear () "Clear the theorems buffer." (with-current-buffer proof-thms-buffer + (let (start str) (goto-char (point-max)) (newline) (setq start (point)) (insert str) (unless (bolp) (newline)) (proof-fontify-region start (point)) - (set-buffer-modified-p nil))) + (set-buffer-modified-p nil)))) diff --git a/generic/pg-user.el b/generic/pg-user.el index 27adf37f..f6b7cdd6 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -552,7 +552,7 @@ Make sure the modeline is updated to display new value for electric terminator." (defun proof-electric-term-incomment-fn () "Used as argument to proof-assert-until-point." - ;; CAREFUL: (1) dynamic scoping here + ;; CAREFUL: (1) dynamic scoping here (incomment, ins, mrk) ;; (2) needs this name to be recognized in ;; proof-assert-until-point (setq incomment t) @@ -803,7 +803,7 @@ If NUM is negative, move upwards. Return new span." (defun pg-fixup-children-span (span) (if (span-property span 'controlspan) - ;; WARNING: dynamic binding + ;; WARNING: dynamic binding for new-span (progn (set-span-property span 'controlspan new-span) (list span)))) diff --git a/generic/proof-script.el b/generic/proof-script.el index 56080211..3a8f7167 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1839,10 +1839,9 @@ This version is used when `proof-script-command-end-regexp' is set." ;; (FIXME: ignore nested comments here, we should ;; have a consistent policy!) (unless - (if (fboundp 'comment-forward) - (progn + (if (progn (goto-char (or (match-end 1) (match-beginning 0))) - (comment-forward)) + (forward-comment)) (proof-re-search-forward proof-script-comment-end-regexp cmdend t)) (error @@ -2385,7 +2384,7 @@ with `proof-script-set-buffer-hooks' which is what this function does, as well as setting `proof-script-buffer-file-name' (which see). This hook also gives a warning in case this is the active scripting buffer." - (setq proof-script-buffer-file-true buffer-file-name) + (setq proof-script-buffer-file-name buffer-file-name) (if (eq (current-buffer) proof-script-buffer) (proof-warning "Active scripting buffer changed name; synchronization risked if prover tracks filenames!")) diff --git a/generic/proof-site.el b/generic/proof-site.el index d2205a2f..6001771d 100644 --- a/generic/proof-site.el +++ b/generic/proof-site.el @@ -83,9 +83,9 @@ You can use customize to set this variable." (cons proof-info-directory Info-directory-list)) (setq Info-dir-contents nil))) ;; Info is not yet initialized. Change its default. - (if (not (member proof-info-directory Info-default-directory-list)) - (setq Info-default-directory-list - (cons proof-info-directory Info-default-directory-list))))) + (if (not (member proof-info-directory Info-directory-list)) + (setq Info-directory-list + (cons proof-info-directory Info-directory-list))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; diff --git a/generic/proof-utils.el b/generic/proof-utils.el index da796e2c..639f206d 100644 --- a/generic/proof-utils.el +++ b/generic/proof-utils.el @@ -782,7 +782,7 @@ EXTRAPATH is a list of extra path components" (executable-find progname))) ;; PG 3.4: try a new Emacs function. ((fboundp 'locate-file) (locate-file progname - (append (split-path (getenv "PATH") extrapth)) + (append (split-path (getenv "PATH") extrapath)) (if proof-running-on-win32 '(".exe")) 1))) (if returnnopath progname))) diff --git a/generic/span-overlay.el b/generic/span-overlay.el index 41097447..6055e03a 100644 --- a/generic/span-overlay.el +++ b/generic/span-overlay.el @@ -280,7 +280,7 @@ A span is before PT if it covers the character before PT." ;; list may be huge: is it a bottleneck?) ;; [Why has this function never used the before-list ?] (let* ((start (overlay-start span)) - (pos start) + ;; (pos start) (nextos (overlays-in (1+ start) (point-max))) diff --git a/isa/x-symbol-isabelle.el b/isa/x-symbol-isabelle.el index 5288f5aa..0fbb575c 100644 --- a/isa/x-symbol-isabelle.el +++ b/isa/x-symbol-isabelle.el @@ -175,6 +175,8 @@ Uses `x-symbol-isabelle-font-lock-scripts-regexp'." ;;; Charsym Info ;;;=========================================================================== +;;; FIXME: da: attempting to compile these defcustoms gives error on +;;; !! Symbol's function definition is void ((x-symbol-set-cache-variable)) (defcustom x-symbol-isabelle-class-alist '((VALID "Isabelle Symbol" (x-symbol-info-face)) (INVALID "no Isabelle Symbol" (red x-symbol-info-face))) diff --git a/lego/lego.el b/lego/lego.el index 6a8b50d6..00a32319 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -350,11 +350,11 @@ Checks the width in the `proof-goals-buffer'" (setq outline-heading-end-regexp lego-outline-heading-end-regexp) ;; tags - (cond ((boundp 'tags-table-list) + (cond ((boundp 'tags-table-list) ;; GNU Emacs (make-local-variable 'tags-table-list) (setq tags-table-list (cons lego-tags tags-table-list)))) - (and (boundp 'tag-table-alist) + (and (boundp 'tag-table-alist) ;; XEmacs (setq tag-table-alist (append '(("\\.l$" . lego-tags) ("lego" . lego-tags)) diff --git a/plastic/plastic.el b/plastic/plastic.el index 5b033daf..463ab4ec 100644 --- a/plastic/plastic.el +++ b/plastic/plastic.el @@ -540,60 +540,55 @@ We assume that module identifiers coincide with file names." (defun plastic-large-bar () (interactive) (insert "%-------------------------------------------------------------------------------\n")) -(defun plastic-preprocessing () +(defun plastic-preprocessing () ;; NB: dynamic scoping of string "clear comments and remove literate marks (ie, \\n> ) - acts on var string" - ;; might want to use proof-string-match here if matching is going to be - ;; case sensitive (see docs) + ;; might want to use proof-string-match here if matching is going + ;; to be case sensitive (see docs) (if (= 0 (length plastic-lit-string)) - string ;; no-op if non-literate - - ;; remaining lines are the Else. (what, no 'return'?) + string ; no-op if non-literate + ; remaining lines are the + ; Else. (what, no 'return'?) (setq string (concat "\n" string " ")) ;; seed routine below, & extra char (let* ;; da: let* not really needed, added to nuke byte-comp warnings. - ( (i 0) - (l (length string)) - (eat-rest (lambda () + (x + (i 0) + (l (length string)) + (eat-rest (lambda () (aset string i ?\ ) ;; kill the \n or "-" at least (incf i) (while (and (< i l) (/= (aref string i) ?\n)) - (aset string i ?\ ) - (incf i) ))) - (keep-rest (lambda () - (loop for x in (string-to-list plastic-lit-string) - do (aset string i ?\ ) (incf i)) - (while (and (< i l) - (/= (aref string i) ?\n) - (/= (aref string i) ?-)) - (incf i) ))) - ) - (while (< i l) - (cond - ((eq 0 (string-match "--" (substring string i))) - (funcall eat-rest)) ;; comment. - ((eq 0 (string-match "\n\n" (substring string i))) - (aset string i ?\ ) - (incf i)) ;; kill repeat \n - - ((= (aref string i) ?\n) ;; start of new line - (aset string i ?\ ) (incf i) ;; remove \n - - (if (eq 0 (string-match plastic-lit-string - (substring string i))) - (funcall keep-rest) ;; code line. - (funcall eat-rest) ;; non-code line - )) - - (t (incf i)) ;; else include. - ) - ) - (setq string (replace-in-string string " *" " ")) - (setq string (replace-in-string string "^ *" "")) + (aset string i ?\ ) + (incf i) ))) + (keep-rest (lambda () + (loop for x in (string-to-list plastic-lit-string) + do (aset string i ?\ ) (incf i)) + (while (and (< i l) + (/= (aref string i) ?\n) + (/= (aref string i) ?-)) + (incf i) )))) + (while (< i l) + (cond + ((eq 0 (string-match "--" (substring string i))) + (funcall eat-rest)) ; comment. + ((eq 0 (string-match "\n\n" (substring string i))) + (aset string i ?\ ) + (incf i)) ; kill repeat \n + ((= (aref string i) ?\n) ; start of new line + (aset string i ?\ ) (incf i) ; remove \n + (if (eq 0 (string-match plastic-lit-string + (substring string i))) + (funcall keep-rest) ; code line. + (funcall eat-rest) ; non-code line + )) + (t + (incf i)))) ; else include. + (setq string (replace-in-string string " *" " ")) + (setq string (replace-in-string string "^ *" "")) (if (string-match "^\\s-*$" string) (setq string (concat "ECHO comment line" proof-terminal-string)) - string) - ))) + string)))) (defun plastic-all-ctxt () -- cgit v1.2.3