diff options
| -rw-r--r-- | coq/coq.el | 4 | ||||
| -rw-r--r-- | generic/proof-config.el | 5 | ||||
| -rw-r--r-- | generic/proof-indent.el | 6 | ||||
| -rw-r--r-- | generic/proof-script.el | 39 | ||||
| -rw-r--r-- | generic/proof-shell.el | 21 | ||||
| -rw-r--r-- | generic/proof-site.el | 12 | ||||
| -rw-r--r-- | generic/proof-splash.el | 4 | ||||
| -rw-r--r-- | generic/proof-syntax.el | 1 | ||||
| -rw-r--r-- | generic/proof-toolbar.el | 53 | ||||
| -rw-r--r-- | generic/proof.el | 74 | ||||
| -rw-r--r-- | generic/span-extent.el | 8 | ||||
| -rw-r--r-- | isa/isa-syntax.el | 1 | ||||
| -rw-r--r-- | isa/isa.el | 7 | ||||
| -rw-r--r-- | isa/thy-mode.el | 1 | ||||
| -rw-r--r-- | lego/lego.el | 4 | ||||
| -rw-r--r-- | todo | 14 |
16 files changed, 157 insertions, 97 deletions
@@ -6,9 +6,11 @@ ;; $Id$ +(require 'proof) (require 'coq-syntax) + +;; FIXME: outline and info should be autoloaded. (require 'outline) -(require 'proof) (require 'info) ; Configuration diff --git a/generic/proof-config.el b/generic/proof-config.el index c342631e..bec16319 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1,4 +1,4 @@ -;; proof-config.el Proof General configuration for proof assistant. +;; proof-config.el Proof General configuration for proof assistant ;; ;; Copyright (C) 1994 - 1998 LFCS Edinburgh. ;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen, @@ -628,5 +628,8 @@ data triggered by `proof-shell-retract-files-regexp'." + + + ;; End of proof-config.el (provide 'proof-config) diff --git a/generic/proof-indent.el b/generic/proof-indent.el index 515c304f..74638bef 100644 --- a/generic/proof-indent.el +++ b/generic/proof-indent.el @@ -5,9 +5,11 @@ ;; ;; $Id$ ;; +;; FIXME: byte compile complains about not knowing +;; proof-script-buffer-list, proof-goto-end-of-locked, +;; proof-locked-end -(require 'cl) -(require 'proof-syntax) +(require 'proof) (defvar proof-stack-to-indent nil "Prover-specific code for indentation.") diff --git a/generic/proof-script.el b/generic/proof-script.el index d5ad9587..4486ab9a 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -9,7 +9,16 @@ ;; $Id$ ;; -(require 'proof-config) +(require 'proof) +(require 'proof-syntax) +(require 'proof-indent) + +;; Spans are our abstraction of extents/overlays. +(cond ((fboundp 'make-extent) (require 'span-extent)) + ((fboundp 'make-overlay) (require 'span-overlay))) + +(eval-when-compile + (require 'func-menu)) ;; ;; Internal variables used by script mode @@ -23,26 +32,6 @@ (defvar proof-terminal-string nil "End-of-line string for proof process.") -(defvar proof-marker nil - "Marker in proof shell buffer pointing to previous command input.") - -(defvar proof-shell-buffer nil - "Process buffer where the proof assistant is run.") - -(defvar proof-script-buffer-list nil - "Scripting buffers with locked regions. -The first element is current and in scripting minor mode. -The cdr of the list of corresponding file names is a subset of -`proof-included-files-list'.") - -(defvar proof-pbp-buffer nil - "The goals buffer (also known as the pbp buffer).") - -(defvar proof-response-buffer nil - "The response buffer.") - -(deflocal proof-buffer-type nil - "Symbol indicating the type of this buffer: 'script, 'shell, or 'pbp.") (defvar proof-action-list nil "action list") @@ -69,7 +58,7 @@ name. Moves point after the match. The package fume-func provides the function `fume-match-find-next-function-name' with the same specification. -However, fume-func's version is incorrec" +However, fume-func's version is incorrect" ;; DO NOT USE save-excursion; we need to move point! ;; save-excursion is called at a higher level in the func-menu ;; package @@ -1360,9 +1349,11 @@ sent to the assistant." ;; sml-mode. ;; FIXME: add more doc to the mode below, to give hints on ;; configuring for new assistants. + +;;;###autoload (define-derived-mode proof-mode fundamental-mode proof-mode-name - "Proof General major mode for proof scripts. + "Proof General major mode class for proof scripts. \\{proof-mode-map}" (setq proof-buffer-type 'script) @@ -1467,7 +1458,7 @@ finish setup which depends on specific proof assistant configuration." (setq indent-line-function 'proof-indent-line) ;; Toolbar - (if (featurep 'proof-toolbar) + (if (featurep 'toolbar) (proof-toolbar-setup)) ;; Menu diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 24bb5bef..2fb74034 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -9,7 +9,7 @@ ;; $Id$ ;; -(require 'proof-config) +(require 'proof) ;; Internal variables used by shell mode ;; @@ -22,6 +22,11 @@ Set in proof-shell-mode.") "Regexp matching terminator, comment start, or comment end. Set in proof-shell-mode.") +(defvar proof-marker nil + "Marker in proof shell buffer pointing to previous command input.") + + + @@ -35,11 +40,6 @@ Set in proof-shell-mode.") ;; ;; -(defvar proof-shell-busy nil - "A lock indicating that the proof shell is processing. -When this is non-nil, proof-shell-ready-prover will give -an error.") - ;; ;; History of these horrible functions. ;; @@ -351,9 +351,6 @@ The default value is \"\n\" to match up to the end of the line.") (defvar proof-shell-delayed-output nil "Last interesting output from proof process output and what to do with it.") -(defvar proof-shell-proof-completed nil - "Flag indicating that a completed proof has just been observed.") - (defvar proof-analyse-using-stack nil "Are annotations sent by proof assistant local or global") @@ -933,9 +930,11 @@ how far we've got." ;; Proof General shell mode definition ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; This has to come after proof-mode is defined +;; OLD COMMENT: "This has to come after proof-mode is defined" + +;;###autoload (define-derived-mode proof-shell-mode comint-mode - "proof-shell" "Proof shell mode - not standalone" + "proof-shell" "Proof General shell mode class for proof assistant processes" (setq proof-buffer-type 'shell) (setq proof-shell-busy nil) (setq proof-shell-delayed-output (cons 'insert "done")) diff --git a/generic/proof-site.el b/generic/proof-site.el index d88d2324..ea3b7198 100644 --- a/generic/proof-site.el +++ b/generic/proof-site.el @@ -132,6 +132,18 @@ NOTE: to change proof assistant, you must start a new Emacs session.") (setq load-path (cons proof-lisp-path load-path)))) +;; During compilation from the Makefile, generic is on the load path. +;; Add all of the prover directories. +;; FIXME: this doesn't work quite right. We want to test +;; whether we are running during a compilation. How? +; (eval-when-compile +; (dolist (assistant proof-internal-assistant-table) +; (let ((path (concat proof-internal-home-directory +; (concat (symbol-name (car assistant)) "/")))) +; (or (member path load-path) +; (setq load-path +; (cons path load-path)))))) + ;; Now add auto-loads and load-path elements to support the ;; proof assistants selected, and define a stub (let ((assistants proof-assistants) assistant) diff --git a/generic/proof-splash.el b/generic/proof-splash.el index f5e83ee3..9f83e936 100644 --- a/generic/proof-splash.el +++ b/generic/proof-splash.el @@ -157,7 +157,9 @@ Only do it if proof-splash-display is nil." ;; redisplay until proof-internal-display-splash-time has elapsed. ;; Display the screen ASAP... -(proof-splash-display-screen) +;; FIXME: don't want this to display during compilation! +(eval-when (load) + (proof-splash-display-screen)) (defun proof-splash-timeout-waiter () "Wait for proof-splash-timeout, then remove self from hook." diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el index 265791db..9ea7ee56 100644 --- a/generic/proof-syntax.el +++ b/generic/proof-syntax.el @@ -6,6 +6,7 @@ ;; $Id$ ;; + (require 'font-lock) ;;; FIXME: change this to proof- diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el index f562ed14..68c73834 100644 --- a/generic/proof-toolbar.el +++ b/generic/proof-toolbar.el @@ -10,7 +10,12 @@ ;; Toolbar is just for scripting buffer at the moment. ;; -(require 'proof-config) +(require 'proof-script) +(require 'proof-shell) + +;; FIXME: would be nice to have proof-shell autoloaded when shell is +;; actually started. Need to fixup references to variables here to be +;; autoloaded functions from proof-shell, and remove from enablers. (defcustom proof-toolbar-wanted t "*Whether to use toolbar in proof mode." @@ -31,6 +36,20 @@ This gives a bare toolbar that works for any prover. To add prover specific buttons, see proof-toolbar.el.") +(defconst proof-toolbar-iconlist + '((proof-toolbar-next-icon "next") + (proof-toolbar-undo-icon "undo") + (proof-toolbar-retract-icon "retract") + (proof-toolbar-use-icon "use") + (proof-toolbar-goal-icon "goal") + (proof-toolbar-qed-icon "qed") + (proof-toolbar-restart-icon "restart")) + "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-internal-images-directory. The toolbar +code expects to find files IMAGE.xbm, IMAGE.xpm, IMAGE.8bit.xpm +and chooses the best one for the display properites.") + (defvar proof-toolbar-button-list proof-toolbar-default-button-list "A toolbar descriptor evaluated in proof-toolbar-setup. Specifically, a list of sexps which evaluate to entries in a toolbar @@ -40,15 +59,25 @@ will work for any proof assistant.") (defvar proof-toolbar nil "Proof mode toolbar button list. Set in proof-toolbar-setup.") +(defconst proof-old-toolbar default-toolbar + "Saved value of default-toolbar for proofmode.") + + ;; FIXME: edit-toolbar cannot edit proof toolbar (even in a proof mode) ;; Need a variable containing a specifier or similar. -; (defvar proof-toolbar-specifier nil -; "Specifier for proof toolbar.") +;; (defvar proof-toolbar-specifier nil +;; "Specifier for proof toolbar.") +;; This doesn't seem worth fixing until XEmacs toolbar implementation +;; settles a bit. Enablers don't work too well at the moment. +;; FIXME: could automatically defvar the icon variables. + +;;; ###autoload (defun proof-toolbar-setup () - "Initialize proof-toolbar and enable it for the current buffer. + "Initialize Proof General toolbar and enable it for the current buffer. If proof-mode-use-toolbar is nil, change the current buffer toolbar to the default toolbar." + (interactive) (if (and proof-toolbar-wanted ;; NB for FSFmacs use window-system, not console-type @@ -74,9 +103,6 @@ to the default toolbar." (set-specifier default-toolbar proof-toolbar (current-buffer))) (set-specifier default-toolbar proof-old-toolbar (current-buffer)))) -(defconst proof-old-toolbar default-toolbar - "Saved value of default-toolbar for proofmode.") - ;; ;; GENERIC PROOF TOOLBAR BUTTONS ;; @@ -186,16 +212,6 @@ Initialised in proof-toolbar-setup.") ;; (proof-toolbar-qed-enable-p) "Save proved theorem"]) -(defconst proof-toolbar-iconlist - '((proof-toolbar-next-icon "next") - (proof-toolbar-undo-icon "undo") - (proof-toolbar-retract-icon "retract") - (proof-toolbar-use-icon "use") - (proof-toolbar-goal-icon "goal") - (proof-toolbar-qed-icon "qed") - (proof-toolbar-restart-icon "restart")) - "List of icon variable names and their associated image files") - ;; ;; GENERIC PROOF TOOLBAR FUNCTIONS ;; @@ -280,6 +296,7 @@ Move point if the end of the locked position is invisible." "Insert a save theorem command into the script buffer, issue it." (interactive) (if (proof-toolbar-qed-enable-p) - (call-interactively 'proof-issue-save))) + (call-interactively 'proof-issue-save) + (error "I can't see a completed proof!"))) ;; (provide 'proof-toolbar)
\ No newline at end of file diff --git a/generic/proof.el b/generic/proof.el index 890c5275..bd4669a6 100644 --- a/generic/proof.el +++ b/generic/proof.el @@ -1,4 +1,4 @@ -;; proof.el Proof General loader. +;; proof.el Proof General loader. All files require this one. ;; ;; Copyright (C) 1994 - 1998 LFCS Edinburgh. ;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen, @@ -15,26 +15,16 @@ (require 'proof-site) ; site config -(require 'proof-config) ; variables +(require 'proof-config) ; configuration variables (require 'proof-splash) ; splash screen -;; FIXME da: I think these ones should be autoloaded!! -(require 'cl) -(require 'compile) -(require 'comint) -(require 'etags) -(require 'easymenu) - - -;; Spans are our abstraction of extents/overlays. -(cond ((fboundp 'make-extent) (require 'span-extent)) - ((fboundp 'make-overlay) (require 'span-overlay)) - (t nil)) - -(require 'proof-syntax) -(require 'proof-indent) - +;; FIXME da: I think these should all be autoloaded!! +;; (require 'cl) +;; (require 'compile) +;; (require 'comint) +;; (require 'etags) +;; (require 'easymenu) ;; browse-url function doesn't seem to be autoloaded in ;; XEmacs 20.4, but it is in FSF Emacs 20.2. @@ -42,6 +32,22 @@ (autoload 'browse-url "browse-url" "Ask a WWW browser to load URL." t)) +;;; Autoloads for main code + +(autoload 'proof-mode "proof-script" + "Proof General major mode class for proof scripts.") + +(autoload 'proof-shell-mode "proof-shell" + "Proof General shell mode class for proof assistant processes") + +(if (featurep 'toolbar) + (autoload 'proof-toolbar-setup "proof-toolbar" + "Initialize Proof General and enable it for the current buffer" t)) + +;;; +;;; Utilities/macros used in several files +;;; + (defmacro deflocal (var value &optional docstring) "Define a buffer local variable VAR with default value VALUE." (list 'progn @@ -49,15 +55,35 @@ (list 'make-variable-buffer-local (list 'quote var)) (list 'setq-default var value))) +;;; +;;; Global variables +;;; -;; Load toolbar code if toolbars available. -(if (featurep 'toolbar) - (require 'proof-toolbar)) +(deflocal proof-buffer-type nil + "Symbol indicating the type of this buffer: 'script, 'shell, or 'pbp.") + +(defvar proof-shell-busy nil + "A lock indicating that the proof shell is processing. +When this is non-nil, proof-shell-ready-prover will give +an error.") + +(defvar proof-script-buffer-list nil + "Scripting buffers with locked regions. +The first element is current and in scripting minor mode. +The cdr of the list of corresponding file names is a subset of +`proof-included-files-list'.") + +(defvar proof-shell-buffer nil + "Process buffer where the proof assistant is run.") + +(defvar proof-pbp-buffer nil + "The goals buffer (also known as the pbp buffer).") -;; Main code is in these files -(require 'proof-script) -(require 'proof-shell) +(defvar proof-response-buffer nil + "The response buffer.") +(defvar proof-shell-proof-completed nil + "Flag indicating that a completed proof has just been observed.") (provide 'proof) ;; proof.el ends here diff --git a/generic/span-extent.el b/generic/span-extent.el index 91ad6ac9..db1a70cd 100644 --- a/generic/span-extent.el +++ b/generic/span-extent.el @@ -31,6 +31,10 @@ "Set the end point of SPAN to VALUE." (set-extent-endpoints span (extent-start-position span) value)) +(defsubst set-span-property (span name value) + "Set SPAN's property NAME to VALUE." + (set-extent-property span name value)) + (defsubst span-read-only (span) "Set SPAN to be read only." (set-span-property span 'read-only t)) @@ -43,10 +47,6 @@ "Return SPAN's value for property PROPERTY." (extent-property span name)) -(defsubst set-span-property (span name value) - "Set SPAN's property NAME to VALUE." - (set-extent-property span name value)) - (defsubst delete-span (span) "Delete SPAN." (delete-extent span)) diff --git a/isa/isa-syntax.el b/isa/isa-syntax.el index 93ad9758..07373805 100644 --- a/isa/isa-syntax.el +++ b/isa/isa-syntax.el @@ -9,7 +9,6 @@ (require 'proof-syntax) - ;;; Proof mode customization: how should it work? ;;; Presently we have a bunch of variables in proof.el which are ;;; set from a bunch of similarly named variables in <engine>-syntax.el. @@ -9,11 +9,14 @@ ;; -(require 'isa-syntax) -(require 'outline) (setq proof-tags-support nil) ; we don't want it, no isatags prog. (require 'proof) +(require 'isa-syntax) + +;; FIXME: outline should be autoloaded +(require 'outline) + ;;; ;;; ======== User settings for Isabelle ======== diff --git a/isa/thy-mode.el b/isa/thy-mode.el index 57568a63..641be424 100644 --- a/isa/thy-mode.el +++ b/isa/thy-mode.el @@ -10,6 +10,7 @@ ;; NAMESPACE management: all functions and variables declared ;; in this file begin with isa-thy- +(require 'proof-site) (require 'isa) ;;; ========== Theory File Mode User Options ========== diff --git a/lego/lego.el b/lego/lego.el index f0564857..2ea0594e 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -9,9 +9,11 @@ ;; $Id$ ;; +(require 'proof) (require 'lego-syntax) + +;; FIXME: outline should be autoloaded (require 'outline) -(require 'proof) ;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; User Configuration ;;; @@ -14,6 +14,13 @@ X (Low) probably not worth wasting time on * This is a list of things which need doing in the generic interface ==================================================================== +A byte-compilation: continue fixups for clean byte compile. + Need to compile from clean Emacs to see proper warnings. + Unfortunately I get odd Arithmetic Errors when comiling. + Check that byte compilation (and compiled code!) + works for both varieties of Emacs. Add instructions to INSTALL on + how to byte compile. Fill out Makefile.dist (2hr da) + C Remove "FIXME notes" which are just notes I've put in about old code in case something breaks (da, 30mins). @@ -26,9 +33,6 @@ A* Fixup for non-script buffer locking: proof-restart-script is now broken (2h da) -A* Fixup for clean byte compile now that proof.el has been split. - (30min da) - A* Fixup multiple files -- needs debugging. 1. mark atomic makes some assumption about non-comment commands in @@ -44,10 +48,6 @@ A* Fixup multiple files -- needs debugging. B Improve web pages after suggestions in doc/notes.txt (da, 1.5hrs) -C byte-compilation: check that byte compilation (and compiled code!) - works for both varieties of Emacs. Add instructions to INSTALL on - how to byte compile. (1hr) - C Remove .gif, .jpg, .xpm, .xbm files from the CVS repository. Add .cvsignore's for them instead. Disadvantage: developers will need to have the Gimp installed to build them via 'make images' |