diff options
-rw-r--r-- | Makefile.devel | 4 | ||||
-rw-r--r-- | generic/proof-config.el | 28 | ||||
-rw-r--r-- | generic/proof-script.el | 5 | ||||
-rw-r--r-- | generic/proof-shell.el | 94 | ||||
-rw-r--r-- | generic/proof.el | 12 | ||||
-rw-r--r-- | lego/lego-syntax.el | 8 | ||||
-rw-r--r-- | lego/lego.el | 26 | ||||
-rw-r--r-- | todo | 10 |
8 files changed, 128 insertions, 59 deletions
diff --git a/Makefile.devel b/Makefile.devel index 5c577b16..48ab9786 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -17,7 +17,7 @@ ## make rpm - make RPM packages based on etc/ProofGeneral.spec ## ## make release - make tag, dist, and install it in RELEASEDIR. -## make releaseall - make release and rpmrelease. +## make releaseall - make release, local installation and rpmrelease. ## ## make distinstall - install distribution build by 'make dist' ## into DISTINSTALLDIR. @@ -332,7 +332,7 @@ releaseclean: ## releaseall: ## Do everything! ## -releaseall: release rpmrelease releaseclean +releaseall: release rpmrelease distinstall releaseclean ############################################################ ## diff --git a/generic/proof-config.el b/generic/proof-config.el index b4f42458..9fcb13ec 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -198,6 +198,11 @@ Could come either from proof assistant or Proof General itself." ;; functions. This is why prover-config appears under the ;; proof-general-internal group. +(defcustom proof-assistant-home-page "http://www.dcs.ed.ac.uk/home/proofgen/" + "Web address of the proof assistant Proof General is using." + :type 'string + :group 'prover-config) + (defcustom proof-assistant "" "Name of the proof assistant Proof General is using. This is set automatically by the mode stub defined in proof-site, @@ -212,29 +217,38 @@ from the name given in proof-assistant-table." ;; 2. The major modes used by Proof General. ;; -;; FIXME: these symbols could be set automatically to standard values, +;; FIXME: these functions could be set automatically to standard values, ;; i.e. <assistant>-mode, <assistant>-shell-mode, <assistant>-pbp-mode. ;; FIXME: mode-for-script is unused at the moment, added just for ;; uniformity. The other two are used when a shell buffer is started. -(defcustom proof-mode-for-shell nil +(defcustom proof-mode-for-shell 'proof-shell-mode "Mode for proof shell buffers. +Usually customised for specific prover. +Suggestion: this can be set in proof-pre-shell-start-hook." + :type 'function + :group 'prover-config) + +(defcustom proof-mode-for-response 'proof-response-mode + "Mode for proof response buffer. +Usually customised for specific prover. Suggestion: this can be set in proof-pre-shell-start-hook." - :type 'symbol + :type 'function :group 'prover-config) -(defcustom proof-mode-for-pbp nil +(defcustom proof-mode-for-pbp 'pbp-mode "Mode for proof state display buffers. +Usually customised for specific prover. Suggestion: this can be set in proof-pre-shell-start-hook." - :type 'symbol + :type 'function :group 'prover-config) -(defcustom proof-mode-for-script nil +(defcustom proof-mode-for-script 'ignore "Mode for proof script buffers. This is used by Proof General to find out which buffers contain proof scripts. Suggestion: this can be set in the script mode configuration." - :type 'symbol + :type 'function :group 'prover-config) diff --git a/generic/proof-script.el b/generic/proof-script.el index fa09ede9..624a468e 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -272,10 +272,7 @@ to allow other files loaded by proof assistants to be marked read-only." (defun proof-warning (str) "Issue the warning STR." (proof-response-buffer-display str 'proof-warning-face) - (display-buffer proof-response-buffer) - (set-window-dedicated-p - (get-buffer-window proof-response-buffer) 'dedicated)) - + (proof-display-and-keep-buffer proof-response-buffer)) (defun proof-register-possibly-new-processed-file (file) "Register a possibly new FILE as having been processed by the prover." diff --git a/generic/proof-shell.el b/generic/proof-shell.el index f39479c8..f4b31772 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -206,6 +206,8 @@ Does nothing if proof assistant is already running." (save-excursion (set-buffer proof-shell-buffer) (funcall proof-mode-for-shell) + (set-buffer proof-response-buffer) + (funcall proof-mode-for-response) (set-buffer proof-pbp-buffer) (funcall proof-mode-for-pbp)) @@ -338,7 +340,15 @@ Does nothing if proof assistant is already running." ;; processed (assuming they're all successful) (defvar proof-shell-delayed-output nil - "Last interesting output from proof process output and what to do with it.") + "Last interesting output from proof process output and what to do with it. + +This is a list of tuples of the form (type . string). type is either +'analyse or 'insert. + +'analyse denotes that string's term structure ought to be analysed + and displayed in the `proof-goals-buffer' +'insert denotes that string ought to be displayed in the + `proof-response-buffer' ") (defun proof-shell-analyse-structure (string) (save-excursion @@ -351,7 +361,7 @@ Does nothing if proof assistant is already running." (progn (aset out op c) (incf op))) (incf ip)) - (display-buffer (set-buffer proof-pbp-buffer)) + (proof-display-and-keep-buffer (set-buffer proof-pbp-buffer)) (erase-buffer) (insert (substring out 0 op)) @@ -408,12 +418,10 @@ Does nothing if proof assistant is already running." (substring out 0 op))) (defun proof-shell-handle-output (start-regexp end-regexp append-face) - "Pretty print output in process buffer in specified region. -The region begins with the match for START-REGEXP and is delimited by + "Displays output from `proof-shell-buffer' in + `proof-response-buffer'. +The region in `proof-shell-buffer begins with the match for START-REGEXP and is delimited by END-REGEXP. The match for END-REGEXP is not part of the specified region. -Removes any annotations in the region. -Fontifies the region. -Appends APPEND-FACE to the text property of the region . Returns the string (with faces) in the specified region." (let (start end string) (save-excursion @@ -424,33 +432,38 @@ Returns the string (with faces) in the specified region." (length (match-string 0))))) (setq string (proof-shell-strip-annotations (buffer-substring start end))) - (delete-region start end) + (set-buffer proof-response-buffer) + (goto-char (point-max)) + (newline) + (setq start (point-max)) (insert string) (setq end (+ start (length string))) + ;; FIXME tms: FSF Emacs 20.2 problems ;; This doesn't work with FSF Emacs 20.2's version of Font-lock ;; because there are no known keywords in the process buffer ;; Never mind. In a forthcoming version, the process buffer will ;; not be tampered with. Fontification will take place in a ;; separate response buffer. - ;; (font-lock-fontify-region start end) + (font-lock-fontify-region start end) (font-lock-append-text-property start end 'face append-face) (buffer-substring start end)))) (defun proof-shell-handle-delayed-output () + "Display delayed output. +See the documentation fo `proof-shell-delayed-output' for furter details." (let ((ins (car proof-shell-delayed-output)) (str (cdr proof-shell-delayed-output))) - (display-buffer proof-pbp-buffer) - (save-excursion - (cond - ((eq ins 'insert) - (setq str (proof-shell-strip-annotations str)) - (set-buffer proof-pbp-buffer) + (cond + ((eq ins 'insert) + (setq str (proof-shell-strip-annotations str)) + (save-excursion + (set-buffer proof-response-buffer) (erase-buffer) (insert str)) - ((eq ins 'analyse) - (proof-shell-analyse-structure str)) - (t (set-buffer proof-pbp-buffer) - (insert "\n\nbug???"))))) + (proof-display-and-keep-buffer proof-response-buffer)) + ((eq ins 'analyse) + (proof-shell-analyse-structure str)) + (t (assert nil)))) (run-hooks 'proof-shell-handle-delayed-output-hook) (setq proof-shell-delayed-output (cons 'insert "done"))) @@ -478,8 +491,8 @@ Returns the string (with faces) in the specified region." (defun proof-shell-handle-error (cmd string) "React on an error message triggered by the prover. -We display the process buffer, scroll to the end, beep and fontify the -error message. At the end it calls `proof-shell-handle-error-hook'. " +The error message is displayed in the `proof-response-buffer'. Then, +we call `proof-shell-handle-error-hook'. " ;; We extract all text between text matching ;; `proof-shell-error-regexp' and the following prompt. ;; Alternatively one could higlight all output between the @@ -491,7 +504,7 @@ error message. At the end it calls `proof-shell-handle-error-hook'. " (proof-shell-handle-output proof-shell-error-regexp proof-shell-annotated-prompt-regexp 'proof-error-face) - (save-excursion (display-buffer proof-shell-buffer) + (save-excursion (proof-display-and-keep-buffer proof-response-buffer) (beep) ;; unwind script buffer @@ -559,10 +572,12 @@ assistant." ((and proof-shell-abort-goal-regexp (string-match proof-shell-abort-goal-regexp string)) - (setq proof-shell-delayed-output (cons 'insert "\n\nAborted")) + (proof-clean-buffer proof-pbp-buffer) + (setq proof-shell-delayed-output (cons 'insert "\n\nAborted")) ()) ((string-match proof-shell-proof-completed-regexp string) + (proof-clean-buffer proof-pbp-buffer) (setq proof-shell-proof-completed t) (setq proof-shell-delayed-output (cons 'insert (concat "\n" (match-string 0 string))))) @@ -956,8 +971,25 @@ Annotations are characters 128-255." "Menu used in Proof General shell mode." (cons proof-mode-name (cdr proof-shell-menu))) +(defun proof-font-lock-minor-mode () + "Start font-lock as a minor mode in the current buffer." + (and (fboundp 'font-lock-set-defaults) (font-lock-set-defaults))) + +(defun proof-goals-config-done () + "Initialise the goals buffer after the child has been configured." + (save-excursion + (set-buffer proof-pbp-buffer) + (proof-font-lock-minor-mode))) + + +(defun proof-response-config-done () + "Initialise the response buffer after the child has been configured." + (save-excursion + (set-buffer proof-response-buffer) + (proof-font-lock-minor-mode))) + (defun proof-shell-config-done () - "Initialise the specific proover after the child has been configured." + "Initialise the specific prover after the child has been configured." (save-excursion (set-buffer proof-shell-buffer) (accept-process-output (get-buffer-process proof-shell-buffer)) @@ -984,16 +1016,24 @@ Annotations are characters 128-255." () (error "Failed to initialise proof process"))))) +(eval-and-compile +(define-derived-mode proof-universal-keys-only-mode fundamental-mode + proof-mode-name "Universal keymaps only" + (suppress-keymap proof-universal-keys-only-mode-map 'all) + (proof-define-keys pbp-mode-map proof-universal-keys))) + (eval-and-compile ; to define vars -(define-derived-mode pbp-mode fundamental-mode +(define-derived-mode pbp-mode proof-universal-keys-only-mode proof-mode-name "Proof by Pointing" ;; defined-derived-mode pbp-mode initialises pbp-mode-map (setq proof-buffer-type 'pbp) - (suppress-keymap pbp-mode-map 'all) ;; (define-key pbp-mode-map [(button2)] 'pbp-button-action) - (proof-define-keys pbp-mode-map proof-universal-keys) (erase-buffer))) +(eval-and-compile +(define-derived-mode proof-response-mode proof-universal-keys-only-mode + "PGResp" "Responses from Proof Assistant" + (setq proof-buffer-type 'response))) diff --git a/generic/proof.el b/generic/proof.el index 16149937..1d6580bc 100644 --- a/generic/proof.el +++ b/generic/proof.el @@ -103,6 +103,18 @@ The argument KBL is a list of tuples (k . f) where `k' is a keybinding ;; (insert "\n")))) +(defun proof-display-and-keep-buffer (buffer) + "Display BUFFER and mark window as dedicated." + (display-buffer buffer) + (set-window-dedicated-p (get-buffer-window buffer) 'dedicated)) + +(defun proof-clean-buffer (buffer) + "Erase buffer and hide from display." + (save-excursion + (set-buffer buffer) + (erase-buffer)) + (delete-windows-on buffer)) + ;;; ;;; Global variables ;;; diff --git a/lego/lego-syntax.el b/lego/lego-syntax.el index 20b0a326..f3a8f767 100644 --- a/lego/lego-syntax.el +++ b/lego/lego-syntax.el @@ -1,6 +1,6 @@ -;; lego-fontlock.el Font lock expressions for LEGO -;; Copyright (C) 1994, 1995, 1996, 1997 LFCS Edinburgh. -;; Author: Healfdene Goguen, Thomas Kleymann and Dilip Sequeira +;; lego-syntax.el Syntax of LEGO +;; Copyright (C) 1994 - 1998 LFCS Edinburgh. +;; Author: Thomas Kleymann and Dilip Sequeira ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> ;; Please let us know if you could maintain this package! ;; @@ -63,7 +63,7 @@ (list ; lambda binders - (list (lego-decl-defn-regexp "[:|]") 1 + (list (lego-decl-defn-regexp "[:|?]") 1 'proof-declaration-name-face) ; let binders diff --git a/lego/lego.el b/lego/lego.el index 869cf50a..3674979d 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -10,6 +10,8 @@ ;; (require 'proof) +(require 'proof-script) +(require 'proof-shell) (require 'lego-syntax) ;; FIXME: outline should be autoloaded @@ -178,10 +180,17 @@ (easy-menu-change (list proof-mode-name) (car proof-help-menu) (append (cdr proof-help-menu) lego-help-menu-list))) +(eval-and-compile + (define-derived-mode lego-response-mode proof-response-mode + "LEGOResp" nil + (setq font-lock-keywords lego-font-lock-terms) + (proof-response-config-done))) + (define-derived-mode lego-pbp-mode pbp-mode - "pbp" nil + "LEGOGoals" "LEGO Proof State" (lego-pbp-mode-config)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Code that's lego specific ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -354,9 +363,10 @@ ))))) (defun lego-pre-shell-start () - (setq proof-prog-name lego-prog-name) - (setq proof-mode-for-shell 'lego-shell-mode) - (setq proof-mode-for-pbp 'lego-pbp-mode)) + (setq proof-prog-name lego-prog-name + proof-mode-for-shell 'lego-shell-mode + proof-mode-for-response 'lego-response-mode + proof-mode-for-pbp 'lego-pbp-mode)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Configuring proof and pbp mode and setting up various utilities ;; @@ -365,7 +375,7 @@ (defun lego-init-syntax-table () "Set appropriate values for syntax table in current buffer." - (modify-syntax-entry ?_ "_") + (modify-syntax-entry ?_ "w") (modify-syntax-entry ?\' "_") (modify-syntax-entry ?\| ".") (modify-syntax-entry ?\* ". 23") @@ -525,7 +535,9 @@ We assume that module identifiers coincide with file names." (defun lego-pbp-mode-config () (setq pbp-change-goal "Next %s;" - pbp-error-regexp lego-error-regexp - )) + pbp-error-regexp lego-error-regexp) + (setq font-lock-keywords lego-font-lock-terms) + (proof-goals-config-done)) + (provide 'lego) @@ -59,6 +59,8 @@ C Remove "FIXME notes" which are just notes I've put in about old C Check on all FIXME notes. +C Toolbar icon for `proof-execute-minibuffer-cmd' + A* Fixup for non-script buffer locking: proof-locked-end called from wrong buffer when error message @@ -125,14 +127,6 @@ B Implement more generic mechanism for large undos (4h tms) LEGO: consider Discharge; perhaps unrol to the beginning of the module? -A New buffer model (4h tms): - - 1. Script buffers - 2. Response buffer - 3. (optionally part of response buffer) goals buffer - 4. (hidden) process buffer - 5. Minibuffer for additionally sending information to the process - A Revise ProofGeneral.texi and publish LaTeX version as an LFCS Technical Report (2 days; da + tms) |