Fix compile warnings

5 files changed, 65 insertions, 63 deletions

diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el
index a2a57949..8987b2a4 100644
--- a/generic/pg-pgip.el
+++ b/generic/pg-pgip.el
@@ -46,8 +46,8 @@ The list PGIPS may contain one or more PGIP packets, whose contents are processe
   ;; PGIP processing is split into two steps:
   ;; (1) process each command, altering internal data structures
   ;; (2) post-process for each command type, affecting external interface (menus, etc).
-  (mapcar 'pg-pgip-post-process
-	  (reduce 'union (mapcar 'pg-pgip-process-pgip pgips))))
+  (mapc 'pg-pgip-post-process
+	(reduce 'union (mapcar 'pg-pgip-process-pgip pgips))))
 
 ;; TODO: use id's and sequence numbers to reconstruct streams of messages.
 (defvar pg-pgip-last-seen-id nil)
@@ -246,9 +246,9 @@ Return a symbol representing the PGIP command processed, or nil."
 		(adjoin objtype proof-assistant-idtables)))
 	(cond
 	 ((or (eq opn 'setids) (eq opn 'addids))
-	  (mapcar (lambda (i) (intern i obarray)) idents))
+	  (mapc (lambda (i) (intern i obarray)) idents))
 	 ((eq opn 'delids)
-	  (mapcar (lambda (i) (unintern i obarray)) idents))
+	  (mapc (lambda (i) (unintern i obarray)) idents))
 	 (t
 	  (pg-pgip-error "Pg-pgip-process-ids: called on wrong node %s"
 			 (xml-node-name node))))))))
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 642387c7..54c2c919 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -642,8 +642,8 @@ If NUM is negative, move upwards.  Return new span."
       (span-set-property span 'duplicable 't)
       ;; TODO: this is faulty: moving span up gives children
       ;; list with single nil element.  Hence liveness test
-      (mapcar (lambda (s) (if (span-live-p s)
-			      (span-set-property s 'duplicable 't)))
+      (mapc (lambda (s) (if (span-live-p s)
+			    (span-set-property s 'duplicable 't)))
 	      (span-property span 'children))
       (let* ((start     (span-start span))
 	     (end       (span-end span))
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 28ec1545..0f32ccdd 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -677,7 +677,7 @@ NAME does not need to be unique."
 								(symbol-name arg)))
 		     (lambda (arg) (pg-make-element-visible idiom
 							    (symbol-name arg))))))
-    (mapcar alterfn elts))
+    (mapc alterfn elts))
   (pg-redisplay-for-gnuemacs))
 
 ;; Next two could be in pg-user.el.  No key-bindings for these.
@@ -1618,7 +1618,7 @@ Argument GOALEND is the end of the goal;."
       ;; start of the buffer, we make a fake goal-save region.
 
       ;; Delete spans between the previous goal and new command
-      (mapcar 'span-delete dels)
+      (mapc 'span-delete dels)
 
       ;; Try to set the name from the goal... [as above]
       (setq nam (or (proof-get-name-from-goal gspan)
@@ -2353,7 +2353,7 @@ others)."
 ;; 		      (unless (eq (span-property span 'type) 'comment)
 ;; 			(pg-remove-from-input-history
 ;; 			 (span-property span 'cmd))))))
-;; 	  (mapcar fn (reverse cmds)))
+;; 	  (mapc fn (reverse cmds)))
 	
 	(proof-script-delete-spans start end)
 	(span-delete span)
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 12dfc738..c4ec9411 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -829,13 +829,61 @@ This function sets variables: `proof-shell-last-output',
     (t
      (setq proof-shell-last-output-kind 'response)))))
 
+
+
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
-;;   Low-level commands for shell communication
+;; Interrupts
 ;;
 
+(defvar proof-shell-expecting-output nil
+  "A flag indicating some input has been sent and we're expecting output.
+This is used when processing interrupts.")
+
+(defvar proof-shell-interrupt-pending nil
+  "A flag indicating an interrupt is pending.
+This ensures that the proof queue will be interrupted even if no
+interrupt message is printed from the prover after the last output.")
+
+
+(defun proof-interrupt-process ()
+  "Interrupt the proof assistant.  Warning! This may confuse Proof General.
+
+This sends an interrupt signal to the proof assistant, if Proof General
+thinks it is busy.
+
+This command is risky because we don't know whether the last command
+succeeded or not.  The assumption is that it didn't, which should be true
+most of the time, and all of the time if the proof assistant has a careful
+handling of interrupt signals.
+
+Some provers may ignore (and lose) interrupt signals, or fail to indicate
+that they have been acted upon but get stop in the middle of output.
+In the first case, PG will terminate the queue of commands at the first
+available point.  In the second case, you may need to press enter inside
+the prover command buffer (e.g., with Isabelle2009 press RET inside *isabelle*)."
+  (interactive)
+  (unless (proof-shell-live-buffer)
+      (error "Proof Process Not Started!"))
+  (unless proof-shell-busy
+    (error "Proof Process Not Active!"))
+  (with-current-buffer proof-shell-buffer
+    (if proof-shell-expecting-output
+	(progn
+	  (setq proof-shell-interrupt-pending t) ; interrupt even if no interrupt message
+	  (interrupt-process nil comint-ptyp))
+      ;; otherwise, interrupt the queue right here
+      (proof-shell-error-or-interrupt-action 'interrupt))))
+      
 
 
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;;   Low-level commands for shell communication
+;;
+
 ;;;###autoload
 (defun proof-shell-insert (string action &optional scriptspan)
   "Insert STRING at the end of the proof shell, call `comint-send-input'.
@@ -1062,7 +1110,7 @@ The return value is non-nil if the action list is now empty."
 		   (string=
 		    (nth 1 (setq item (car proof-action-list)))
 		    proof-no-command))
-	 (proo-shell-invoke-callback item)
+	 (proof-shell-invoke-callback item)
 	 (setq proof-action-list (cdr proof-action-list)))
 
        ;; if action list is (nearly) empty, ensure prover is noisy.
@@ -1554,7 +1602,7 @@ by the filter is to send the next command from the queue."
      (t
       (setq proof-shell-delayed-output-kind proof-shell-last-output-kind)
       (setq proof-shell-delayed-output proof-shell-last-output)
-      (setq proof-shell-delayed-flags flags)
+      (setq proof-shell-delayed-output-flags flags)
       (if (proof-shell-exec-loop)
 	  (proof-shell-handle-delayed-output))))))
 
