From 2d6b4150e681dfb09a75eab05c052a0fa04c621c Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 22 Oct 1998 16:01:38 +0000 Subject: Added todo for clean byte compile --- generic/proof-config.el | 79 +++++++++++++++++++++++++-------- generic/proof-script.el | 111 +++++++++++++++++++++++++++++++++++++++++------ generic/proof-shell.el | 71 +----------------------------- generic/proof-toolbar.el | 2 + todo | 2 + 5 files changed, 166 insertions(+), 99 deletions(-) diff --git a/generic/proof-config.el b/generic/proof-config.el index f5fb761d..5c82946e 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -9,22 +9,65 @@ ;; $Id$ ;; ;; -;; This file declares all prover-specific configuration variables. -;; These are used variously by the proof script mode and the proof -;; shell mode. +;; This file declares all user options and prover-specific +;; configuration variables for Proof General. The variables +;; are used variously by the proof script mode and the +;; proof shell mode, menus, and toolbar. ;; ;; To customize Proof General for a new proof assistant, you ;; should read this file carefully! ;; -;; 0. Major modes -;; 1. Menus, user-level commands. -;; 2. Script mode configuration -;; 3. Shell mode configuration -;; 3a. commands -;; 3b. regexps -;; 3c. hooks +;; 1. User options +;; 2. Major modes +;; 3. Menus, user-level commands. +;; 4. Script mode configuration +;; 5. Shell mode configuration +;; 5a. commands +;; 5b. regexps +;; 5c. hooks ;; +;; The user options don't need to be set on a per-prover basis. +;; The remaining variables in sections 2-5 do. +;; + +;; A global constant that's convenient to keep here. +(defconst proof-mode-name "Proof-General" + "Root name for proof script mode. +Used internally and in menu titles.") + + + +;; +;; 1. User options for proof mode +;; +;; The following variables are user options for Proof General. +;; They appear in the 'proof' customize group and should +;; *not* normally be touched by prover specific code. +;; + +(defcustom proof-prog-name-ask-p nil + "*If non-nil, query user which program to run for the inferior process." + :type 'boolean + :group 'proof) + +(defcustom proof-one-command-per-line nil + "*If non-nil, format for newlines after each proof command in a script." + :type 'boolean + :group 'proof) + +(defcustom proof-general-home-page + "http://www.dcs.ed.ac.uk/home/proofgen" + "*Web address for Proof General" + :type 'string + :group 'proof-internal) + + + +;; +;; CONFIGURATION VARIABLES +;; +;; (defgroup prover-config nil "Configuration of Proof General for the prover in use." @@ -59,9 +102,10 @@ from the name given in proof-internal-assistant-table." + ;; -;; 0. The major modes used by Proof General. +;; 2. The major modes used by Proof General. ;; (defcustom proof-mode-for-shell nil @@ -85,8 +129,9 @@ Suggestion: this can be set in proof-pre-shell-start-hook." + ;; -;; 1. Configuration for menus, user-level commands, etc. +;; 3. Configuration for menus, user-level commands, etc. ;; (defcustom proof-www-home-page "" @@ -136,7 +181,7 @@ This variable should be set before requiring proof.el" ;; -;; 2. Configuration for proof script mode +;; 4. Configuration for proof script mode ;; ;; @@ -289,7 +334,7 @@ assistant, for example, to switch to a new theory." ;; -;; 3. Configuration for proof shell +;; 5. Configuration for proof shell ;; ;; The variables in this section concern the proof shell mode. ;; The first group of variables are hooks invoked at various points. @@ -308,7 +353,7 @@ assistant, for example, to switch to a new theory." ;; -;; 3a. commands +;; 5a. commands ;; (defcustom proof-prog-name nil @@ -329,7 +374,7 @@ Suggestion: this can be set in proof-pre-shell-start-hook." ;; -;; 3b. Regexp variables for matching output from proof process. +;; 5b. Regexp variables for matching output from proof process. ;; (defcustom proof-shell-prompt-pattern nil @@ -406,7 +451,7 @@ In particular, after a `pbp-goal-command' or a `pbp-hyp-command'." :group 'proof-shell) ;; -;; 3c. hooks +;; 5c. hooks ;; (defcustom proof-shell-insert-hook nil diff --git a/generic/proof-script.el b/generic/proof-script.el index 453b18db..3a799252 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -9,6 +9,8 @@ ;; $Id$ ;; +(require 'proof-config) + ;; ;; Internal variables used by script mode ;; @@ -316,6 +318,89 @@ buffer is closed off atomically." (not buffer) (proof-mark-buffer-atomic buffer)))))) +;; NEW utility functions, use them! + +(defun proof-locked-region-full-p () + "Non-nil if the locked region covers all the buffer's non-whitespace. +Should be called from a proof script buffer." + (save-excursion + (goto-char (point-max)) + (skip-chars-backward " \t\n") + (>= (proof-unprocessed-begin) (point)))) + +(defun proof-locked-region-empty-p () + "Non-nil if the locked region is empty. +Should be called from a proof script buffer." + (eq (proof-unprocessed-begin) (point-min))) + + +(defun proof-check-process-available (&optional relaxed) + "Adjust internal variables for scripting of current buffer. + +Signals an error if current buffer is not a proof script or if the +proof process is not idle. If RELAXED is set, nothing more is done. No +changes are necessary if the current buffer is already in Scripting +minor mode. Otherwise, the current buffer will become the current +scripting buffer provided the current scripting buffer has either no +locked region or everything in it has been processed." + (proof-start-shell) + (cond + ((not (or relaxed (eq proof-buffer-type 'script))) + (error "Must be running in a script buffer")) + (proof-shell-busy (error "Proof Process Busy!")) + (relaxed ()) ;exit cond + + ;; No buffer is in Scripting minor mode. + ;; We assume the setup is done somewhere else + ;; so this should never happen + ((null proof-script-buffer-list) (assert nil)) + + ;; The current buffer is in Scripting minor mode + ;; so there's nothing to do + ((equal (current-buffer) (car proof-script-buffer-list))) + + (t + (let ((script-buffer (car proof-script-buffer-list)) + (current-buffer (current-buffer))) + (save-excursion + (set-buffer script-buffer) + ;; We only allow switching of the Scripting buffer if the + ;; locked region is either empty or full for all buffers. + ;; Here we check the current Scripting buffer's status. + (if (proof-locked-region-full-p) + ;; We're switching from a buffer which has been + ;; completely processed. Make sure that it's + ;; registered on the included files list, in + ;; case it has been processed piecemeal. + (if buffer-file-name + (proof-register-possibly-new-processed-file + buffer-file-name))) + + (if (or + (proof-locked-region-empty-p) + (proof-locked-region-full-p)) + ;; we are changing the scripting buffer + (progn + (setq proof-active-buffer-fake-minor-mode nil) + (set-buffer current-buffer) + + ;; does the current buffer contain locked regions already? + (if (member current-buffer proof-script-buffer-list) + (setq proof-script-buffer-list + (remove current-buffer proof-script-buffer-list)) + (proof-init-segmentation)) + (setq proof-script-buffer-list + (cons current-buffer proof-script-buffer-list)) + (setq proof-active-buffer-fake-minor-mode t) + (run-hooks 'proof-activate-scripting-hook)) + ;; Locked region covers only part of the buffer + ;; FIXME da: ponder alternative of trying to complete rest + ;; of current scripting buffer? + (error "Cannot deal with two unfinished script buffers!"))))))) + + + + @@ -646,15 +731,16 @@ Assumes that point is at the end of a command." (defun proof-assert-until-point (&optional unclosed-comment-fun ignore-proof-process-p) "Process the region from the end of the locked-region until point. - Default action if inside a comment is just to go until the start of - the comment. If you want something different, put it inside - unclosed-comment-fun. If ignore-proof-process-p is set, no commands - will be added to the queue." +Default action if inside a comment is just process as far as the start of +the comment. If you want something different, put it inside +unclosed-comment-fun. If ignore-proof-process-p is set, no commands +will be added to the queue." (interactive) (let ((pt (point)) (crowbar (or ignore-proof-process-p (proof-check-process-available))) semis) (save-excursion + ;; Give error if no non-whitespace between point and end of locked region. (if (not (re-search-backward "\\S-" (proof-unprocessed-begin) t)) (progn (goto-char pt) (error "I don't know what I should be doing in this buffer!"))) @@ -689,10 +775,9 @@ Assumes that point is at the end of a command." (&optional unclosed-comment-fun ignore-proof-process-p dont-move-forward for-new-command) "Process until the end of the next unprocessed command after point. -If inside a comment, just to go the start of -the comment. If you want something different, put it inside -UNCLOSED-COMMENT-FUN. If IGNORE-PROOF-PROCESS-P is set, no commands -will be added to the queue. +If inside a comment, just process until the start of the comment. +If you want something different, put it inside UNCLOSED-COMMENT-FUN. +If IGNORE-PROOF-PROCESS-P is set, no commands will be added to the queue. Afterwards, move forward to near the next command afterwards, unless DONT-MOVE-FORWARD is non-nil. If FOR-NEW-COMMAND is non-nil, a space or newline will be inserted automatically." @@ -700,6 +785,8 @@ a space or newline will be inserted automatically." (let ((pt (point)) (crowbar (or ignore-proof-process-p (proof-check-process-available))) semis) + (if (proof-locked-region-full-p) + (error "Locked region is full, no more commands to do!")) (save-excursion ;; CHANGE from old proof-assert-until-point: don't bother check ;; for non-whitespace between locked region and point. @@ -711,12 +798,10 @@ a space or newline will be inserted automatically." ;; (progn (goto-char pt) ;; (error "I don't know what I should be doing in this buffer!"))) ;; (setq semis (proof-segment-up-to (point)))) - (if (and unclosed-comment-fun (eq 'unclosed-comment (car semis))) + (if (and unclosed-comment-fun (eq 'unclosed-comment (car-safe semis))) (funcall unclosed-comment-fun) - (if (eq 'unclosed-comment (car semis)) - ;; CHANGE: if inside a comment, do as the documentation - ;; suggests. - (setq semis nil)) + (if (eq 'unclosed-comment (car-safe semis)) + (setq semis (cdr semis))) (if (and (not ignore-proof-process-p) (not crowbar) (null semis)) (error "I don't know what I should be doing in this buffer!")) (goto-char (nth 2 (car semis))) diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 1657b049..eab8dc17 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -9,6 +9,8 @@ ;; $Id$ ;; +(require 'proof-config) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Starting and stopping the proof-system shell ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -536,75 +538,6 @@ assistant." (incf i))) (save-excursion (proof-shell-insert string))) -(defun proof-check-process-available (&optional relaxed) - "Adjust internal variables for scripting of current buffer. - -Signals an error if current buffer is not a proof script or if the -proof process is not idle. If RELAXED is set, nothing more is done. No -changes are necessary if the current buffer is already in Scripting -minor mode. Otherwise, the current buffer will become the current -scripting buffer provided the current scripting buffer has either no -locked region or everything in it has been processed." - (proof-start-shell) - (cond - ((not (or relaxed (eq proof-buffer-type 'script))) - (error "Must be running in a script buffer")) - (proof-shell-busy (error "Proof Process Busy!")) - (relaxed ()) ;exit cond - - ;; No buffer is in Scripting minor mode. - ;; We assume the setup is done somewhere else - ;; so this should never happen - ((null proof-script-buffer-list) (assert nil)) - - ;; The current buffer is in Scripting minor mode - ;; so there's nothing to do - ((equal (current-buffer) (car proof-script-buffer-list))) - - (t - (let ((script-buffer (car proof-script-buffer-list)) - (current-buffer (current-buffer))) - (save-excursion - (set-buffer script-buffer) - ;; We only allow switching of the Scripting buffer if the - ;; locked region is either empty or full for all buffers. - ;; Here we check the current Scripting buffer's status. - (let - ((locked-is-empty (eq (proof-unprocessed-begin) (point-min))) - (locked-is-full (progn - (goto-char (point-max)) - (skip-chars-backward " \t\n") - (>= (proof-unprocessed-begin) (point))))) - (if locked-is-full - ;; We're switching from a buffer which has been - ;; completely processed. Make sure that it's - ;; registered on the included files list, in - ;; case it has been processed piecemeal. - (if buffer-file-name - (proof-register-possibly-new-processed-file - buffer-file-name))) - - (if (or locked-is-full locked-is-empty) - ;; we are changing the scripting buffer - (progn - (setq proof-active-buffer-fake-minor-mode nil) - (set-buffer current-buffer) - - ;; does the current buffer contain locked regions already? - (if (member current-buffer proof-script-buffer-list) - (setq proof-script-buffer-list - (remove current-buffer proof-script-buffer-list)) - (proof-init-segmentation)) - (setq proof-script-buffer-list - (cons current-buffer proof-script-buffer-list)) - (setq proof-active-buffer-fake-minor-mode t) - (run-hooks 'proof-activate-scripting-hook)) - ;; Locked region covers only part of the buffer - ;; FIXME da: ponder alternative of trying to complete rest - ;; of current scripting buffer? - (error "Cannot deal with two unfinished script buffers!")))))))) - - (defun proof-grab-lock (&optional relaxed) (proof-start-shell) (proof-check-process-available relaxed) diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el index 31a70e9d..2795ea18 100644 --- a/generic/proof-toolbar.el +++ b/generic/proof-toolbar.el @@ -10,6 +10,8 @@ ;; Toolbar is just for scripting buffer at the moment. ;; +(require 'proof-config) + (defcustom proof-toolbar-wanted t "*Whether to use toolbar in proof mode." :type 'boolean diff --git a/todo b/todo index bedf88dc..8dc8b60e 100644 --- a/todo +++ b/todo @@ -14,6 +14,8 @@ X (Low) probably not worth wasting time on * This is a list of things which need doing in the generic interface ==================================================================== +A* Fixup for clean byte compile now that proof.el has been split. + A* Fixup multiple files -- needs debugging. 1. mark atomic makes some assumption about non-comment commands in -- cgit v1.2.3