diff options
| -rw-r--r-- | generic/pg-pgip.el | 8 | ||||
| -rw-r--r-- | generic/pg-user.el | 4 | ||||
| -rw-r--r-- | generic/proof-script.el | 6 | ||||
| -rw-r--r-- | generic/proof-shell.el | 108 | ||||
| -rw-r--r-- | generic/proof-toolbar.el | 2 | ||||
| -rw-r--r-- | isar/isar.el | 12 |
6 files changed, 72 insertions, 68 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 diff --git a/isar/isar.el b/isar/isar.el index 2dc2c3b6..4b91f7d7 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -20,6 +20,8 @@ (eval-when-compile (require 'span) (require 'proof-syntax) + (require 'pg-goals) + (require 'pg-vars) (proof-ready-for-assistant 'isar)) ; compile for isar (require 'isabelle-system) ; system code @@ -240,17 +242,17 @@ See -k option for Isabelle interface script." (defun isar-configure-from-settings () (isar-set-proof-find-theorems-command)) +(defpacustom use-find-theorems-form nil + "Use a form-style input for the find theorems operation." + :type 'boolean + :eval (isar-set-proof-find-theorems-command)) + (defun isar-set-proof-find-theorems-command () (setq proof-find-theorems-command (if isar-use-find-theorems-form 'isar-find-theorems-form 'isar-find-theorems-minibuffer))) -(defpacustom use-find-theorems-form nil - "Use a form-style input for the find theorems operation." - :type 'boolean - :eval (isar-set-proof-find-theorems-command)) - ;;; ;;; Theory loader operations ;;; |