aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2010-08-08 13:42:31 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2010-08-08 13:42:31 +0000
commit95d8a7f7364fde5af433ffa0e6c9f5bf664c5ebc (patch)
tree9be997d4d9af9c12882d53434d8dbbcb49cbdcb6
parent0877b91645ec1a824eba51cf0ad46eb4d76a138f (diff)
Checkdoc cleanups
Diffstat
-rw-r--r--generic/pg-assoc.el5
-rw-r--r--generic/pg-autotest.el39
-rw-r--r--generic/pg-custom.el38
-rw-r--r--generic/pg-movie.el23
-rw-r--r--generic/pg-pbrpm.el8
-rw-r--r--generic/pg-pgip.el17
-rw-r--r--generic/pg-response.el24
-rw-r--r--generic/pg-thymodes.el97
-rw-r--r--generic/pg-user.el7
-rw-r--r--generic/pg-vars.el15
-rw-r--r--generic/proof-config.el26
-rw-r--r--generic/proof-depends.el30
-rw-r--r--generic/proof-faces.el4
-rw-r--r--generic/proof-indent.el15
-rw-r--r--generic/proof-maths-menu.el14
-rw-r--r--generic/proof-menu.el33
-rw-r--r--generic/proof-mmm.el20
-rw-r--r--generic/proof-script.el73
-rw-r--r--generic/proof-shell.el100
-rw-r--r--generic/proof-site.el16
-rw-r--r--generic/proof-splash.el12
-rw-r--r--generic/proof-syntax.el6
-rw-r--r--generic/proof-toolbar.el9
-rw-r--r--generic/proof-useropts.el6
-rw-r--r--generic/proof-utils.el26
25 files changed, 320 insertions, 343 deletions
diff --git a/generic/pg-assoc.el b/generic/pg-assoc.el
index 51633afe..7bb6146d 100644
--- a/generic/pg-assoc.el
+++ b/generic/pg-assoc.el
@@ -1,15 +1,16 @@
;;; pg-assoc.el --- Functions for associated buffers
;;
-;; Copyright (C) 1994-2008 LFCS Edinburgh.
+;; Copyright (C) 1994-2008, 2010 LFCS Edinburgh.
;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen,
;; Thomas Kleymann and Dilip Sequeira
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;
;; $Id$
;;
+;;; Commentary:
;;
;; Defines an empty mode inherited by modes of the associated buffers.
-;;
+;;
;;; Code:
diff --git a/generic/pg-autotest.el b/generic/pg-autotest.el
index 8a1b74c8..fb52ebf1 100644
--- a/generic/pg-autotest.el
+++ b/generic/pg-autotest.el
@@ -1,6 +1,6 @@
;;; pg-autotest.el --- Simple testing framework for Proof General
;;
-;; Copyright (C) 2005, 2009 LFCS Edinburgh, David Aspinall.
+;; Copyright (C) 2005, 2009-10 LFCS Edinburgh, David Aspinall.
;; Authors: David Aspinall
;;
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
@@ -27,7 +27,7 @@
"Flag indicating overall successful state of tests.")
(defvar pg-autotest-log t
- "Value for 'standard-output' during tests")
+ "Value for 'standard-output' during tests.")
(setq debug-on-error t) ;; enable in case a test goes wrong
@@ -58,16 +58,16 @@
(progn
(setq standard-output pg-autotest-log)
(condition-case err
- (let ((scaffoldfn
- (intern (concat "pg-autotest-"
+ (let ((scaffoldfn
+ (intern (concat "pg-autotest-"
(symbol-name (quote ,fn))))))
(if (fboundp scaffoldfn)
(apply scaffoldfn (list ,@args))
- (pg-autotest-message
- "TEST: %s"
- (prin1-to-string (cons (quote ,fn)
+ (pg-autotest-message
+ "TEST: %s"
+ (prin1-to-string (cons (quote ,fn)
(quote ,args))))
- (apply (intern (concat "pg-autotest-test-"
+ (apply (intern (concat "pg-autotest-test-"
(symbol-name (quote ,fn))))
(list ,@args))))
(error
@@ -89,7 +89,7 @@
(defun pg-autotest-message (msg &rest args)
"Give message MSG in log file output and on display."
(let ((fmsg (if args (apply 'format msg args) msg)))
- (proof-with-current-buffer-if-exists
+ (proof-with-current-buffer-if-exists
pg-autotest-log
(insert fmsg "\n"))
(message fmsg)
@@ -106,17 +106,17 @@
(defun pg-autotest-timetaken (&optional clockname)
"Report time since (startclock CLOCKNAME)."
(let* ((timestart (get 'pg-autotest-time (or clockname 'local)))
- (timetaken
+ (timetaken
(time-subtract (current-time) timestart)))
(pg-autotest-message
- "TIME: %f (%s)"
+ "TIME: %f (%s)"
(float-time timetaken)
(if clockname (symbol-name clockname)
"this test"))))
(defun pg-autotest-exit ()
"Exit Emacs returning Unix success 0 if all tests succeeded."
- (proof-with-current-buffer-if-exists
+ (proof-with-current-buffer-if-exists
pg-autotest-log
(save-buffer 0))
(kill-emacs (if pg-autotest-success 0 1)))
@@ -132,8 +132,7 @@ An error is signalled if scripting doesn't completely the whole buffer."
(pg-autotest-test-assert-processed file))
(defun pg-autotest-test-script-wholefile (file)
- "Load FILE and script line-by-line, using `proof-shell-wait' before sending
-each line.
+ "Process FILE line-by-line, using `proof-shell-wait'.
An error is signalled if scripting doesn't complete."
(pg-autotest-find-file-restart file)
(save-excursion
@@ -144,13 +143,13 @@ An error is signalled if scripting doesn't complete."
(save-current-buffer
(condition-case err
(proof-assert-next-command-interactive)
- (error
+ (error
(let ((msg (car-safe (cdr-safe err))))
(unless (string-equal msg
- ;; normal user error message at end of buffer
+ ;; normal user error message at end of buffer
"At end of the locked region, nothing to do to!")
- (pg-autotest-message
- "proof-assert-next-command-interactive hit an error: %s"
+ (pg-autotest-message
+ "proof-assert-next-command-interactive hit an error: %s"
msg)))))
(proof-shell-wait))
(goto-char (proof-queue-or-locked-end))
@@ -165,7 +164,7 @@ completely processing the buffer as the last step."
(while (> jumps 0)
(let ((random-point (random (point-max))))
;; TODO: random use of retract/process whole buffer too
- (pg-autotest-message
+ (pg-autotest-message
" random jump to point: %d" random-point)
(goto-char random-point)
(unless (proof-only-whitespace-to-locked-region-p)
@@ -191,7 +190,7 @@ completely processing the buffer as the last step."
(defun pg-autotest-test-assert-full ()
"Check that current buffer has been fully processed."
(unless (proof-locked-region-full-p)
- (error (format "Locked region in buffer `%s' is not full"
+ (error (format "Locked region in buffer `%s' is not full"
(buffer-name)))))
(defun pg-autotest-test-assert-unprocessed (file)
diff --git a/generic/pg-custom.el b/generic/pg-custom.el
index 7457de50..eb8afa3c 100644
--- a/generic/pg-custom.el
+++ b/generic/pg-custom.el
@@ -60,26 +60,26 @@ support depends on whether your proof assistant supports it."
:group 'proof-user-options)
(defconst proof-toolbar-entries-default
- `((state "Display Proof State" "Display the current proof state" t
+`((state "Display Proof State" "Display the current proof state" t
proof-showproof-command)
- (context "Display Context" "Display the current context" t
+ (context "Display Context" "Display the current context" t
proof-context-command)
- (goal "Start a New Proof" "Start a new proof" t nil)
- (retract "Retract Buffer" "Retract (undo) whole buffer" t)
- (undo "Undo Step" "Undo the previous proof command" t t)
- (delete "Delete Step" "Delete the last proof command" t t)
- (next "Next Step" "Process the next proof command" t t)
- (use "Use Buffer" "Process whole buffer" t t)
- (goto "Goto Point" "Process or undo to the cursor position" t t)
- (qed "Finish Proof" "Close/save proved theorem" t nil)
- (home "Goto Locked End" "Goto end of the last command proceesed" t t)
- (find "Find Theorems" "Find theorems" t proof-find-theorems-command)
- (info "Identifier Info" "Information about identifier" t proof-query-identifier-command)
- (command "Issue Command" "Issue a non-scripting command" t t)
- (interrupt "Interrupt Prover" "Interrupt the proof assistant" t t)
- (restart "Restart Scripting" "Restart scripting (clear all locked regions)" t t)
- (visibility "Toggle Visibility" "Show or hide hidden proofs" nil t)
- (help nil "Proof General manual" t t))
+ (goal "Start a New Proof" "Start a new proof" t nil)
+ (retract "Retract Buffer" "Retract (undo) whole buffer" t)
+ (undo "Undo Step" "Undo the previous proof command" t t)
+ (delete "Delete Step" "Delete the last proof command" t t)
+ (next "Next Step" "Process the next proof command" t t)
+ (use "Use Buffer" "Process whole buffer" t t)
+ (goto "Goto Point" "Process or undo to the cursor position" t t)
+ (qed "Finish Proof" "Close/save proved theorem" t nil)
+ (home "Goto Locked End" "Goto end of the last command proceesed" t t)
+ (find "Find Theorems" "Find theorems" t proof-find-theorems-command)
+ (info "Identifier Info" "Information about identifier" t proof-query-identifier-command)
+ (command "Issue Command" "Issue a non-scripting command" t t)
+ (interrupt "Interrupt Prover" "Interrupt the proof assistant" t t)
+ (restart "Restart Scripting" "Restart scripting (clear all locked regions)" t t)
+ (visibility "Toggle Visibility" "Show or hide hidden proofs" nil t)
+ (help nil "Proof General manual" t t))
"Example value for proof-toolbar-entries. Also used to define scripting menu.
This gives a bare toolbar that works for any prover, providing the
appropriate configuration variables are set.
@@ -124,7 +124,7 @@ arguments are -x foo -y bar, then the list should be '(\"-x\" \"foo\"
Each element should be a string of the form ENVVARNAME=VALUE. They will be
added to the environment before launching the prover (but not pervasively).
For example for coq on Windows you might need something like:
-(setq coq-prog-env '(\"HOME=C:\\Program Files\\Coq\\\"))"
+\(setq coq-prog-env '(\"HOME=C:\\Program Files\\Coq\\\"))"
:type '(list string)
:group 'proof-shell)
diff --git a/generic/pg-movie.el b/generic/pg-movie.el
index 72afca03..4e16b112 100644
--- a/generic/pg-movie.el
+++ b/generic/pg-movie.el
@@ -16,12 +16,13 @@
;;
;; Much more could be done to dump the prettified output from the
;; prover, but this is probably not the right way of doing things in
-;; general (one would rather have prover-integrated batch tools).
+;; general (one would rather have prover-integrated batch tools).
;;
;; It does give quick and easy results for provers already supported by
;; Proof General though!
;;
+;;; Code:
(eval-when-compile
(require 'span))
@@ -29,10 +30,10 @@
(defconst pg-movie-xml-header "<?xml version=\"1.0\"?>")
-(defconst pg-movie-stylesheet
+(defconst pg-movie-stylesheet
"<?xml-stylesheet type=\"text/xsl\" href=\"proviola-spp.xsl\"?>")
-(defvar pg-movie-frame 0 "Frame counter for movie")
+(defvar pg-movie-frame 0 "Frame counter for movie.")
(defun pg-movie-of-span (span)
(let* ((cmd (buffer-substring-no-properties
@@ -40,7 +41,7 @@
(helpspan (span-property span 'pg-helpspan))
(resp (and helpspan (span-property helpspan 'response)))
(type (span-property span 'type))
- (class (cond
+ (class (cond
((eq type 'comment) "comment")
((eq type 'proof) "lemma")
((eq type 'goalsave) "lemma")
@@ -48,11 +49,11 @@
(label (span-property span 'rawname))
(frameid (int-to-string pg-movie-frame)))
(incf pg-movie-frame)
- (pg-xml-node frame
+ (pg-xml-node frame
(list (pg-xml-attr frameNumber frameid))
- (list
- (pg-xml-node command
- (append
+ (list
+ (pg-xml-node command
+ (append
(list (pg-xml-attr class class))
(if label (list (pg-xml-attr label label))))
(list cmd))
@@ -64,12 +65,12 @@
(span-mapcar-spans-inorder
'pg-movie-of-span start end 'type))))))
-;;;###autoload
+;;;###autoload
(defun pg-movie-export ()
"Export the movie file from the current script buffer."
(interactive)
(setq pg-movie-frame 0)
- (let ((movie (pg-movie-of-region
+ (let ((movie (pg-movie-of-region
(point-min)
(point-max)))
(movie-file-name
@@ -84,7 +85,7 @@
(xml-print movie)
(write-file movie-file-name t))))
-;;;###autoload
+;;;###autoload
(defun pg-movie-export-from (script)
"Export the movie file that results from processing SCRIPT."
(interactive "f")
diff --git a/generic/pg-pbrpm.el b/generic/pg-pbrpm.el
index e036d7ae..1b287194 100644
--- a/generic/pg-pbrpm.el
+++ b/generic/pg-pbrpm.el
@@ -1,11 +1,13 @@
;; pg-pbrpm.el --- Proof General - Proof By Rules Pop-up Menu - mode.
;;
-;; Copyright (C) 2004, 2009 - Universite de Savoie, France.
+;; Copyright (C) 2004 - Universite de Savoie, France.
;; Authors: Jean-Roch SOTTY, Christophe Raffalli
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;
;; $Id$
;;
+;;; Commentary:
+;;
;; Analyse the goal buffer to produce a popup menu.
;;
;; NB: this code is currently XEmacs specific
@@ -28,6 +30,8 @@
;;
+
+
;;; Code:
(require 'span)
(eval-when-compile
@@ -425,7 +429,7 @@ If no match found, return the empty string."
(defun pg-pbrpm-translate-position (buffer pos)
"return pos if buffer is goals-buffer otherwise, return the point position in
- the goal buffer"
+the goal buffer"
(if (eq proof-goals-buffer buffer)
pos
(with-current-buffer proof-goals-buffer
diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el
index 7ceb0d66..98b51136 100644
--- a/generic/pg-pgip.el
+++ b/generic/pg-pgip.el
@@ -1,6 +1,6 @@
;; pg-pgip.el --- PGIP manipulation for Proof General
;;
-;; Copyright (C) 2000-2002, 2009 LFCS Edinburgh.
+;; Copyright (C) 2000-2002, 2010 LFCS Edinburgh.
;; Author: David Aspinall <David.Aspinall@ed.ac.uk>
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;
@@ -58,16 +58,16 @@ The list PGIPS may contain one or more PGIP packets, whose contents are processe
(defun pg-pgip-process-pgip (pgip)
"Process the commands in the PGIP XML-node PGIP."
- ;; FIXME: appearances of 'notreallyoptional below should be removed,
- ;; but they are needed for compatibility with Isabelle 2004 whose
- ;; PGIP messages are incomplete.
+ ;; NB: appearances of 'notreallyoptional below should be removed,
+ ;; but they are needed for compatibility with Isabelle at the moment,
+ ;; whose PGIP follows an older schema.
(let* ((name (xml-node-name pgip))
(tag (pg-xml-get-attr 'tag pgip 'optional))
(id (pg-xml-get-attr 'id pgip 'optional))
- (class (pg-xml-get-attr 'messageclass pgip 'notreallyoptional))
+ (class (pg-xml-get-attr 'messageclass pgip 'notreallyoptional))
(refseq (pg-xml-get-attr 'refseq pgip 'optional))
(refid (pg-xml-get-attr 'refid pgip 'optional))
- (seq (pg-xml-get-attr 'seq pgip 'notreallyoptional)))
+ (seq (pg-xml-get-attr 'seq pgip 'notreallyoptional)))
(setq pg-pgip-last-seen-id id)
(setq pg-pgip-last-seen-seq seq)
(if (eq name 'pgip)
@@ -91,7 +91,7 @@ Return a symbol representing the PGIP command processed, or nil."
(defvar pg-pgip-post-process-functions
'((hasprefs . proof-assistant-menu-update)
- (oldhaspref . proof-assistant-menu-update) ;; FIXME: for Isabelle2004 backward compat
+ (oldhaspref . proof-assistant-menu-update) ;; NB: Isabelle compatibility
(menuadd . proof-assistant-menu-update)
(menudel . proof-assistant-menu-update)
(idtable . pg-pgip-update-idtables) ;; TODO: not yet implemented
@@ -104,7 +104,8 @@ Return a symbol representing the PGIP command processed, or nil."
(let ((ppfn (cdr-safe (assoc cmdname pg-pgip-post-process-functions))))
(if (fboundp ppfn)
(progn
- (pg-pgip-debug "Post-processing for PGIP message type `%s' with function `%s'" cmdname ppfn)
+ (pg-pgip-debug
+ "Post-processing for PGIP message type `%s' with function `%s'" cmdname ppfn)
(funcall ppfn))
(pg-pgip-debug "[No post-processing defined for PGIP message type `%s']" cmdname))))
diff --git a/generic/pg-response.el b/generic/pg-response.el
index e8ed6512..ff5487bb 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -1,6 +1,6 @@
;; pg-response.el --- Proof General response buffer mode.
;;
-;; Copyright (C) 1994-2009 LFCS Edinburgh.
+;; Copyright (C) 1994-2010 LFCS Edinburgh.
;; Authors: David Aspinall, Healfdene Goguen,
;; Thomas Kleymann and Dilip Sequeira
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
@@ -10,7 +10,7 @@
;;; Commentary:
;;
;; This mode is used for the response buffer proper, and
-;; also the trace and theorems buffer. A sub-module of proof-shell.
+;; also the trace and theorems buffer. A sub-module of proof-shell.
;;
;;; Code:
@@ -94,7 +94,7 @@ Internal variable, setting this will have no effect!")
(unsplittable . t)
(menu-bar-lines . 0)
(tool-bar-lines . nil)
- (proofgeneral . t)) ;; indicates generated for/by PG FIXME!!
+ (proofgeneral . t)) ;; indicates generated for/by PG
"List of GNU Emacs frame parameters for secondary frames.")
(defun proof-multiple-frames-enable ()
@@ -221,12 +221,12 @@ For multiple frame mode, this function obeys the setting of
;;;###autoload
(defun pg-response-maybe-erase
(&optional erase-next-time clean-windows force)
- "Erase the response buffer according to pg-response-erase-flag.
+ "Erase the response buffer according to `pg-response-erase-flag'.
ERASE-NEXT-TIME is the new value for the flag.
-If CLEAN-WINDOWS is set, use proof-clean-buffer to do the erasing.
-If FORCE, override pg-response-erase-flag.
+If CLEAN-WINDOWS is set, use `proof-clean-buffer' to do the erasing.
+If FORCE, override `pg-response-erase-flag'.
-If the user option proof-tidy-response is nil, then
+If the user option `proof-tidy-response' is nil, then
the buffer is only cleared when FORCE is set.
No effect if there is no response buffer currently.
@@ -323,7 +323,7 @@ is set to nil, so responses are not cleared automatically."
;;;####autoload
(defun pg-response-warning (&rest args)
"Issue the warning ARGS in the response buffer and display it.
-The warning is coloured with proof-warning-face."
+The warning is coloured with `proof-warning-face'."
(pg-response-display-with-face (apply 'concat args) 'proof-warning-face)
(proof-display-and-keep-buffer proof-response-buffer))
@@ -345,9 +345,7 @@ negative means move back to previous error messages.
Optional argument ARGP means reparse the error message buffer
and start at the first error."
(interactive "P")
- (if (and ;; At least one setting must be configured
- pg-next-error-regexp
- ;; Response buffer must be live
+ (if (and pg-next-error-regexp
(or
(buffer-live-p proof-response-buffer)
(error "Next error: no response buffer to parse!")))
@@ -390,9 +388,7 @@ and start at the first error."
(if file
(find-file-noselect file)
(or proof-script-buffer
- ;; We could make more guesses here,
- ;; e.g. last script buffer active
- ;; (keep a record of it?)
+ ;; Could make guesses, e.g. last active script
(error
"Next error: can't guess file for error message"))))
(pop-up-windows t)
diff --git a/generic/pg-thymodes.el b/generic/pg-thymodes.el
deleted file mode 100644
index b019e6ef..00000000
--- a/generic/pg-thymodes.el
+++ /dev/null
@@ -1,97 +0,0 @@
-;; pg-thymodes.el --- Proof General "theory" modes.
-;;
-;; Copyright (C) 2002 LFCS Edinburgh.
-;; Author: David Aspinall
-;; License: GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
-;;
-;;; Commentary:
-;;
-;; Functions for defining "theory" modes, i.e. modes for
-;; non-interactive proof assistant files which do not contain proof
-;; scripts.
-;;
-;; STATUS: in progress, experimental; needs macro debugging.
-
-
-(require 'proof)
-
-
-;;;###autoload
-;;; Code:
-(defmacro pg-defthymode (sym name &rest body)
- "Define a Proof General mode for theory files.
-Mode name is SYM-mode, named NAMED. BODY is the body of a setq and
-can define a number of variables for the mode, viz:
-
- SYM-<font-lock-keywords> (value for font-lock-keywords)
- SYM-<syntax-table-entries> (list of pairs: used for modify-syntax-entry calls)
- SYM-<menu> (menu for the mode, arg of easy-menu-define)
- SYM-<parent-mode> (defaults to fundamental-mode)
- SYM-<filename-regexp> (regexp matching filenames for auto-mode-alist)
-
-All of these settings are optional."
- (progn
- (eval `(setq ,@body))
- (let*
- ;; See what was defined
- ((mode (intern (concat (symbol-name sym) "-mode")))
- (parentmode (pg-modesymval sym 'parent-mode 'fundamental-mode))
- (flks (pg-modesymval sym 'font-lock-keywords))
- (syntaxes (pg-modesymval sym 'syntax-table-entries))
- (menu (pg-modesymval sym 'menu))
- (menusym (pg-modesym sym 'menu))
- (keymap (pg-modesym mode 'map))
- (fileregexp (pg-modesymval sym 'filename-regexp)))
- ;; Set auto-mode-alist
- (if fileregexp
- (setq auto-mode-alist
- (cons (cons fileregexp mode) auto-mode-alist)))
- ;; `(quote (list ,mode ,parentmode ,flks ,fileregexp)))))
- ;; Define the mode (also makes keymap)
- (eval
- `(define-derived-mode ,mode ,parentmode ,name
- (interactive)
- (pg-do-unless-null ,flks (setq font-lock-defaults (',flks)))
- (pg-do-unless-null ,syntaxes (mapcar 'modify-syntax-entry ,syntaxes))))
- ;; Define the menu (final value of macro to be evaluated)
- `(pg-do-unless-null ,menu
- `(easy-menu-define
- ,menusym ,keymap
- ,(concat "Menu for "
- (symbol-name mode)
- " defined by `pg-defthymode'.")
- ,menu)))))
-
-
-
-;; Utilities
-
-(defmacro pg-do-unless-null (val &rest body)
- `(if ,val
- (progn ,@body)))
-
-
-(defun pg-symval (sym &optional other)
- "Return (symbol-value SYM) or nil/OTHER if SYM unbound."
- (if (boundp sym)
- (symbol-value sym)
- other))
-
-(defun pg-modesym (mode sym)
- "Return MODE-SYM."
- (intern (concat (symbol-name mode) "-" (symbol-name sym))))
-
-(defun pg-modesymval (mode sym &optional other)
- "Return value of symbol MODE-SYM or nil/OTHER if unbound."
- (let ((modesym (pg-modesym mode sym)))
- (if (boundp modesym)
- (symbol-value modesym)
- other)))
-
-
-
-
-(provide 'pg-thymodes)
-;;; pg-thymodes.el ends here
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 49c40675..fca238f8 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -966,6 +966,7 @@ The function `substitute-command-keys' is called on the argument."
(global-set-key [f5] 'pg-identifier-near-point-query)
(defun pg-identifier-under-mouse-query (event)
+ "Query the prover about the identifier near mouse click EVENT."
(interactive "e")
(if proof-query-identifier-command
(save-selected-window
@@ -975,6 +976,7 @@ The function `substitute-command-keys' is called on the argument."
(pg-identifier-near-point-query))))))
(defun pg-identifier-near-point-query ()
+ "Query the prover about the identifier near point."
(interactive)
(let* ((stend (if (region-active-p)
(cons (region-beginning) (region-end))
@@ -1005,6 +1007,7 @@ The function `substitute-command-keys' is called on the argument."
(defvar proof-query-identifier-history nil)
(defun proof-query-identifier (string)
+ "Query the prover about the identifier STRING."
(interactive
(list
(completing-read "Query identifier: "
@@ -1015,8 +1018,10 @@ The function `substitute-command-keys' is called on the argument."
(if string (pg-identifier-query string)))
(defun pg-identifier-query (identifier &optional ctxt callback)
- "Query the proof assisstant about the given identifier (or string).
+ "Query the proof assisstant about the given IDENTIFIER.
This uses `proof-query-identifier-command'.
+Parameter CTXT allows to give a context for the identifier (which
+allows for multiple name spaces).
If CALLBACK is set, we invoke that when the command completes."
(unless (or (null identifier)
(string-equal identifier "")) ;; or whitespace?
diff --git a/generic/pg-vars.el b/generic/pg-vars.el
index f30b0461..1f22c629 100644
--- a/generic/pg-vars.el
+++ b/generic/pg-vars.el
@@ -1,6 +1,6 @@
;;; pg-custom.el --- Proof General global variables
;;
-;; Copyright (C) 2008 LFCS Edinburgh.
+;; Copyright (C) 2008, 2010 LFCS Edinburgh.
;; Author: David Aspinall <David.Aspinall@ed.ac.uk> and others
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;
@@ -34,7 +34,7 @@ proof-assistant-table.")
(defvar proof-assistant ""
"Name of the proof assistant Proof General is using.
Do not change this variable! It is set automatically by the mode
-stub defined in proof-site, from names given in proof-assistant-table.")
+stub defined in proof-site, from names given in `proof-assistant-table'.")
(defvar proof-assistant-symbol nil
"Symbol for the proof assistant Proof General is using.
@@ -82,7 +82,7 @@ has been set.")
(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
+When this is non-nil, `proof-shell-ready-prover' will give
an error.")
(defvar proof-included-files-list nil
@@ -91,9 +91,9 @@ This list contains files in canonical truename format
\(see `file-truename').
Whenever a new file is being processed, it gets added to this list
-via the proof-shell-process-file configuration settings.
+via the `proof-shell-process-file' configuration settings.
When the prover retracts a file, this list is resynchronised via the
-proof-shell-retract-files-regexp and proof-shell-compute-new-files-list
+`proof-shell-retract-files-regexp' and `proof-shell-compute-new-files-list'
configuration settings.
Only files which have been *fully* processed should be included here.
@@ -111,7 +111,7 @@ read.")
"The currently active scripting buffer or nil if none.")
(defvar proof-previous-script-buffer nil
- "Previous value of proof-script-buffer, recorded when scripting turned off.
+ "Previous value of `proof-script-buffer', recorded when scripting turned off.
This can be used to help multiple file handling.")
(defvar proof-shell-buffer nil
@@ -265,4 +265,5 @@ where `k' is a key binding (vector) and `f' the designated function."
(provide 'pg-vars)
-;; pg-vars.el ends here
+
+;;; pg-vars.el ends here
diff --git a/generic/proof-config.el b/generic/proof-config.el
index c965e754..c6e073ea 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1,6 +1,6 @@
;;; proof-config.el --- Proof General configuration for proof assistant
;;
-;; Copyright (C) 1998-2009 LFCS Edinburgh.
+;; Copyright (C) 1998-2010 LFCS Edinburgh.
;; Author: David Aspinall <David.Aspinall@ed.ac.uk> and others
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;
@@ -350,7 +350,7 @@ You should set this variable for reliable working of Proof General."
(defcustom proof-script-comment-end-regexp nil
"Regexp which matches a comment end in the proof command language.
-The default value for this is set as (regexp-quote proof-script-comment-end)
+The default value for this is set as (regexp-quote `proof-script-comment-end')
but you can set this variable to something else more precise if necessary."
:type 'string
:group 'proof-script)
@@ -391,7 +391,7 @@ It's safe to leave this setting as nil."
:group 'proof-script)
(defcustom proof-save-with-hole-result 2
- "How to build theorem name after matching with `proof-save-with-hole-regexp'.
+ "How to get theorem name after `proof-save-with-hole-regexp' match.
String or Int.
If an int N use match-string to recover the value of the Nth parenthesis matched.
If it is a string use replace-match. In this case, `proof-save-with-hole-regexp'
@@ -421,7 +421,7 @@ It's safe to leave this setting as nil."
:group 'proof-script)
(defcustom proof-goal-with-hole-result 2
- "How to build theorem name after matching with `proof-goal-with-hole-regexp'.
+ "How to get theorem name after `proof-goal-with-hole-regexp' match.
String or Int.
If an int N use match-string to recover the value of the Nth parenthesis matched.
If it is a string use replace-match. In this case, proof-save-with-hole-regexp
@@ -612,7 +612,7 @@ steps within the outer proof."
"Non-nil if Proof General may undo to arbitrary positions.
The classic behaviour of Proof General is to undo completed
proofs in one step: this design arose because older provers
-discarded nested history once proofs were complete. The proof
+discarded nested history once proofs were complete. The proof
script engine amalgamates spans for a complete proof (into a
single 'goalsave) to give this effect.
@@ -1163,7 +1163,7 @@ and possibly analysed further for proof-by-pointing markup."
(defcustom proof-shell-end-goals-regexp nil
"Regexp matching the end of the proof state output, or nil.
This allows a shorter form of the proof state output to be displayed,
-in case several messages are combined in a command output.
+in case several messages are combined in a command output.
The portion treated as the goals output will be that between the
*end* of the match on `proof-shell-start-goals-regexp' and the
@@ -1247,8 +1247,8 @@ used to help parse the goals buffer to annotate it for proof by pointing."
"A pair (REGEXP . FUNCTION) to match a processed file name.
If REGEXP matches output, then the function FUNCTION is invoked.
-It must return the name of a script file (with complete path)
-that the system has successfully processed. In practice,
+It must return the name of a script file (with complete path)
+that the system has successfully processed. In practice,
FUNCTION is likely to inspect the match data. If it returns
the empty string, the file name of the scripting buffer is used
instead. If it returns nil, no action is taken.
@@ -1286,7 +1286,7 @@ date and needs to be updated with the help of the function
"Function to update `proof-included-files list'.
It needs to return an up-to-date list of all processed files. The
-result will be stored in `proof-included-files-list'.
+result will be stored in `proof-included-files-list'.
This function is called when `proof-shell-retract-files-regexp'
has been matched in the prover output.
@@ -1430,7 +1430,7 @@ response buffer.
This is intended for unusual debugging output from
the prover, rather than ordinary output from final proofs.
-This should match a string which is bounded by matches
+This should match a string which is bounded by matches
on `proof-shell-eager-annotation-start' and
`proof-shell-eager-annotation-end'.
@@ -1631,7 +1631,7 @@ before returning to the top level."
(defcustom proof-shell-handle-output-system-specific nil
"Set this variable to handle system specific output.
-Errors and interrupts are recognised in the function
+Errors and interrupts are recognised in the function
`proof-shell-handle-immediate-output'. Later output is
handled by `proof-shell-handle-delayed-output', which
displays messages to the user in *goals* and *response*
@@ -1643,7 +1643,7 @@ It should be a function which is passed (cmd string) as
arguments, where `cmd' is a string containing the currently
processed command and `string' is the response from the proof
system. If action is taken and goals/response display should
-be prevented, the function should update the variable
+be prevented, the function should update the variable
`proof-shell-last-output-kind' to some non-nil symbol.
The symbol will be compared against standard ones, see documentation
@@ -1798,7 +1798,7 @@ See also `proof-script-font-lock-keywords' and `proof-goals-font-lock-keywords'.
(defcustom proof-shell-font-lock-keywords nil
"Value of `font-lock-keywords' used to fontify the shell buiffer.
The shell mode should may this before calling `proof-response-config-done'.
-Note that by default, font lock is turned *off* in shell buffers to
+Note that by default, font lock is turned *off* in shell buffers to
improve performance. If you need to understand some output it may help
to turn it on temporarily.
See also `proof-script-font-lock-keywords', `proof-goals-font-lock-keywords'
diff --git a/generic/proof-depends.el b/generic/proof-depends.el
index aaa8f59d..535da59f 100644
--- a/generic/proof-depends.el
+++ b/generic/proof-depends.el
@@ -1,6 +1,6 @@
-;; proof-depends.el Theorem-theorem and theorem-definition dependencies.
+;;; proof-depends.el --- Theorem-theorem and theorem-definition dependencies
;;
-;; Copyright (C) 2000-2004 University of Edinburgh.
+;; Copyright (C) 2000-2004, 2010 University of Edinburgh.
;; Authors: David Aspinall <David.Aspinall@ed.ac.uk>
;; Earlier version by Fiona McNeil.
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
@@ -8,18 +8,20 @@
;;
;; $Id$
;;
+;;; Commentary:
+;;
;; Based on Fiona McNeill's MSc project on analysing dependencies
;; within proofs. Code rewritten by David Aspinall.
;;
+
+
(require 'cl)
(require 'span)
(require 'pg-vars)
(require 'proof-config)
(require 'proof-autoloads)
-;; Variables
-
(defvar proof-thm-names-of-files nil
"A list of file and theorems contained within.
A list of lists; the first element of each list is a file-name, the
@@ -33,6 +35,8 @@ second element a list of all the def names in that file.
i.e.: ((file-name-1 (def1 def2 def3)) (file-name-2 (def1 def2 def3)))")
+;;; Code:
+
;; Utility functions
(defun proof-depends-module-name-for-buffer ()
@@ -46,7 +50,7 @@ For other provers, this function may need modifying."
(file-name-sans-extension buffer-file-name)) ""))
(defun proof-depends-module-of (name)
- "Return a pair of a module name and base name for a given item name.
+ "Return a pair of a module name and base name for given item NAME.
Assumes module name is given by dotted prefix."
(let ((dot (string-match "\\." name)))
(if dot
@@ -126,7 +130,7 @@ Called from `proof-done-advancing' when a save is processed and
;;;###autoload
(defun proof-dependency-in-span-context-menu (span)
- "Make a portion of a context-sensitive menu showing proof dependencies."
+ "Make some menu entries showing proof dependencies of SPAN."
;; FIXME: might only activate this for dependency-relevant spans.
(list
"-------------"
@@ -192,8 +196,9 @@ Called from `proof-done-advancing' when a save is processed and
(cons nested toplevel)))
(defun proof-dep-make-submenu (name namefn appfn list)
- "Make menu items for a submenu NAME, using appfn applied to each elt in LIST.
-If LIST is empty, return a disabled menu item with NAME."
+ "Make menu items for a submenu NAME, using APPFN applied to each elt in LIST.
+If LIST is empty, return a disabled menu item with NAME.
+NAMEFN is applied to each element of LIST to make the names."
(if list
(cons name
(mapcar `(lambda (l)
@@ -204,7 +209,7 @@ If LIST is empty, return a disabled menu item with NAME."
(defun proof-make-highlight-depts-menu (name fn span prop)
"Return a menu item that for highlighting dependents/depencies of SPAN."
(let ((deps (span-property span prop)))
- (vector name `(,fn ,(span-property span 'name) (quote ,deps))
+ (vector name `(,fn ,(span-property span 'name) (quote ,deps))
(not (not deps)))))
@@ -213,6 +218,7 @@ If LIST is empty, return a disabled menu item with NAME."
;;
(defun proof-goto-dependency (name span)
+ "Go to the start of SPAN."
;; FIXME: check buffer is right one. Later we'll allow switching buffer
;; here and jumping to different files.
(goto-char (span-start span))
@@ -253,7 +259,7 @@ This is simply to display the dependency somehow."
(defun proof-depends-save-old-face (span)
(unless (span-property span 'depends-old-face)
- (span-set-property span 'depends-old-face
+ (span-set-property span 'depends-old-face
(span-property span 'face))))
(defun proof-depends-restore-old-face (span)
@@ -279,3 +285,7 @@ This is simply to display the dependency somehow."
(provide 'proof-depends)
;; proof-depends.el ends here
+
+(provide 'proof-depends)
+
+;;; proof-depends.el ends here
diff --git a/generic/proof-faces.el b/generic/proof-faces.el
index e689f051..7fe80ea7 100644
--- a/generic/proof-faces.el
+++ b/generic/proof-faces.el
@@ -17,7 +17,7 @@
;;
;; But it's difficult to keep track of all that!
;; Please report any bad/failing colour
-;; combinations (with suggested improvements) at
+;; combinations (with suggested improvements) at
;; http://proofgeneral.inf.ed.ac.uk/trac
;;
;; Some of these faces aren't used by default in Proof General,
@@ -108,7 +108,7 @@ Exactly what uses this face depends on the proof assistant."
(defface proof-error-face
(proof-face-specs
- (:background "rosybrown1") ; a drab version of misty rose
+ (:background "rosybrown1") ; a drab version of misty rose
(:background "brown")
(:bold t))
"*Face for error messages from proof assistant."
diff --git a/generic/proof-indent.el b/generic/proof-indent.el
index fc035aea..2ff6cf69 100644
--- a/generic/proof-indent.el
+++ b/generic/proof-indent.el
@@ -1,4 +1,4 @@
-;; proof-indent.el Generic Indentation for Proof Assistants
+;;; proof-indent.el --- Generic indentation for proof assistants
;;
;; Authors: Markus Wenzel, David Aspinall
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
@@ -6,11 +6,16 @@
;; $Id$
;;
+
+;;; Commentary:
+;;
+
(require 'proof-config) ; config variables
(require 'proof-utils) ; proof-ass
(require 'proof-syntax) ; p-looking-at-safe, p-re-search
(require 'proof-autoloads) ; p-locked-end
+;;; Code:
(defun proof-indent-indent ()
"Determine indentation caused by syntax element at current point."
(cond
@@ -21,7 +26,7 @@
(t 0)))
(defun proof-indent-offset ()
- "Determine offset of syntax element at current point"
+ "Determine offset of syntax element at current point."
(cond
((proof-looking-at-syntactic-context)
proof-indent)
@@ -54,7 +59,8 @@
(proof-indent-goto-prev))))
(defun proof-indent-calculate (indent inner) ; Note: may change point!
- "Calculate proper indentation level at current point"
+ "Calculate indentation level at point.
+INDENT is current indentation level, INNER a flag for inner indentation."
(let*
((current (point))
(found-prev (proof-indent-goto-prev)))
@@ -89,4 +95,7 @@
(if (< (current-column) (current-indentation))
(back-to-indentation)))))
+
(provide 'proof-indent)
+
+;;; proof-indent.el ends here
diff --git a/generic/proof-maths-menu.el b/generic/proof-maths-menu.el
index 4195a7dc..7d8db94d 100644
--- a/generic/proof-maths-menu.el
+++ b/generic/proof-maths-menu.el
@@ -1,4 +1,4 @@
-;; proof-maths-menu.el Support for maths menu mode package
+;;; proof-maths-menu.el --- Support for maths menu mode package
;;
;; Copyright (C) 2007, 2009 LFCS Edinburgh / David Aspinall
;; Author: David Aspinall <David.Aspinall@ed.ac.uk>
@@ -10,14 +10,16 @@
;;
;; $Id$
;;
-;; =================================================================
-;;
-;; NB: maths-menu is bundled with Proof General in lib/, and PG will select
+;;; Commentary:
+;;
+;; Note: maths menu is bundled with Proof General in lib/, and PG will select
;; it's own version before any other version on the Emacs load path.
;; If you want to override this, simply load your version before
;; starting Emacs, with (require 'maths-menu).
;;
+;;; Code:
+
(eval-when-compile
(require 'cl))
@@ -54,3 +56,7 @@ in future if we have just activated it for this buffer."
(provide 'proof-maths-menu)
;; End of proof-maths-menu.el
+
+(provide 'proof-maths-menu)
+
+;;; proof-maths-menu.el ends here
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index ee7189ea..7ab7a3ae 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -1,6 +1,6 @@
-;; proof-menu.el Menus, keymaps, and misc commands for Proof General
+;;; proof-menu.el --- Menus, keymaps, misc commands for Proof General
;;
-;; Copyright (C) 2000,2001,2009 LFCS Edinburgh.
+;; Copyright (C) 2000,2001,2009,2010 LFCS Edinburgh.
;; Authors: David Aspinall
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;
@@ -9,6 +9,7 @@
(require 'cl) ; mapcan
+;;; Code:
(eval-when (compile)
(defvar proof-assistant-menu nil) ; defined by macro in proof-menu-define-specific
(defvar proof-mode-map nil))
@@ -43,9 +44,9 @@ If in three window or multiple frame mode, display two buffers.
The idea of this function is to change the window->buffer mapping
without adjusting window layout."
(interactive)
- ;; Idea: a humane toggle, which allows habituation.
+ ;; Idea: a humane toggle, which allows habituation.
;; E.g. two taps of C-c C-l always shows the goals buffer, three the
- ;; trace buffer, etc. (Makes less sense from the menu, though,
+ ;; trace buffer, etc. (Makes less sense from the menu, though,
;; where it seems more natural just to rotate from last position)
(cond
((and (interactive-p)
@@ -290,6 +291,7 @@ without adjusting window layout."
(proof-deftoggle proof-sticky-errors)
(proof-deftoggle proof-shell-quiet-errors)
(proof-deftoggle proof-minibuffer-messages)
+(proof-deftoggle proof-autosend)
(proof-deftoggle-fn 'proof-imenu-enable 'proof-imenu-toggle)
(proof-deftoggle proof-keep-response-history)
@@ -359,7 +361,7 @@ without adjusting window layout."
["Auto Raise" proof-auto-raise-toggle
:style toggle
:selected proof-auto-raise-buffers
- :help "Automatically raise buffers when output arrives"]
+ :help "Automatically raise buffers when output arrives"]
["Use Three Panes" proof-three-window-toggle
:style toggle
:active (not proof-multiple-frames-enable)
@@ -392,12 +394,12 @@ without adjusting window layout."
:selected proof-sticky-errors
:help "Highlight commands that caused errors"])
("Read Only"
- ["Strict Read Only"
+ ["Strict Read Only"
(customize-set-variable 'proof-strict-read-only t)
:style radio
:selected (eq proof-strict-read-only t)
:help "Do not allow editing in processed region"]
- ["Undo On Edit"
+ ["Undo On Edit"
(customize-set-variable 'proof-strict-read-only 'retract)
:style radio
:selected (eq proof-strict-read-only 'retract)
@@ -571,9 +573,9 @@ without adjusting window layout."
(defconst proof-advanced-menu
(cons "Advanced"
(append
- '(["Complete Identifier" proof-script-complete
+ '(["Complete Identifier" proof-script-complete
:help "Complete the identifier at point"]
- ["Insert Last Output" pg-insert-last-output-as-comment
+ ["Insert Last Output" pg-insert-last-output-as-comment
:active proof-shell-last-output
:help "Insert the last output into the proof script as a comment"]
["Make Movie" pg-movie-export
@@ -664,6 +666,10 @@ suitable for adding to the proof assistant menu."
(vector menuname menu-fn t)))
+
+;;; Commentary:
+;;
+
;;; Code for adding "favourites" to the proof-assistant specific menu
(defvar proof-make-favourite-cmd-history nil
@@ -708,7 +714,7 @@ suitable for adding to the proof assistant menu."
"Name of command on menu: "
cmd
proof-make-favourite-menu-history))
- (key (if (y-or-n-p "Set a keybinding for this command? : ")
+ (key (if (y-or-n-p "Set a keybinding for this command? ")
;; FIXME: better validation here would be to check
;; this is a new binding, or remove old binding below.
(read-key-sequence
@@ -853,7 +859,7 @@ KEY is the optional key binding."
)))
(defun proof-maybe-askprefs ()
- "If `proof-use-pgip-askprefs' is non-nil, try to issue <askprefs>"
+ "If `proof-use-pgip-askprefs' is non-nil, try to issue <askprefs>."
(if (and proof-use-pgip-askprefs proof-shell-issue-pgip-cmd)
(pg-pgip-askprefs)))
@@ -881,7 +887,7 @@ NB: if no settings are configured, this has no effect."
(cons "%i" '(proof-assistant-format-int curvalue))
(cons "%s" '(proof-assistant-format-string curvalue)))
"Table to use with `proof-format' for formatting CURVALUE for assistant.
-NB: variable curvalue is dynamically scoped (used in proof-assistant-format).")
+NB: variable curvalue is dynamically scoped (used in `proof-assistant-format').")
(defun proof-assistant-format-bool (value)
(if value proof-assistant-true-value proof-assistant-false-value))
@@ -921,4 +927,5 @@ value) and the second for false."
(provide 'proof-menu)
-;; proof-menu.el ends here.
+
+;;; proof-menu.el ends here
diff --git a/generic/proof-mmm.el b/generic/proof-mmm.el
index ce0dd1ef..b450f20c 100644
--- a/generic/proof-mmm.el
+++ b/generic/proof-mmm.el
@@ -1,26 +1,30 @@
;; proof-mmm.el --- Support for MMM mode package
;;
-;; Copyright (C) 2003 LFCS Edinburgh / David Aspinall
+;; Copyright (C) 2003, 2010 LFCS Edinburgh / David Aspinall
;; Author: David Aspinall <David.Aspinall@ed.ac.uk>
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;
;; The MMM package is at http://mmm-mode.sourceforge.net/
;;
-;; With thanks to Stefan Monnier for pointing me to this package,
-;; and Michael Abraham Shulman for providing it.
-;;
;; $Id$
;;
-;; =================================================================
+;;; Commentary:
+;;
+;; Configuration for the prover is expected to reside in <foo>-mmm.el
+;; It should define an MMM submode class called <foo>.
;;
;; NB: mmm-mode is bundled with Proof General, and PG will select
;; it's own version before any other version on the Emacs load path.
;; If you want to override this, simply load your version before
;; starting Emacs, with (require 'mmm-auto).
;;
-;; Configuration for the prover is expected to reside in <foo>-mmm.el
-;; It should define an MMM submode class called <foo>.
+;; Credits: thanks to Stefan Monnier for pointing me to this package,
+;; and Michael Abraham Shulman for providing it.
+;;
+
+
+;;; Code:
(eval-when-compile
(require 'cl))
@@ -61,7 +65,7 @@ in future if we have just activated it for this buffer."
(when (proof-mmm-support-available)
;; Make sure auto mode follows PG's global setting. (NB: might do
;; only if global state changes, but by now (proof-ass mmm-mode) set).
- (with-no-warnings ; bytecomp gives spurious error
+ (with-no-warnings ; bytecomp gives spurious error
; "proof-mmm-set-global might not be defined"
; because the autoload overrides the definition above(!)
(proof-mmm-set-global (not mmm-mode)))
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 3db7bfde..d8807940 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1,6 +1,6 @@
;;; proof-script.el --- Major mode for proof assistant script files.
;;
-;; Copyright (C) 1994-2009 LFCS Edinburgh.
+;; Copyright (C) 1994-2010 LFCS Edinburgh.
;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen,
;; Thomas Kleymann and Dilip Sequeira
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
@@ -309,7 +309,7 @@ value of proof-locked span."
(defun proof-script-clear-queue-spans-on-error (badspan)
"Remove the queue span from buffer, cleaning spans no longer queued.
-If BADSPAN is non-nil, assume that this was the span whose command
+If BADSPAN is non-nil, assume that this was the span whose command
caused the error. Go to the start of it if `proof-follow-mode' is
'locked.
@@ -324,7 +324,7 @@ This is a subroutine used in proof-shell-handle-{error,interrupt}."
(goto-char (span-start badspan))
(skip-chars-forward " \t\n"))
(when proof-sticky-errors
- (pg-set-span-helphighlights badspan
+ (pg-set-span-helphighlights badspan
'proof-script-highlight-error-face
'proof-script-sticky-error-face)))
(proof-script-delete-spans start end)))
@@ -496,7 +496,7 @@ Intended as a hook function for `proof-shell-handle-error-or-interrupt-hook'."
(span-detach span) ;; delete overlay, without pre-del fn
(remhash id elts))))
-(defun pg-get-element (idiomsym id)
+(defun pg-get-element (idiomsym id)
"Return proof script element of type IDIOM identifier ID.
IDIOM is a symbol, ID is a string."
(assert (symbolp idiomsym))
@@ -525,15 +525,15 @@ It is recorded in the span with the 'rawname property."
(rawname name)
(name (or name id))
(idiom (symbol-name idiomsym))
- (delfn `(lambda () (pg-remove-element
+ (delfn `(lambda () (pg-remove-element
(quote ,idiomsym) (quote ,idsym))))
(elts (cdr-safe (assq idiomsym pg-script-portions))))
(unless elts
- (setq pg-script-portions
+ (setq pg-script-portions
(cons (cons idiomsym (setq elts (make-hash-table)))
pg-script-portions)))
(if (gethash idsym elts)
- (proof-debug "Element named " name
+ (proof-debug "Element named " name
" (type " idiom ") was already in buffer."))
(puthash idsym span elts)
;; Idiom and ID are stored in the span as symbols; name as a string.
@@ -575,7 +575,7 @@ It is recorded in the span with the 'rawname property."
(defun pg-toggle-element-span-visibility (span)
"Toggle visibility of SPAN."
- (span-set-property
+ (span-set-property
span 'invisible
(not (span-property span 'invisible))))
@@ -670,10 +670,10 @@ This is used to annotate the buffer with the result of proof steps."
proof-shell-last-output))))
;; HACK: for Isabelle which puts ugly leading \n's around proofstate.
- (if (and (> (length text) 0)
+ (if (and (> (length text) 0)
(string= (substring text 0 1) "\n"))
(setq text (substring text 1)))
- (if (and (> (length text) 0)
+ (if (and (> (length text) 0)
(string= (substring text -1) "\n"))
(setq text (substring text 0 -1)))
@@ -703,12 +703,12 @@ Argument FACE means add regular face property FACE to the span."
(span-set-property newspan 'pghelp t)
(span-set-property newspan 'response output)
- (span-set-property newspan 'help-echo
+ (span-set-property newspan 'help-echo
(if (<= (length output) 2)
(pg-span-name span)
- output))
+ output))
- ;; Here's the message we used to show in minibuffer
+ ;; Here's the message we used to show in minibuffer
;; when pg-show-hints was on:
;;
;; " ("
@@ -722,7 +722,7 @@ Argument FACE means add regular face property FACE to the span."
(span-set-property newspan 'modification-hooks
(list 'pg-delete-self-modification-hook))
(if (or (facep mouseface)
- (setq mouseface
+ (setq mouseface
(unless mouseface 'proof-mouse-highlight-face)))
(span-set-property newspan 'mouse-face mouseface))
(if face
@@ -828,7 +828,7 @@ proof assistant and Emacs has a modified buffer visiting the file."
'wait))))))
(defun proof-query-save-this-buffer-p ()
- "Predicate testing whether save-some-buffers during scripting should query."
+ "Predicate testing whether `save-some-buffers' during scripting should query."
(and (eq major-mode proof-mode-for-script)
(not (eq (current-buffer) proof-script-buffer))))
@@ -1404,7 +1404,7 @@ Argument SPAN has just been processed."
(and proof-save-with-hole-regexp
(proof-string-match proof-save-with-hole-regexp cmd)
;; Give a message of a name if one can be determined
- (proof-minibuffer-message
+ (proof-minibuffer-message
(format "proved %s"
(setq nam
(if (stringp proof-save-with-hole-result)
@@ -1469,7 +1469,7 @@ Argument SPAN has just been processed."
(if proof-last-theorem-dependencies
(proof-depends-process-dependencies nam gspan)))))
-(defun proof-make-goalsave
+(defun proof-make-goalsave
(gspan goalend savestart saveend nam &optional nestedundos)
"Make new goal-save span, using GSPAN. Subroutine of `proof-done-advancing-save'.
Argument GOALEND is the end of the goal;."
@@ -1578,7 +1578,7 @@ Subroutine of `proof-done-advancing-save'."
;; Hidable regions for commands: the problem is that they have no
;; natural surrounding region, so makes it difficult to define a
;; region for revealing again.
- (cond
+ (cond
((funcall proof-goal-command-p span)
(pg-add-element 'statement id bodyspan)
(incf proof-nesting-depth))
@@ -1604,7 +1604,7 @@ Subroutine of `proof-done-advancing-save'."
(defun proof-segment-up-to-parser (pos &optional next-command-end)
"Parse the script buffer from end of queue/locked region to POS.
This partitions the script buffer into contiguous regions, classifying
-them by type. We Return a list of lists of the form
+them by type. Return a list of lists of the form
(TYPE TEXT ENDPOS)
@@ -1650,7 +1650,7 @@ to the function which parses the script segment by segment."
((null type)) ; nothing left in buffer
(t
(error
- "Proof-segment-up-to-parser: bad TYPE value from proof-script-parse-function.")))
+ "Proof-segment-up-to-parser: bad TYPE value from proof-script-parse-function")))
;;
(if seg
(progn
@@ -1781,7 +1781,7 @@ to the function which parses the script segment by segment."
(progn (goto-char end) 'cmd)))))
-(defun proof-semis-to-vanillas (semis)
+(defun proof-semis-to-vanillas (semis &optional queueflags)
"Create vanilla spans for SEMIS and a list for the queue.
Proof terminator positions SEMIS has the form returned by
the function `proof-segment-up-to'. The argument list is destroyed.
@@ -1789,7 +1789,9 @@ The callback in each queue element is `proof-done-advancing'.
If the variable `proof-script-preprocess' is set (to the name of
a function, call that function to construct the first element of
-each queue item."
+each queue item.
+
+The optional QUEUEFLAGS are added to each queue item."
(let ((start (proof-queue-or-locked-end))
(file (or (buffer-file-name) (buffer-name)))
(cb 'proof-done-advancing)
@@ -1804,7 +1806,7 @@ each queue item."
(let* ((cmd (nth 1 semi))
(qcmd (if proof-script-preprocess
(funcall proof-script-preprocess
- file
+ file
;; ignore spaces at start of command
(+ start (save-excursion
(goto-char start)
@@ -1818,7 +1820,8 @@ each queue item."
;; ignored text
(span-set-property span 'type 'comment)
(setq alist
- (cons (list span nil cb) alist))) ; nil was `proof-no-command'
+ (cons (list span nil cb queueflags) ; nil was `proof-no-command'
+ alist)))
(setq start end)))
(nreverse alist)))
@@ -1849,20 +1852,20 @@ Assumes that point is at the end of a command."
;; commands, and the adds the commands into the queue.
;;
-(defun proof-assert-until-point ()
+(defun proof-assert-until-point (&optional displayflags)
"Process the region from the end of the locked-region until point."
(if (proof-only-whitespace-to-locked-region-p)
(error
"At end of the locked region, nothing to do to!"))
(let ((semis (save-excursion
- (skip-chars-backward " \t\n"
+ (skip-chars-backward " \t\n"
(proof-queue-or-locked-end))
(proof-segment-up-to-using-cache (point)))))
(if (eq 'unclosed-comment (car semis))
(setq semis (cdr semis)))
(if (null semis) ; maybe inside a string or something.
(error "I can't find any complete commands to process!"))
- (proof-assert-semis semis)))
+ (proof-assert-semis semis displayflags)))
(defun proof-assert-electric-terminator ()
"Insert the proof command terminator, and assert up to it.
@@ -1882,7 +1885,7 @@ comment, and insert or skip to the next semi)."
(= (char-after (point)) proof-terminal-char)))
(insert proof-terminal-string)
(setq ins t))
- (let* ((pos
+ (let* ((pos
(if proof-electric-terminator-noterminator (1- (point)) (point)))
(semis
(save-excursion
@@ -1899,7 +1902,7 @@ comment, and insert or skip to the next semi)."
(proof-assert-semis semis)
(proof-script-next-command-advance))))))
-(defun proof-assert-semis (semis)
+(defun proof-assert-semis (semis &optional displayflags)
"Add to the command queue the list SEMIS of command positions.
SEMIS must be a non-empty list, in reverse order (last position first).
We assume that the list is contiguous and begins at (proof-queue-or-locked-end).
@@ -1909,7 +1912,7 @@ that these may be overwritten)."
(proof-activate-scripting nil 'advancing)
(let ((startpos (proof-queue-or-locked-end))
(lastpos (nth 2 (car semis)))
- (vanillas (proof-semis-to-vanillas semis)))
+ (vanillas (proof-semis-to-vanillas semis displayflags)))
(proof-script-delete-secondary-spans startpos lastpos)
(proof-extend-queue lastpos vanillas)))
@@ -1957,7 +1960,7 @@ No effect if prover is busy."
(span-set-property span 'type 'pbp)
(span-set-property span 'cmd cmd)
(proof-start-queue (proof-unprocessed-begin) (point)
- (list (list span (list cmd)
+ (list (list span (list cmd)
'proof-done-advancing)))))
;;;###autoload
@@ -2174,10 +2177,10 @@ command."
(proof-goto-end-of-locked)
(backward-char)
(setq span (span-at (point) 'type)))
- (if span
+ (if span
(proof-retract-target span delete-region)
;; something wrong
- (proof-debug
+ (proof-debug
"proof-retract-until-point: couldn't find a span!"))))))
@@ -2224,7 +2227,7 @@ command."
(add-hook 'proof-activate-scripting-hook 'proof-cd-sync nil t))
;; NB: proof-mode-map declared above
-(proof-menu-define-keys proof-mode-map)
+(proof-menu-define-keys proof-mode-map)
(proof-eval-when-ready-for-assistant
(define-key proof-mode-map [(control c) (control a)] (proof-ass keymap)))
@@ -2644,6 +2647,8 @@ Choice of function depends on configuration setting."
'proof-script-after-change-function nil t))
+
+
(provide 'proof-script)
;;; proof-script.el ends here
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 4749a55b..788d32da 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1,6 +1,6 @@
;;; proof-shell.el --- Proof General shell mode.
;;
-;; Copyright (C) 1994-2009 LFCS Edinburgh.
+;; Copyright (C) 1994-2010 LFCS Edinburgh.
;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen,
;; Thomas Kleymann and Dilip Sequeira
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
@@ -41,15 +41,16 @@ The value is a list of lists of the form
(SPAN COMMANDS ACTION [FLAGS])
-which is the queue of things to do. Flags are set for non-standard
-commands (out of script). They may include
+which is the queue of things to do. Flags are set for non-scripting
+commands or for when scripting should not bother the user.
+They may include
'no-response-display do not display messages in *response* buffer
'no-error-display do not display errors/take error action
'no-goals-display do not goals in *goals* buffer
If flags are non-empty, other interactive cues will be surpressed.
-\(E.g., printing help messages).
+\(E.g., printing hints).
See the functions `proof-start-queue' and `proof-shell-exec-loop'.")
@@ -396,7 +397,7 @@ shell buffer, alled by `proof-shell-bail-out' if process exits."
(bufname (buffer-name)))
(message "%s, cleaning up and exiting..." bufname)
- (let (timeout-id)
+ (let (timeout-id)
(redisplay t) ; redisplay
(if alive ; process still there
(progn
@@ -503,10 +504,11 @@ This simply kills the `proof-shell-buffer' relying on the hook function
(error "No proof shell buffer to kill!")))
(defun proof-shell-bail-out (process event)
- "Value for the process sentinel for the proof assistant process.
-If the proof assistant dies, run proof-shell-kill-function to
+ "Value for the process sentinel for the proof assistant PROCESS.
+If the proof assistant dies, run `proof-shell-kill-function' to
cleanup and remove the associated buffers. The shell buffer is
-left around so the user may discover what killed the process."
+left around so the user may discover what killed the process.
+EVENT is the string describing the change."
(message "Process %s %s, shutting down scripting..." process event)
(proof-shell-kill-function)
(message "Process %s %s, shutting down scripting...done." process event))
@@ -605,7 +607,7 @@ non-empty flags) will not invoke any of this action." ; PG4.0 change
(unless (memq 'no-error-display flags)
(cond
((eq err-or-int 'interrupt)
- (pg-response-maybe-erase t t t) ; force cleaned now & next
+ (pg-response-maybe-erase t t t) ; force cleaned now & next
(proof-shell-handle-error-output
(if proof-shell-truncate-before-error proof-shell-interrupt-regexp)
'proof-error-face)
@@ -626,7 +628,7 @@ non-empty flags) will not invoke any of this action." ; PG4.0 change
(unless proof-shell-quiet-errors
(beep))
(proof-with-current-buffer-if-exists proof-script-buffer
- (proof-script-clear-queue-spans-on-error
+ (proof-script-clear-queue-spans-on-error
(car-safe (car-safe proof-action-list))))
(setq proof-action-list nil)
(proof-release-lock)
@@ -660,7 +662,7 @@ This is a hook function for proof-shell-handle-delayed-output-hook."
"See if the output between START and END must be dealt with immediately.
To speed up processing, PG tries to avoid displaying output that
the user will not have a chance to see. Some output must be
-handled immediately, however: these are errors, interrupts,
+handled immediately, however: these are errors, interrupts,
goals and loopbacks (proof step hints/proof by pointing results).
In this function we check, in turn:
@@ -797,7 +799,7 @@ used in `proof-add-to-queue' when we start processing a queue, and in
(goto-char (point-max))
;; TEMP: next step: preprocess list of strings directly
- (let ((string (apply 'concat strings)))
+ (let ((string (apply 'concat strings)))
;; Hook for munging `string' and other dirty hacks.
(run-hooks 'proof-shell-insert-hook)
@@ -878,7 +880,7 @@ track what happens in the proof queue."
Comments are not sent to the prover."
(let (cbitems nextitem)
(while (and proof-action-list
- (not (nth 1 (setq nextitem
+ (not (nth 1 (setq nextitem
(car proof-action-list)))))
(setq cbitems (cons nextitem cbitems))
(setq proof-action-list (cdr proof-action-list)))
@@ -911,7 +913,7 @@ being processed."
;; (should have proof-action-list<>nil -> busy)
(and proof-shell-busy queuemode
(unless (eq proof-shell-busy queuemode)
- (proof-debug
+ (proof-debug
"proof-append-alist: wrong queuemode detected for busy shell")
(assert (eq proof-shell-busy queuemode)))))
@@ -1030,9 +1032,9 @@ The return value is non-nil if the action list is now empty."
(defun proof-shell-insert-loopback-cmd (cmd)
- "Insert command sequence sent from prover into script buffer.
+ "Insert command string CMD sent from prover into script buffer.
String is inserted at the end of locked region, after a newline
-and indentation. Assumes proof-script-buffer is active."
+and indentation. Assumes `proof-script-buffer' is active."
(unless (string-match "^\\s-*$" cmd) ; FIXME: assumes cmd is single line
(with-current-buffer proof-script-buffer
(let (span)
@@ -1088,7 +1090,7 @@ ends with text matching `proof-shell-eager-annotation-end'."
(proof-shell-process-urgent-message-elisp))
((proof-looking-at-safe proof-shell-match-pgip-cmd)
- (pg-pgip-process-packet
+ (pg-pgip-process-packet
;; NB: xml-parse-region ignores junk before XML
(xml-parse-region start end)))
@@ -1108,11 +1110,11 @@ ends with text matching `proof-shell-eager-annotation-end'."
;; Clear the response buffer this time, but not next, leave window.
(pg-response-maybe-erase nil nil)
(proof-minibuffer-message
- (buffer-substring-no-properties
- (save-excursion
+ (buffer-substring-no-properties
+ (save-excursion
(re-search-forward proof-shell-eager-annotation-start end nil)
(point))
- (min end
+ (min end
(save-excursion (end-of-line) (point))
(+ start 75))))
(pg-response-display-with-face
@@ -1122,7 +1124,7 @@ ends with text matching `proof-shell-eager-annotation-end'."
(defun proof-shell-process-urgent-message-trace (start end)
"Display a message in the tracing buffer.
A subroutine of `proof-shell-process-urgent-message'."
- (proof-trace-buffer-display
+ (proof-trace-buffer-display
(buffer-substring-no-properties start end))
(unless (and proof-trace-output-slow-catchup
(pg-tracing-tight-loop))
@@ -1173,7 +1175,7 @@ A subroutine of `proof-shell-process-urgent-message'."
(let ((names (match-string 1))
(deps (match-string 2))
(sep proof-shell-theorem-dependency-list-split))
- (setq
+ (setq
proof-last-theorem-dependencies
(cons (split-string names sep)
(split-string deps sep)))))
@@ -1219,7 +1221,7 @@ A subroutine of `proof-shell-process-urgent-message'."
"Filter for the proof assistant shell-process.
A function for `scomint-output-filter-functions'.
-Deal with output and issue new input from the queue. This is
+Deal with output STR and issue new input from the queue. This is
an important internal function.
Handle urgent messages first. As many as possible are processed,
@@ -1242,9 +1244,9 @@ example, in this case:
`proof-marker' points after INPUT.
`proof-shell-urgent-message-marker' points after URGENT-MESSAGE-2,
-after both urgent messages have been processed by
-`proof-shell-process-urgent-messages'. Urgent messages always
-processed; they are intended to correspond to informational
+after both urgent messages have been processed by
+`proof-shell-process-urgent-messages'. Urgent messages always
+processed; they are intended to correspond to informational
notes that the prover makes to inform the user or interface on
progress.
@@ -1302,7 +1304,7 @@ is only changed when input is sent in `proof-shell-insert'."
(progn
(setq endpos (match-beginning 0))
(setq proof-shell-last-prompt
- (buffer-substring-no-properties
+ (buffer-substring-no-properties
endpos (match-end 0)))
(goto-char (point-max))
(setq proof-shell-expecting-output nil)
@@ -1335,13 +1337,13 @@ messages."
"Scan the shell buffer for urgent messages.
Scanning starts from `proof-shell-urgent-message-scanner' or
`scomint-last-input-end', which ever is later. We deal with strings
-between regexps `proof-shell-eager-annotation-start' and
-`proof-shell-eager-annotation-end'.
+between regexps `proof-shell-eager-annotation-start' and
+`proof-shell-eager-annotation-end'.
We update `proof-shell-urgent-message-marker' to point to last message found.
This is a subroutine of `proof-shell-filter'."
- (let ((pt (point)) (end t)
+ (let ((pt (point)) (end t)
lastend laststart
(initstart (max (marker-position proof-shell-urgent-message-scanner)
(marker-position scomint-last-input-end))))
@@ -1357,11 +1359,11 @@ This is a subroutine of `proof-shell-filter'."
;; Process the region including the annotations
(proof-shell-process-urgent-message laststart lastend))))
- (set-marker
+ (set-marker
proof-shell-urgent-message-scanner
(if end ;; couldn't find message start; move forward to avoid rescanning
(max initstart
- (- (point)
+ (- (point)
(1+ proof-shell-eager-annotation-start-length)))
;; incomplete message; leave marker at start of message
laststart))
@@ -1398,7 +1400,7 @@ by the filter is to send the next command from the queue."
;; Keep a copy of the last message from the prover
;; PG 4.0: this is kept verbatim, never modified.
- (setq proof-shell-last-output
+ (setq proof-shell-last-output
(buffer-substring-no-properties start end))
;; sets proof-shell-last-output-kind
@@ -1429,7 +1431,7 @@ are not dealt with eagerly during script processing, namely
This is useful even with empty delayed output as it can
clear the buffers.
-The delayed output is in the region
+The delayed output is in the region
\[proof-shell-last-output-start,proof-shell-last-output-end].
If goals output is found, the last matching instance, possibly
@@ -1446,7 +1448,7 @@ if OUTPUT has this form:
then GOALS-2 will be displayed in the goals buffer, and MESSAGE-2
in the response buffer. Notice that the above alternation can
-only be distinguished if both `proof-shell-start-goals-regexp'
+only be distinguished if both `proof-shell-start-goals-regexp'
and `proof-shell-end-goals-regexp' are set. With just the
former, MESSAGE-1 GOALS-1 MESSAGE-2 would all appear in
the response buffer.
@@ -1471,22 +1473,22 @@ i.e., 'goals or 'response."
(goto-char gstart)
(while (re-search-forward proof-shell-start-goals-regexp end t)
(setq gstart (match-beginning 0))
- (setq gend
+ (setq gend
(if proof-shell-end-goals-regexp
(progn
(re-search-forward proof-shell-end-goals-regexp end t)
(match-beginning 0)
(setq rstart (match-end 0)))
end)))
- (setq proof-shell-last-goals-output
+ (setq proof-shell-last-goals-output
(buffer-substring-no-properties gstart gend))
(unless (memq 'no-goals-display flags)
(pg-goals-display proof-shell-last-goals-output))
;; also allow (for Coq) any preceding output as a response
;; FIXME heuristic: 4 allows for annotation in end-goals-regexp
(when (> (- gstart rstart) 4)
- (proof-shell-display-output-as-response
- flags
+ (proof-shell-display-output-as-response
+ flags
(buffer-substring-no-properties rstart gstart)))
;; primary output kind is goals
'goals))
@@ -1587,15 +1589,17 @@ Only works when system timer has microsecond count available."
;;
;;;###autoload
-(defun proof-shell-wait ()
+(defun proof-shell-wait (&optional interrupt-on-input)
"Busy wait for `proof-shell-busy' to become nil.
Needed between sequences of commands to maintain synchronization,
because Proof General does not allow for the action list to be extended
in some cases. May be called by `proof-shell-invisible-command'."
(let ((proverproc (get-buffer-process proof-shell-buffer)))
(when proverproc
- (while (and proof-shell-busy (not quit-flag))
- (accept-process-output proverproc 1)
+ (while (and proof-shell-busy (not quit-flag)
+ (or (not interrupt-on-input) (input-pending-p)))
+ (accept-process-output proverproc 0.2) ;; NB: FIXME likely GE 23-ism
+ ;; assume filters ran, redisplay
(redisplay t))
(if quit-flag
(error "Proof General: Quit in proof-shell-wait")))))
@@ -1612,7 +1616,7 @@ Calls proof-state-change-hook."
The CMD is `invisible' in the sense that it is not recorded in buffer.
CMD may be a string or a string-yielding expression.
-Automatically add proof-terminal-char if necessary, examining
+Automatically add `proof-terminal-char' if necessary, examining
`proof-shell-no-auto-terminate-commands'.
By default, let the command be processed asynchronously.
@@ -1625,7 +1629,7 @@ INVISIBLECALLBACK will be invoked after the command has finished,
if it is set. It should probably run the hook variables
`proof-state-change-hook'.
-If NOERROR is set, surpress usual error action."
+FLAGS are put onto the If NOERROR is set, surpress usual error action."
(unless (stringp cmd)
(setq cmd (eval cmd)))
(if cmd
@@ -1715,16 +1719,16 @@ Error messages are displayed as usual."
;; scomint customisation.
- (setq scomint-output-filter-functions
+ (setq scomint-output-filter-functions
(append
(if proof-shell-strip-crs-from-output 'scomint-strip-ctrl-m)
(list 'proof-shell-filter)))
(setq proof-marker ; follows prompt
- (make-marker)
- proof-shell-urgent-message-marker
+ (make-marker)
+ proof-shell-urgent-message-marker
(make-marker) ; follows urgent messages
- proof-shell-urgent-message-scanner
+ proof-shell-urgent-message-scanner
(make-marker)) ; last scan point
(set-marker proof-shell-urgent-message-scanner (point-min))
diff --git a/generic/proof-site.el b/generic/proof-site.el
index 81ef2325..7af1f7a0 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -1,5 +1,4 @@
;; proof-site.el -- Loading stubs for Proof General.
-;; Configuration for site and choice of provers.
;;
;; Copyright (C) 1998-2003 LFCS Edinburgh.
;; Author: David Aspinall <David.Aspinall@ed.ac.uk>
@@ -7,6 +6,10 @@
;;
;; $Id$
;;
+;;; Commentary:
+;;
+;; Loading stubs and configuration for site and choice of provers.
+;;
;; NB: Normally users do not need to edit this file. Developers/installers
;; may want to adjust proof-assistant-table-default below.
;;
@@ -19,6 +22,7 @@
;; Master table of supported proof assistants.
;;
+;;; Code:
(defconst proof-assistant-table-default
'((isar "Isabelle" "\\.thy$")
(coq "Coq" "\\.v$\\|\\.v8$\\|\\.v7$")
@@ -63,7 +67,7 @@
(string-match "Version \\([^ ]+\\)\\." proof-general-version)
(match-string 1 proof-general-version))))
-(defconst proof-general-version-year "2009")
+(defconst proof-general-version-year "2010")
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
@@ -89,7 +93,7 @@
;;
(defun proof-home-directory-fn ()
- "Used to set proof-home-directory."
+ "Used to set `proof-home-directory'."
(let ((s (getenv "PROOFGENERAL_HOME")))
(if s
(if (string-match "/$" s) s (concat s "/"))
@@ -125,6 +129,8 @@ You can use customize to set this variable."
(add-to-list 'load-path (concat proof-home-directory "lib/"))
;; Declare some global variables and autoloads
+
+
(require 'pg-vars)
(require 'proof-autoloads)
@@ -319,3 +325,7 @@ If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'."
(provide 'proof-site)
;; proof-site.el ends here
+
+(provide 'proof-site)
+
+;;; proof-site.el ends here
diff --git a/generic/proof-splash.el b/generic/proof-splash.el
index f8f88f3e..91ee4660 100644
--- a/generic/proof-splash.el
+++ b/generic/proof-splash.el
@@ -1,12 +1,18 @@
;; proof-splash.el -- Splash welcome screen for Proof General
;;
-;; Copyright (C) 1998-2005, 2009 LFCS Edinburgh.
+;; Copyright (C) 1998-2005, 2009, 2010 LFCS Edinburgh.
;; Author: David Aspinall
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;
;; $Id$
;;
;;
+;;; Commentary:
+;;
+;; Provide splash screen for Proof General.
+;;
+
+;;; Code:
(require 'proof-site)
@@ -256,5 +262,7 @@ If TIMEOUT is non-nil, arrange for a time-out to occur outside this function."
(setq frame-title-format proof-splash-old-frame-title-format)
(setq proof-splash-old-frame-title-format nil)))
+
(provide 'proof-splash)
-;; End of proof-splash.
+
+;;; proof-splash.el ends here
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index 1c86e6f5..4ca8b9fe 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -1,4 +1,4 @@
-;; proof-syntax.el Functions for dealing with syntax
+;; proof-syntax.el --- Functions for dealing with syntax
;;
;; Copyright (C) 1997-2001 LFCS Edinburgh.
;; Authors: David Aspinall, Healfdene Goguen,
@@ -17,8 +17,8 @@
(defsubst proof-ids-to-regexp (l)
"Maps a non-empty list of tokens `l' to a regexp matching any element.
Uses a regexp of the form \\_<...\\_>."
- (concat "\\_<\\(?:"
- (regexp-opt l) ; was: (mapconcat 'identity l "\\|")
+ (concat "\\_<\\(?:"
+ (regexp-opt l) ; was: (mapconcat 'identity l "\\|")
"\\)\\_>"))
(defsubst proof-anchor-regexp (e)
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index fc23aabd..a50905b0 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -31,14 +31,18 @@
;;
(defun proof-toolbar-function (token)
+ "Construct name of toolbar function for TOKEN."
(intern (concat "proof-toolbar-" (symbol-name token))))
(defun proof-toolbar-icon (token)
+ "Construct name of toolbar icon for TOKEN."
(intern (concat "proof-toolbar-" (symbol-name token) "-icon")))
(defun proof-toolbar-enabler (token)
+ "Construct name of toolbar enabler for TOKEN."
(intern (concat "proof-toolbar-" (symbol-name token) "-enable-p")))
+
;;
;; Now the toolbar icons and buttons
;;
@@ -81,7 +85,8 @@
"Proof mode toolbar button list. Set in `proof-toolbar-setup'.")
(defun proof-toolbar-available-p ()
- (and ;; Check toolbar support...
+ "Check if toolbar support is available in this Emacs."
+ (and
window-system
(featurep 'tool-bar) ;; GNU Emacs tool-bar library
(or (image-type-available-p 'xpm) ;; and XPM
@@ -111,8 +116,8 @@ back the default toolbar."
(kill-local-variable 'tool-bar-map)))))
(defun proof-toolbar-enable ()
+ "Take action when the toolbar is enabled or disabled."
(proof-toolbar-setup)
- ;; make sure changes show up (any neater way?)
(redraw-display))
;;;###autoload (autoload 'proof-toolbar-toggle "proof-toolbar")
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el
index be52f32f..7286f9a6 100644
--- a/generic/proof-useropts.el
+++ b/generic/proof-useropts.el
@@ -1,6 +1,6 @@
;;; proof-useropts.el --- Global user options for Proof General
;;
-;; Copyright (C) 2009 LFCS Edinburgh.
+;; Copyright (C) 2009, 2010 LFCS Edinburgh.
;; Author: David Aspinall <David.Aspinall@ed.ac.uk> and others
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;
@@ -274,10 +274,8 @@ This is only useful for PG developers."
:type 'boolean
:group 'proof-user-options)
-;;; TEMPORARY FOR EXPERIMENTAL CODE:
-
(defcustom proof-use-parser-cache nil
- "*Non-nil to use a simple parsing cache (experimental).
+ "*Non-nil to use a simple parsing cache.
This can be helpful when editing and reprocessing large files.
This variable exists to disable the cache in case of problems."
:type 'boolean
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index ff064b5b..908bcf70 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -255,7 +255,7 @@ Usage: (defpgdefault SYM VALUE)"
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
-;; Prover-assistant specific customizations
+;; Prover-assistant specific customizations
;; which are recorded in `proof-assistant-settings'
;;
@@ -362,11 +362,11 @@ evaluate can be provided instead."
;; Buffers and filenames
(defun proof-file-truename (filename)
- "Returns the true name of the file FILENAME or nil if file non-existent."
+ "Return the true name of the file FILENAME or nil if file non-existent."
(and filename (file-exists-p filename) (file-truename filename)))
(defun proof-files-to-buffers (filenames)
- "Converts a list of FILENAMES into a list of BUFFERS."
+ "Convert a list of FILENAMES into a list of BUFFERS."
(let (bufs buf)
(dolist (file filenames)
(if (setq buf (find-buffer-visiting file))
@@ -374,7 +374,7 @@ evaluate can be provided instead."
bufs))
(defun proof-buffers-in-mode (mode &optional buflist)
- "Return a list of the buffers in the buffer list in major-mode MODE.
+ "Return a list of the buffers in the buffer list in major mode MODE.
Restrict to BUFLIST if it's set."
(let ((bufs-left (or buflist (buffer-list)))
bufs-got)
@@ -399,7 +399,7 @@ user accidently killing an associated buffer."
(set-buffer-modified-p nil)
(bury-buffer)
(error
- "Warning: buffer %s not killed; still associated with prover process."
+ "Warning: buffer %s not killed; still associated with prover process"
bufname)))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -564,7 +564,7 @@ No effect if buffer is dead."
If proof-general-debug is nil, do nothing."
(if proof-general-debug
(let ((formatted (apply 'format msg args)))
- (display-warning 'proof-general
+ (display-warning 'proof-general
formatted 'debug
"*PG Debug*"))))
@@ -738,7 +738,7 @@ It was constructed with `proof-deftoggle-fn'.")
(defmacro proof-deftoggle (var &optional othername)
"Define a function VAR-toggle for toggling a boolean customize setting VAR.
-The toggle function uses customize-set-variable to change the variable.
+The toggle function uses `customize-set-variable' to change the variable.
OTHERNAME gives an alternative name than the default <VAR>-toggle.
The name of the defined function is returned."
`(proof-deftoggle-fn (quote ,var) (quote ,othername)))
@@ -761,7 +761,7 @@ It was constructed with `proof-defintset-fn'.")
(defmacro proof-defintset (var &optional othername)
"Define a function <VAR>-intset for setting an integer customize setting VAR.
-The setting function uses customize-set-variable to change the variable.
+The setting function uses `customize-set-variable' to change the variable.
OTHERNAME gives an alternative name than the default <VAR>-intset.
The name of the defined function is returned."
`(proof-defintset-fn (quote ,var) (quote ,othername)))
@@ -793,14 +793,14 @@ The name of the defined function is returned."
;;;
(defun proof-escape-keymap-doc (string)
- ;; avoid work of substitute-command-keys
+ "Avoid action of `substitute-command-keys' on STRING."
(replace-regexp-in-string "\\\\" "\\\\=\\\\" string))
(defmacro proof-defshortcut (fn string &optional key)
"Define shortcut function FN to insert STRING, optional keydef KEY.
This is intended for defining proof assistant specific functions.
STRING is inserted using `proof-insert', which see.
-KEY is added onto proof-assistant map."
+KEY is added onto proof assistant map."
`(progn
(if ,key
(define-key (proof-ass keymap) (quote ,key) (quote ,fn)))
@@ -814,9 +814,9 @@ KEY is added onto proof-assistant map."
(defmacro proof-definvisible (fn string &optional key)
"Define function FN to send STRING to proof assistant, optional keydef KEY.
This is intended for defining proof assistant specific functions.
-STRING is sent using proof-shell-invisible-command, which see.
+STRING is sent using `proof-shell-invisible-command', which see.
STRING may be a string or a function which returns a string.
-KEY is added onto proof-assistant map."
+KEY is added onto proof assistant map."
`(progn
(if ,key
(define-key (proof-ass keymap) (quote ,key) (quote ,fn)))
@@ -941,7 +941,7 @@ it calls `proof-looking-at-syntactic-context'."
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
-;; Stripping output and message
+;; Stripping output and message
;;
(defsubst proof-shell-strip-output-markup (string &optional push)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-08 13:38:30 +0000