diff options
| -rw-r--r-- | generic/pg-metadata.el | 2 | ||||
| -rw-r--r-- | generic/pg-pgip.el | 2 | ||||
| -rw-r--r-- | generic/pg-user.el | 2 | ||||
| -rw-r--r-- | generic/proof-depends.el | 8 | ||||
| -rw-r--r-- | generic/proof-easy-config.el | 2 | ||||
| -rw-r--r-- | generic/proof-splash.el | 2 | ||||
| -rw-r--r-- | generic/proof-toolbar.el | 116 | ||||
| -rw-r--r-- | generic/proof-utils.el | 2 | ||||
| -rw-r--r-- | generic/proof.el | 2 |
9 files changed, 71 insertions, 67 deletions
diff --git a/generic/pg-metadata.el b/generic/pg-metadata.el index 21cbac9c..e43ccd08 100644 --- a/generic/pg-metadata.el +++ b/generic/pg-metadata.el @@ -1,6 +1,6 @@ ;; pg-metadata.el Persistant storage of metadata for proof scripts ;; -;; Copyright (C) 2001 LFCS Edinburgh. +;; Copyright (C) 2001-2 LFCS Edinburgh. ;; Author: David Aspinall ;; Maintainer: Proof General maintainer <proofgen@dcs.ed.ac.uk> ;; diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el index 327000d6..0c8dbeef 100644 --- a/generic/pg-pgip.el +++ b/generic/pg-pgip.el @@ -1,6 +1,6 @@ ;; pg-pgip.el Functions for processing PGIP for Proof General ;; -;; Copyright (C) 200-2001 LFCS Edinburgh. +;; Copyright (C) 2000-2002 LFCS Edinburgh. ;; ;; Author: David Aspinall <da@dcs.ed.ac.uk> ;; diff --git a/generic/pg-user.el b/generic/pg-user.el index 7b22ad48..8f930382 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -1,6 +1,6 @@ ;; pg-user.el User level commands for Proof General ;; -;; Copyright (C) 2000-2001 LFCS Edinburgh. +;; Copyright (C) 2000-2002 LFCS Edinburgh. ;; Author: David Aspinall and others ;; Maintainer: Proof General maintainer <proofgen@dcs.ed.ac.uk> ;; diff --git a/generic/proof-depends.el b/generic/proof-depends.el index 67a1f586..7182d1bc 100644 --- a/generic/proof-depends.el +++ b/generic/proof-depends.el @@ -1,6 +1,6 @@ -;; proof-depends.el Managing theorem-theorem and theorem-definition dependencies. +;; proof-depends.el Theorem-theorem and theorem-definition dependencies. ;; -;; Copyright (C) 2000,1 University of Edinburgh. +;; Copyright (C) 2000-2002 University of Edinburgh. ;; Authors: Fiona McNeill, David Aspinall. ;; ;; Status: Experimental code @@ -8,8 +8,8 @@ ;; ;; $Id$ ;; -;; Based on Fiona McNeill's MSc project on analysing dependencies within proofs. -;; Code rewritten by David Aspinall. +;; Based on Fiona McNeill's MSc project on analysing dependencies +;; within proofs. Code rewritten by David Aspinall. ;; ;; Variables diff --git a/generic/proof-easy-config.el b/generic/proof-easy-config.el index a6a501f6..d948f3b4 100644 --- a/generic/proof-easy-config.el +++ b/generic/proof-easy-config.el @@ -1,6 +1,6 @@ ;; proof-easy-config.el Easy configuration for Proof General ;; -;; Copyright (C) 1999-2001 David Aspinall / LFCS. +;; Copyright (C) 1999-2002 David Aspinall / LFCS. ;; Author: David Aspinall <da@dcs.ed.ac.uk> ;; Maintainer: Proof General maintainer <proofgen@dcs.ed.ac.uk> ;; diff --git a/generic/proof-splash.el b/generic/proof-splash.el index 98d17d53..0aac6bdd 100644 --- a/generic/proof-splash.el +++ b/generic/proof-splash.el @@ -41,7 +41,7 @@ Proof General." proof-general-version) (match-end 0)) nil - "(C) LFCS, University of Edinburgh, 2001." + "(C) LFCS, University of Edinburgh, 2002." nil nil " Please send problems and suggestions to proofgen@dcs.ed.ac.uk, diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el index c457e49b..8cbe56ad 100644 --- a/generic/proof-toolbar.el +++ b/generic/proof-toolbar.el @@ -87,22 +87,14 @@ (if tooltip (list (list iconvar iconname))))) -(defconst proof-toolbar-iconlist - (apply 'append - (mapcar 'proof-toolbar-make-icon - (proof-ass toolbar-entries))) - "List of icon variable names and their associated image files. -A list of lists of the form (VAR IMAGE). IMAGE is the root name -for an image file in proof-images-directory. The toolbar -code expects to find files IMAGE.xpm or IMAGE.8bit.xpm -and chooses the best one for the display properites.") (defun proof-toolbar-make-toolbar-item (tle) "Make a toolbar button descriptor from a PA-toolbar-entries entry." (let* - ((token (car tle)) - (menuname (cadr tle)) - (tooltip (nth 2 tle)) + ((token (nth 0 tle)) + (includep (or (< (length tle) 5) (eval (nth 4 tle)))) + (menuname (and includep (nth 1 tle))) + (tooltip (and includep (nth 2 tle))) (existsenabler (nth 3 tle)) (enablep (and proof-toolbar-use-button-enablers (>= emacs-major-version 21) @@ -130,16 +122,6 @@ and chooses the best one for the display properites.") (if enabler (list :enable (list enabler))))))))) -(defvar proof-toolbar-button-list - (append - (apply 'append (mapcar 'proof-toolbar-make-toolbar-item - (proof-ass toolbar-entries))) - (if proof-running-on-XEmacs - (list [:style 3d]))) - "A toolbar descriptor evaluated in proof-toolbar-setup. -Specifically, a list of sexps which evaluate to entries in a toolbar -descriptor. The default value proof-toolbar-default-button-list -will work for any proof assistant.") ;; ;; Code for displaying and refreshing toolbar @@ -200,13 +182,36 @@ to the default toolbar." (defun proof-toolbar-build () "Build proof-toolbar." - (let ((icontype - ;; Select 8bit xpm's if we've got a - ;; limited colour depth. - (if (and (boundp 'device-pixel-depth) - (< (device-pixel-depth) 16)) - ".8bit.xpm" ".xpm"))) - + (let + ((icontype (if (and (boundp 'device-pixel-depth) + (< (device-pixel-depth) 16)) + ;; Select 8bit xpm's if we've got a + ;; limited colour depth. + ".8bit.xpm" ".xpm")) + + (proof-toolbar-icon-list + ;; List of icon variable names and their associated image + ;; files. A list of lists of the form (VAR IMAGE). IMAGE is + ;; the root name for ;an image file in proof-images-directory. + ;; The toolbar code expects to find files IMAGE.xpm or + ;; IMAGE.8bit.xpm and chooses the best one for the display + ;; properites. + (apply 'append + (mapcar 'proof-toolbar-make-icon + (proof-ass toolbar-entries)))) + + (proof-toolbar-button-list + ;; A toolbar descriptor evaluated in proof-toolbar-setup. + ;; Specifically, a list of sexps which evaluate to entries in + ;; a toolbar descriptor. The default value + ;; proof-toolbar-default-button-list will work for any proof + ;; assistant. + (append + (apply 'append (mapcar 'proof-toolbar-make-toolbar-item + (proof-ass toolbar-entries))) + (if proof-running-on-XEmacs + (list [:style 3d]))))) + ;; First set the button variables to glyphs. ;; (NB: this is a bit long-winded). (mapcar @@ -223,30 +228,26 @@ to the default toolbar." ;; On GNU emacs, it holds a filename for the icon, ;; without path or extension. (eval (cadr buttons)))))) - ;; On GNU Emacs, it holds an image descriptor or vector of - ;;(if (> 1 (length iconfiles)) - ;; (apply 'vector (mapcar 'create-image iconfiles)) - ;; (create-image (car iconfiles))))))) - proof-toolbar-iconlist)) - - (if proof-running-on-XEmacs - ;; For XEmacs, we evaluate the specifier. - (setq proof-toolbar (mapcar 'eval proof-toolbar-button-list)) - - ;; On GNU emacs, we need to make a new "key"map, - ;; and set a local copy of tool-bar-map to it. - (setq proof-toolbar (make-sparse-keymap)) - (let ((tool-bar-map proof-toolbar) - (load-path (list proof-images-directory))) ; for finding images - (dolist (but proof-toolbar-button-list) - (apply - 'tool-bar-add-item - (eval (nth 0 but)) ; image filename - (nth 1 but) ; function symbol - (nth 2 but) ; dummy key - (nthcdr 3 but))))) ; remaining properties + proof-toolbar-icon-list) + + (if proof-running-on-XEmacs + ;; For XEmacs, we evaluate the specifier. + (setq proof-toolbar (mapcar 'eval proof-toolbar-button-list)) + + ;; On GNU emacs, we need to make a new "key"map, + ;; and set a local copy of tool-bar-map to it. + (setq proof-toolbar (make-sparse-keymap)) + (let ((tool-bar-map proof-toolbar) + (load-path (list proof-images-directory))) ; for finding images + (dolist (but proof-toolbar-button-list) + (apply + 'tool-bar-add-item + (eval (nth 0 but)) ; image filename + (nth 1 but) ; function symbol + (nth 2 but) ; dummy key + (nthcdr 3 but))))) ; remaining properties ;; Finished - ) + )) ;; Action to take after altering proof-toolbar-enable @@ -447,9 +448,11 @@ changed state." ;; (defun proof-toolbar-goal-enable-p () - ;; Goals are always allowed: will crank up process if need be. - ;; Actually this should only be available when "no subgoals" - t) + ;; Goals are always allowed, provided proof-goal-command is set. + ;; Will crank up process if need be. + ;; (Actually this should only be available when "no subgoals") + proof-goal-command) + (defalias 'proof-toolbar-goal 'proof-issue-goal) @@ -460,7 +463,8 @@ changed state." (defun proof-toolbar-qed-enable-p () (proof-with-script-buffer - (and proof-shell-proof-completed + (and proof-save-command + proof-shell-proof-completed (proof-shell-available-p)))) (defalias 'proof-toolbar-qed 'proof-issue-save) diff --git a/generic/proof-utils.el b/generic/proof-utils.el index 4b825adf..eba356c8 100644 --- a/generic/proof-utils.el +++ b/generic/proof-utils.el @@ -1,6 +1,6 @@ ;; proof-utils.el Proof General utility functions ;; -;; Copyright (C) 1998-2001 LFCS Edinburgh. +;; Copyright (C) 1998-2002 LFCS Edinburgh. ;; ;; Author: David Aspinall <da@dcs.ed.ac.uk> and others ;; Maintainer: Proof General maintainer <proofgen@dcs.ed.ac.uk> diff --git a/generic/proof.el b/generic/proof.el index 40d77733..2578259c 100644 --- a/generic/proof.el +++ b/generic/proof.el @@ -1,6 +1,6 @@ ;; proof.el Proof General loader. All files require this one. ;; -;; Copyright (C) 1998-2000 LFCS Edinburgh. +;; Copyright (C) 1998-2002 LFCS Edinburgh. ;; ;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen, ;; Thomas Kleymann and Dilip Sequeira |