@@ -1568,14 +1616,14 @@ This is useful even with empty delayed output, since it clears buffers."
   (cond
    ;; Response buffer output
    ((eq proof-shell-delayed-output-kind 'abort)
-    (unless (memq 'no-error-display proof-shell-delayed-flags)
+    (unless (memq 'no-error-display proof-shell-delayed-output-flags)
       (pg-response-display proof-shell-delayed-output)))
    ((eq proof-shell-delayed-output-kind 'response)
-    (unless (memq 'no-response-display proof-shell-delayed-flags))
-      (pg-response-display proof-shell-delayed-output))
+    (unless (memq 'no-response-display proof-shell-delayed-output-flags)
+      (pg-response-display proof-shell-delayed-output)))
    ;; Goals buffer output
    ((eq proof-shell-delayed-output-kind 'goals)
-    (unless (memq 'no-goals-display proof-shell-delayed-flags)
+    (unless (memq 'no-goals-display proof-shell-delayed-output-flags)
       (pg-goals-display proof-shell-delayed-output)))
    ;; Ignore other cases
    )
@@ -1583,52 +1631,6 @@ This is useful even with empty delayed output, since it clears buffers."
 
 
 
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; Interrupt
-;;
-
-(defvar proof-shell-expecting-output nil
-  "A flag indicating some input has been sent and we're expecting output.
-This is used when processing interrupts.")
-
-(defvar proof-shell-interrupt-pending nil
-  "A flag indicating an interrupt is pending.
-This ensures that the proof queue will be interrupted even if no
-interrupt message is printed from the prover after the last output.")
-
-
-(defun proof-interrupt-process ()
-  "Interrupt the proof assistant.  Warning! This may confuse Proof General.
-
-This sends an interrupt signal to the proof assistant, if Proof General
-thinks it is busy.
-
-This command is risky because we don't know whether the last command
-succeeded or not.  The assumption is that it didn't, which should be true
-most of the time, and all of the time if the proof assistant has a careful
-handling of interrupt signals.
-
-Some provers may ignore (and lose) interrupt signals, or fail to indicate
-that they have been acted upon but get stop in the middle of output.
-In the first case, PG will terminate the queue of commands at the first
-available point.  In the second case, you may need to press enter inside
-the prover command buffer (e.g., with Isabelle2009 press RET inside *isabelle*)."
-  (interactive)
-  (unless (proof-shell-live-buffer)
-      (error "Proof Process Not Started!"))
-  (unless proof-shell-busy
-    (error "Proof Process Not Active!"))
-  (with-current-buffer proof-shell-buffer
-    (if proof-shell-expecting-output
-	(progn
-	  (setq proof-shell-interrupt-pending t) ; interrupt even if no interrupt message
-	  (interrupt-process nil comint-ptyp))
-      ;; otherwise, interrupt the queue right here
-      (proof-shell-error-or-interrupt-action 'interrupt))))
-      
-
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index 1807f691..1acc62e5 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -100,7 +100,7 @@ to the default toolbar."
     (unless proof-toolbar-map
       (setq proof-toolbar-map (make-sparse-keymap))
       (add-to-list 'image-load-path proof-images-directory) ; rude?
-      (mapcar 'proof-toolbar-make-icon (proof-ass toolbar-entries))
+      (mapc 'proof-toolbar-make-icon (proof-ass toolbar-entries))
       (proof-toolbar-make-toolbar-items proof-toolbar-map
 					(proof-ass toolbar-entries)))
     (when proof-toolbar-enable