diff options
| author |  Erik Martin-Dorel <erik@martin-dorel.org> | 2018-08-23 00:01:12 +0200 |
|---|---|---|
| committer | Erik Martin-Dorel <erik@martin-dorel.org> | 2018-08-23 01:23:31 +0200 |
| commit | 86d22428959a0f5aecef270e0f4dd7d4b5712fc3 (patch) | |
| tree | 676fe59b7644498172f96b6da605745a6bf71a13 | |
| parent | 3ba86af3271111cb056676c631b7caa6897e06f1 (diff) | |
Fix most doc issues raised by (checkdoc)
60 files changed, 1029 insertions, 909 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 5a555df5..308ca865 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -69,7 +69,7 @@ ;;; The abbrev table built from keywords tables ;#s and @{..} are replaced by holes by holes-abbrev-complete (defun coq-install-abbrevs () - "install default abbrev table for coq if no other already is." + "Install default abbrev table for coq if no other already is." (if (boundp 'coq-mode-abbrev-table) ;; da: this test will always fail. Assume bound-->non-empty ;; (not (equal coq-mode-abbrev-table (make-abbrev-table)))) @@ -353,9 +353,11 @@ It was constructed with `proof-defstringset-fn'.") ["Compile" coq-Compile t])))) (setq-default coq-help-menu-entries - '(["help on setting prog name persistently for a file" + '(["help on setting prog name persistently for a file" coq-local-vars-list-show-doc t])) (setq-default coq-other-buffers-menu-entries coq-menu-common-entries) (provide 'coq-abbrev) + +;;; coq-abbrev.el ends here diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el index 9126c2ae..cecfdcf1 100644 --- a/coq/coq-autotest.el +++ b/coq/coq-autotest.el @@ -97,3 +97,7 @@ (pg-autotest timetaken 'total) (pg-autotest exit)) + +(provide 'coq-autotest) + +;;; coq-autotest.el ends here diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index c94cd8b7..936ad923 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -78,7 +78,7 @@ Must be used together with `coq-par-enable'." (defun coq-switch-compilation-method () - "Set function for coq-compile-parallel-in-background." + "Set function for function ‘coq-compile-parallel-in-background’." (if coq-compile-parallel-in-background (progn (coq-par-enable) @@ -91,7 +91,7 @@ Must be used together with `coq-par-enable'." (condition-case nil (with-temp-buffer (setq status - (call-process "getconf" nil (current-buffer) t + (call-process "getconf" nil (current-buffer) t "_NPROCESSORS_ONLN")) (setq ncpus (string-to-number (buffer-string)))) (error @@ -103,7 +103,7 @@ Must be used together with `coq-par-enable'." (defvar coq--max-background-vio2vo-percentage-shadow 40 "Internal shadow value of `coq-max-background-vio2vo-percentage'. This variable does always contain the same value as -`coq-max-background-vio2vo-percentage'. It is used only to break +`coq-max-background-vio2vo-percentage'. It is used only to break the dependency cycle between `coq-set-max-vio2vo-jobs' and `coq-max-background-vio2vo-percentage'.") @@ -167,7 +167,7 @@ Ignore any quick setting for Coq versions before 8.5." (defcustom coq-compile-before-require nil "If non-nil, check dependencies of required modules and compile if necessary. If non-nil ProofGeneral intercepts \"Require\" commands and checks if the -required library module and its dependencies are up-to-date. If not, they +required library module and its dependencies are up-to-date. If not, they are compiled from the sources before the \"Require\" command is processed. This option can be set/reset via menu @@ -181,12 +181,12 @@ This option can be set/reset via menu (defcustom coq-compile-parallel-in-background nil "Choose the internal compilation method. When Proof General compiles itself, you have the choice between -two implementations. If this setting is nil, then Proof General +two implementations. If this setting is nil, then Proof General uses the old implementation and compiles everything sequentially -with synchronous job. With this old method Proof General is -locked during compilation. If this setting is t, then the new +with synchronous job. With this old method Proof General is +locked during compilation. If this setting is t, then the new method is used and compilation jobs are dispatched in parallel in -the background. The maximal number of parallel compilation jobs +the background. The maximal number of parallel compilation jobs is set with `coq-max-background-compilation-jobs'. This option can be set/reset via menu @@ -207,58 +207,58 @@ This option can be set/reset via menu "Control quick compilation, vio2vo and vio/vo files auto compilation. This option controls whether ``-quick'' is used for parallel background compilation and whether up-date .vo or .vio files are -used or deleted. Please use the customization system to change +used or deleted. Please use the customization system to change this option to ensure that any ``-quick'' setting is ignored for Coq before 8.5. Note that ``-quick'' can be noticebly slower when your sources do -not declare section variables with ``Proof using''. Note that +not declare section variables with ``Proof using''. Note that even if you do declare section variables, ``-quick'' is typically slower on small files. Use the default `no-quick', if you have not yet switched to -``Proof using''. Use `quick-no-vio2vo', if you want quick -recompilation without producing .vo files. Value +``Proof using''. Use `quick-no-vio2vo', if you want quick +recompilation without producing .vo files. Value `quick-and-vio2vo' updates missing prerequisites with ``-quick'' and starts vio2vo conversion on a subset of the availables cores (see `coq-compile-vio2vo-percentage') when the quick recompilation finished (but see below for a .vio .vo -incompatibility caveat). Note that all the previously described +incompatibility caveat). Note that all the previously described modes might load .vio files and that you therefore might not -notice certain universe inconsistencies. Finally, use `ensure-vo' +notice certain universe inconsistencies. Finally, use `ensure-vo' for only importing .vo files with complete universe checks. Detailed description of the 4 modes: no-quick Compile outdated prerequisites without ``-quick'', producing .vo files, but don't compile prerequisites - for which an up-to-date .vio file exists. Delete + for which an up-to-date .vio file exists. Delete or overwrite outdated .vo files. quick-no-vio2vo Compile outdated prerequisites with ``-quick'', producing .vio files, but don't compile prerequisites - for which an up-to-date .vo file exists. Delete + for which an up-to-date .vo file exists. Delete or overwrite outdated .vio files. quick-and-vio2vo Same as `quick-no-vio2vo', but start vio2vo processes after the last ``Require'' command has been processed - to convert the vio dependencies into vo files. With this + to convert the vio dependencies into vo files. With this mode you might see asynchronous errors from vio2vo compilation while you are processing stuff far below the - last require. vio2vo compilation is done on a subset of + last require. vio2vo compilation is done on a subset of the available cores, see `coq-compile-vio2vo-percentage'. When `coq-compile-keep-going' is set, vio2vo compilation is scheduled for those files for which coqc compilation was successful. Warning: This mode does only work when you process require - commands in batches. Slowly single-stepping through require's + commands in batches. Slowly single-stepping through require's might lead to inconsistency errors when loading some libraries, see Coq issue #5223. ensure-vo Ensure that all library dependencies are present as .vo files and delete outdated .vio files or .vio files that - are more recent than the corresponding .vo file. This + are more recent than the corresponding .vo file. This setting is the only one that ensures soundness. This option can be set via menu @@ -296,9 +296,9 @@ This option can be set/reset via menu (defcustom coq-max-background-compilation-jobs 'all-cpus "Maximal number of parallel jobs, if parallel compilation is enabled. Use the number of available CPU cores if this is set to -'all-cpus. This variable is the user setting. The value that is -really used is `coq--internal-max-jobs'. Use `coq-max-jobs-setter' -or the customization system to change this variable. Otherwise +'all-cpus. This variable is the user setting. The value that is +really used is `coq--internal-max-jobs'. Use `coq-max-jobs-setter' +or the customization system to change this variable. Otherwise your change will have no effect, because `coq--internal-max-jobs' is not adapted." :type '(choice (const :tag "use all CPU cores" all-cpus) @@ -326,13 +326,13 @@ with 'quick-and-vio2vo, see Coq issue #5223." :group 'coq-auto-compile) (defcustom coq-compile-command "" - "External compilation command. If empty ProofGeneral compiles itself. + "External compilation command. If empty ProofGeneral compiles itself. If unset (the empty string) ProofGeneral computes the dependencies of -required modules with coqdep and compiles as necessary. This internal +required modules with coqdep and compiles as necessary. This internal dependency checking does currently not handle ML modules. If a non-empty string, the denoted command is called to do the -dependency checking and compilation. Before executing this +dependency checking and compilation. Before executing this command the following keys are substituted as follows: %p the (physical) directory containing the source of the required module @@ -363,8 +363,8 @@ minibuffer if `coq-confirm-external-compilation' is t." ("%r" requiring-file)) "Substitutions for `coq-compile-command'. Value must be a list of substitutions, where each substitution is -a 2-element list. The first element of a substitution is the -regexp to substitute, the second the replacement. The replacement +a 2-element list. The first element of a substitution is the +regexp to substitute, the second the replacement. The replacement is evaluated before passing it to `replace-regexp-in-string', so it might be a string, or one of the symbols 'physical-dir, 'module-object, 'module-source, 'qualified-id and @@ -380,7 +380,7 @@ that contains the \"Require\".") "Buffers to save before checking dependencies for compilation. There are two orthogonal choices: Firstly one can save all or only the coq buffers, where coq buffers means all buffers in coq mode except the current -buffer. Secondly, Emacs can ask about each such buffer or save all of them +buffer. Secondly, Emacs can ask about each such buffer or save all of them unconditionally. This makes four permitted values: 'ask-coq to confirm saving all @@ -407,7 +407,7 @@ This option can be set via menu (defcustom coq-lock-ancestors t "If non-nil, lock ancestor module files. If external compilation is used (via `coq-compile-command') then -only the direct ancestors are locked. Otherwise all ancestors are +only the direct ancestors are locked. Otherwise all ancestors are locked when the \"Require\" command is processed. This option can be set via menu @@ -433,12 +433,12 @@ This option can be set/reset via menu (defcustom coq-compile-ignored-directories nil "Directories in which ProofGeneral should not compile modules. List of regular expressions for directories in which ProofGeneral -should not compile modules. If a library file name matches one +should not compile modules. If a library file name matches one of the regular expressions in this list then ProofGeneral does neither compile this file nor check its dependencies for -compilation. It makes sense to include non-standard coq library +compilation. It makes sense to include non-standard coq library directories here if they are not changed and if they are so big -that dependency checking takes noticeable time. The regular +that dependency checking takes noticeable time. The regular expressions in here are always matched against the .vo file name, regardless whether ``-quick'' would be used to compile the file or not." @@ -451,12 +451,12 @@ or not." "and has not been found") "Regexp to match errors in the output of coqdep. coqdep indicates errors not always via a non-zero exit status, -but sometimes only via printing warnings. This regular expression +but sometimes only via printing warnings. This regular expression is used for recognizing error conditions in the output of -coqdep (when coqdep terminates with exit status 0). Its default +coqdep (when coqdep terminates with exit status 0). Its default value matches the warning that some required library cannot be found on the load path and ignores the warning for finding a -library at multiple places in the load path. If you want to turn +library at multiple places in the load path. If you want to turn the latter condition into an error, then set this variable to \"^\\*\\*\\* Warning\"." :type 'string @@ -468,7 +468,7 @@ the latter condition into an error, then set this variable to "[ \t\n]*\\([A-Za-z0-9_']+\\(\\.[A-Za-z0-9_']+\\)*\\)[ \t\n]*" "Regular expression matching one Coq module identifier. Should match precisely one complete module identifier and surrounding -white space. The module identifier must be matched with group number 1. +white space. The module identifier must be matched with group number 1. Note that the trailing dot in \"Require A.\" is not part of the module identifier and should therefore not be matched by this regexp.") @@ -488,25 +488,25 @@ modules are matched separately with `coq-require-id-regexp'") "Name of the buffer to display error messages from coqc and coqdep.") (defvar coq--debug-auto-compilation nil - "*Display more messages during compilation") + "*Display more messages during compilation.") ;;; basic utilities (defun time-less-or-equal (time-1 time-2) - "Return `t' if time value time-1 is earlier or equal to time-2. + "Return t if time value TIME-1 is earlier or equal to TIME-2. A time value is a list of two, three or four integers of the form (high low micro pico) as returned by `file-attributes' or -'current-time'. First element high contains the upper 16 bits and +'current-time'. First element high contains the upper 16 bits and the second low the lower 16 bits of the time." (not (time-less-p time-2 time-1))) (defun coq-max-dep-mod-time (dep-mod-times) "Return the maximum in DEP-MOD-TIMES. Argument DEP-MOD-TIMES is a list where each element is either a -time value (see `time-less-or-equal') or 'just-compiled. The +time value (see `time-less-or-equal') or 'just-compiled. The function returns the maximum of the elements in DEP-MOD-TIMES, -where 'just-compiled is considered the greatest time value. If +where 'just-compiled is considered the greatest time value. If DEP-MOD-TIMES is empty it returns nil." (let ((max nil)) (while dep-mod-times @@ -526,10 +526,10 @@ DEP-MOD-TIMES is empty it returns nil." (defun coq-compile-ignore-file (lib-obj-file) "Check whether ProofGeneral should handle compilation of LIB-OBJ-FILE. -Return `t' if ProofGeneral should skip LIB-OBJ-FILE and `nil' if -ProofGeneral should handle the file. For normal users it does, +Return t if ProofGeneral should skip LIB-OBJ-FILE and nil if +ProofGeneral should handle the file. For normal users it does, for instance, not make sense to let ProofGeneral check if the coq -standard library is up-to-date. This function is always invoked +standard library is up-to-date. This function is always invoked on the .vo file name, regardless whether the file would be compiled with ``-quick'' or not." (if (some @@ -556,7 +556,7 @@ Chops off the last character of LIB-OBJ-FILE to convert \"x.vo\" to \"x.v\"." (defun coq-library-vio-of-vo-file (vo-obj-file) "Return .vio file name for VO-OBJ-FILE. -Changes the suffix from .vio to .vo. VO-OBJ-FILE must have a .vo suffix." +Changes the suffix from .vio to .vo. VO-OBJ-FILE must have a .vo suffix." (concat (coq-library-src-of-vo-file vo-obj-file) "io")) @@ -583,7 +583,7 @@ Changes the suffix from .vio to .vo. VO-OBJ-FILE must have a .vo suffix." (defun coq-compile-display-error (command error-message display) "Display COMMAND and ERROR-MESSAGE in `coq--compile-response-buffer'. -If needed, reinitialize `coq--compile-response-buffer'. Then +If needed, reinitialize `coq--compile-response-buffer'. Then display COMMAND and ERROR-MESSAGE." (unless (buffer-live-p (get-buffer coq--compile-response-buffer)) (coq-init-compile-response-buffer)) @@ -598,10 +598,10 @@ display COMMAND and ERROR-MESSAGE." (defun coq-init-compile-response-buffer (&optional command) "Initialize the buffer for the compilation output. -If `coq--compile-response-buffer' exists, empty it. Otherwise +If `coq--compile-response-buffer' exists, empty it. Otherwise create a buffer with name `coq--compile-response-buffer', put it into `compilation-mode' and store it in -`coq--compile-response-buffer' for later use. Argument COMMAND is +`coq--compile-response-buffer' for later use. Argument COMMAND is the command whose output will appear in the buffer." (let ((buffer-object (get-buffer coq--compile-response-buffer))) (if buffer-object @@ -675,10 +675,10 @@ from `coq-compile-save-some-buffers' to (defun coq-compile-save-buffer-filter () "Filter predicate for `coq-compile-save-some-buffers'. -See also `save-some-buffers'. Returns t for buffers with major +See also `save-some-buffers'. Return t for buffers with major mode 'coq-mode' different from `coq-compile-buffer-with-current-require' and nil for all other -buffers. The buffer to test must be current." +buffers. The buffer to test must be current." (and (eq major-mode 'coq-mode) (not (eq coq-compile-buffer-with-current-require @@ -686,7 +686,7 @@ buffers. The buffer to test must be current." (defun coq-compile-save-some-buffers () "Save buffers according to `coq-compile-auto-save'. -Uses the local variable coq-compile-buffer-with-current-require to pass the +Uses the local variable ‘coq-compile-buffer-with-current-require’ to pass the current buffer (which contains the Require command) to `coq-compile-save-buffer-filter'." (let ((coq-compile-buffer-with-current-require (current-buffer)) @@ -711,10 +711,10 @@ current buffer (which contains the Require command) to (defun coq-switch-buffer-kill-proof-shell () "Kill the proof shell without asking the user. -This function is for `proof-deactivate-scripting-hook'. It kills +This function is for `proof-deactivate-scripting-hook'. It kills the proof shell without asking the user for confirmation (assuming she agreed already on switching the active -scripting buffer). This is needed to ensure the load path is +scripting buffer). This is needed to ensure the load path is correct in the new scripting buffer." (unless proof-shell-exit-in-progress (proof-shell-exit t))) diff --git a/coq/coq-db.el b/coq/coq-db.el index dccdca52..cad149a2 100644 --- a/coq/coq-db.el +++ b/coq/coq-db.el @@ -78,10 +78,10 @@ new keyword to colorize.") (defun coq-insert-from-db (db prompt &optional alwaysjump) "Ask for a keyword, with completion on keyword database DB and insert. -Insert corresponding string with holes at point. If an insertion -function is present for the keyword, call it instead. see -`coq-syntax-db' for DB structure. If ALWAYSJUMP is non nil, jump -to the first hole even if more than one." +Insert corresponding string with holes at point. If an insertion +function is present for the keyword, call it instead. See +`coq-syntax-db' for DB structure. If ALWAYSJUMP is non nil, jump to +the first hole even if more than one." (let* ((tac (completing-read (concat prompt " (TAB for completion): ") db nil nil)) (infos (cddr (assoc tac db))) @@ -96,7 +96,7 @@ to the first hole even if more than one." (defun coq-build-command-from-db (db prompt &optional preformatquery) - "Ask for a keyword, with completion on keyword database DB and send to coq. + "Ask for a keyword, with completion on keyword database DB and send to Coq. See `coq-syntax-db' for DB structure." ;; Next invocation of minibuffer (read-string below) will first recursively ;; ask for a command in db and expand it with holes. This way the cursor will @@ -142,7 +142,7 @@ regexp. See `coq-syntax-db' for DB structure." ; (color (concat "\\_<" (nth 4 hd) "\\_>"))) ; colorization string ;; TODO delete doublons (when (and color (or (not filter) (funcall filter hd))) - (setq res + (setq res (nconc res (list (concat "\\_<" color "\\_>"))))) (setq l tl))) @@ -204,8 +204,8 @@ Used by `coq-build-menu-from-db', which you should probably use instead. See (let ((menu-entry (vector ;; menu entry label - (concat menu - (if (not abbrev) "" + (concat menu + (if (not abbrev) "" (concat spaces "(" abbrev keybind-abbrev ")"))) ;;insertion function if present otherwise insert completion (if insertfn insertfn `(holes-insert-and-expand ,complt)) @@ -254,8 +254,7 @@ structure." res)) (defcustom coq-holes-minor-mode t - "*Whether to apply holes minor mode (see `holes-show-doc') in - coq mode." + "*Whether to apply holes minor mode (see `holes-show-doc') in coq mode." :type 'boolean :group 'coq) @@ -298,7 +297,7 @@ See `coq-syntax-db' for DB structure." "Face for names of closing tactics in proof scripts." :group 'proof-faces) -;;A face for cheating tactics +;;A face for cheating tactics ;; We use :box in addition to :background because box remains visible in ;; locked-region. :reverse-video is another solution. (defface coq-cheat-face diff --git a/coq/coq-indent.el b/coq/coq-indent.el index 405cbb46..6e8ba013 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.el @@ -18,6 +18,10 @@ ;; This is experimental, the code is rather ugly for the moment. ;; + +;;; Commentary: +;; + ;;; Code: (require 'coq-syntax) @@ -85,10 +89,10 @@ ;;;; End of regexps (defun coq-indent-goal-command-p (str) - "Syntactical detection of a coq goal opening. -Only used in indentation code and in -v8.0 compatibility mode. Module, Definition and Function need a special parsing to -detect if they start something or not." + "Syntactical detection of a Coq goal opening. +Only used in indentation code and in v8.0 compatibility mode. +Module, Definition and Function need a special parsing to detect +if they start something or not." (let* ((match (coq-count-match "\\_<match\\_>" str)) (with (coq-count-match "\\_<with\\_>" str)) (letwith (+ (coq-count-match "\\_<let\\_>" str) (- with match))) @@ -105,7 +109,7 @@ detect if they start something or not." (defconst coq-simple-cmd-ender-prefix-regexp "[^.]\\|\\=\\|\\.\\." - "Used internally. Matches the allowed prefixes of coq \".\" command ending.") + "Used internally. Matches the allowed prefixes of coq \".\" command ending.") (defconst coq-bullet-regexp-nospace "\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+" "Matches single bullet, WARNING: Lots of false positive. @@ -133,25 +137,24 @@ No context checking.") (concat "\\(?:\\(?2:" coq-simple-cmd-ender-prefix-regexp "\\)\\(?1:\\.\\)\\(?3:\\s-\\|\\'\\)\\)") "Matches coq regular syntax for ending a command (except bullets and curlies). -This should match EXACTLY command ending syntax. No false -positive should be accepted. \"...\" is matched as \".\" with a +This should match EXACTLY command ending syntax. No false +positive should be accepted. \"...\" is matched as \".\" with a left context \"..\". There are 3 substrings (2 and 3 may be nil): * number 1 is the real bullet string, * number 2 is the left context matched that is not part of the bullet -* number 3 is the right context matched that is not part of the bullet -") +* number 3 is the right context matched that is not part of the bullet") ;; captures a lot of false bullets, need to check that the commaand is ;; empty. When searching forward (typically when splitting the buffer ;; into commands commands) we can't do better than that. (defconst coq-bullet-end-command (concat "\\(?:\\(?2:\\s-\\|\\=\\)" "\\(?1:" coq-bullet-regexp-nospace "\\)\\)") - "Matches ltac bullets. WARNING: lots of false positive. + "Matches ltac bullets. WARNING: lots of false positive. This matches more than real bullets as - + and * may match this -when used in regular expressions. See +when used in regular expressions. See `coq-bullet-end-command-backward' for a more precise regexp (but only when searching backward).") @@ -160,7 +163,7 @@ only when searching backward).") (concat "\\(?:\\(?2:" coq-bullet-prefix-regexp "\\)\\(?1:\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+\\)\\)") "Matches ltac bullets when searching backward. -This should match EXACTLY bullets. No false positive should be accepted. +This should match EXACTLY bullets. No false positive should be accepted. There are 2 substrings: * number 1 is the real bullet string, * number 2 is the left context matched that is not part of the bullet" ) @@ -169,14 +172,14 @@ There are 2 substrings: (concat "\\(?:\\(?1:" "\\(?:" coq-bullet-prefix-regexp"\\)?" "{\\)\\(?3:[^|]\\)\\|\\(?2:[^|]\\|\\=\\)\\(?1:}\\)\\)") - "Matches ltac curlies when searching backward. Warning: False positive. + "Matches ltac curlies when searching backward. Warning: False positive. There are 3 substrings (2 and 3 may be nil): * number 1 is the real bullet string, * number 2 is the left context matched that is not part of the bullet * number 3 is the right context matched that is not part of the bullet -This matches more than real ltac curlies. See +This matches more than real ltac curlies. See `coq-bullet-end-command-backward' for a more precise regexp (but only when searching backward).") @@ -187,7 +190,7 @@ only when searching backward).") "\\|\\(?1:}\\)\\)\\)") "Matches ltac curly brackets when searching backward. -This should match EXACTLY script structuring curlies. No false +This should match EXACTLY script structuring curlies. No false positive should be accepted. There are 3 substrings (2 and 3 may be nil): * number 1 is the real bullet string, @@ -198,7 +201,8 @@ There are 3 substrings (2 and 3 may be nil): (concat coq-period-end-command "\\|" coq-bullet-end-command "\\|" coq-curlybracket-end-command) - "Matches end of commands (and ltac bullets and curlies). WARNING: False positive. + "Matches end of commands (and ltac bullets and curlies). +WARNING: False positive. There are 3 substrings: * number 1 is the real coq ending string, @@ -206,10 +210,10 @@ There are 3 substrings: * number 3 is the right context matched that is not part of the ending string WARNING: this regexp accepts some curly brackets and bullets (+ - -*) with no sufficient context verification. Lots of false -positive are matched. Currently bullets and curlies are always +*) with no sufficient context verification. Lots of false +positive are matched. Currently bullets and curlies are always ending an empty command, so we just need to check that the -command ended by the bullet-like regexp is empty. This is done in +command ended by the bullet-like regexp is empty. This is done in coq-smie.el, and see `coq-end-command-regexp-backward' for a more precise regexp (but only when searching backward).") @@ -251,7 +255,7 @@ Return nil if not found." (defun coq-skip-until-one-comment-backward () "Skips comments and normal text until finding an unclosed comment start. Return nil if not found. Point is moved to the the unclosed comment start -if found, to (point-max) otherwise. return true if found, nil otherwise." +if found, to (point-max) otherwise. Return t if found, nil otherwise." (if (= (point) (point-min)) nil (ignore-errors (backward-char 1)) ; if point is between '(' and '*' (if (looking-at coq-comment-start-regexp) t @@ -281,9 +285,9 @@ if found, to (point-max) otherwise. return true if found, nil otherwise." (defun coq-find-comment-start () "Go to the current comment start. -If inside nested comments, go to the start of the -outer most comment. Return the position of the comment start. If not inside a -comment, return nil and does not move the point." +If inside nested comments, go to the start of the outer most comment. +Return the position of the comment start. If not inside a comment, +return nil and does not move the point." (when (coq-looking-at-comment) (let ((prevpos (point)) (init (point))) (while (coq-skip-until-one-comment-backward) @@ -293,9 +297,9 @@ comment, return nil and does not move the point." (defun coq-find-comment-end () "Go to the current comment end. -If inside nested comments, go to the end of the -outer most comment. Return the position of the end of comment end. If not inside a -comment, return nil and does not move the point." +If inside nested comments, go to the end of the outer most +comment. Return the position of the end of comment end. If not inside +a comment, return nil and does not move the point." (let ((prevpos (point)) (init (point))) (while (coq-skip-until-one-comment-forward) (setq prevpos (point))) @@ -317,10 +321,10 @@ Use this one for coq instead of the generic one." (defun coq-find-not-in-comment-backward (reg &optional lim submatch) "Moves to the first not commented occurrence of REG found looking up. -The point is -put exactly before the occurrence if SUBMATCH is nil, otherwise the point is put -before SUBMATCHnth matched sub-expression (see `match-string'). If no occurrence is -found, go as far as possible and return nil." +The point is put exactly before the occurrence if SUBMATCH is nil, +otherwise the point is put before SUBMATCHnth matched +sub-expression (see `match-string'). If no occurrence is found, go as +far as possible and return nil." (coq-find-comment-start) ; first go out of comment if inside some (let ((found nil) (continue t) (regexp (concat coq-comment-end-regexp "\\|" reg))) @@ -407,10 +411,10 @@ Comments are ignored, of course." (defun coq-script-parse-cmdend-forward (&optional limit) "Move to the first end of command found looking forward from point. Point is put exactly after the ending token (but before matching -substring if present). If no end command is found, go as far as +substring if present). If no end command is found, go as far as possible and return nil. End of command appearing in comments are -ignored. This function makes use of the substring 1 of the -command end regexp." +ignored. This function makes use of the substring 1 of the command end +regexp." (if (looking-at proof-script-comment-start-regexp) ;; Handle comments (if (proof-script-generic-parse-find-comment-end) 'comment) @@ -462,7 +466,7 @@ command end regexp." (defun coq-script-parse-cmdend-backward (&optional limit) "Move to the first end of command (not commented) found looking up. Point is put exactly before the last ending token (before the last -\".\" if \"...\"). If no end command is found, go as far as possible +\".\" if \"...\"). If no end command is found, go as far as possible and return nil." (if (looking-at proof-script-comment-start-regexp) ;; Handle comments @@ -507,8 +511,8 @@ and return nil." (defun coq-find-current-start () "Move to the start of command at point. -The point is put exactly after the end of previous command, or at the (point-min if -there is no previous command)." +The point is put exactly after the end of previous command, or at +the (point-min) if there is no previous command." (coq-script-parse-cmdend-backward) (when (proof-looking-at "\\.\\s-\\|{\\|}\\|\\++\\|\\*+\\|-+") @@ -586,8 +590,8 @@ Point is moved at the end of the match if found, at LIM otherwise." (defun coq-find-no-syntactic-on-line () "Return non-nil if there is a not commented non white character on the line. -Moves point to this char or to the end of the line if not found (and return nil in -this case)." +Moves point to this char or to the end of the line if not found (and +return nil in this case)." (let ((eol (save-excursion (end-of-line) (point)))) (back-to-indentation) (while (and (coq-looking-at-syntactic-context) @@ -644,7 +648,9 @@ not inside the {} of a record)." (defun coq-find-unclosed (&optional optlvl limit openreg closereg) - "Finds the first unclosed open item (backward), counter starts to optlvl (default 1) and stops when reaching limit (default point-min)." + "Finds the first unclosed open item (backward). +Counter starts to OPTLVL (default 1) and stops when reaching +LIMIT (default point-min)." (let* ((lvl (or optlvl 1)) (open-re (if openreg @@ -703,7 +709,10 @@ Returns point if found." (defun coq-find-unopened (&optional optlvl limit) - "Finds the last unopened close item (looking forward from point), counter starts to OPTLVL (default 1) and stops when reaching limit (default point-max). This function only works inside an expression." + "Find the last unopened close item (looking forward from point). +Counter starts to OPTLVL (default 1) and stops when reaching +LIMIT (default ‘point-max’). This function only works inside an +expression." (let ((lvl (or optlvl 1)) after nextpt endpt) (save-excursion @@ -746,7 +755,7 @@ Returns point if found." (defun coq-find-last-unopened (&optional optlvl limit) - "Backward moves to and returns the point of the last close item that is not opened after limit." + "Backward move to and return the point of the last close item, not opened after LIMIT." (let ((last nil)) (while (coq-find-unopened optlvl limit) (setq last (point)) @@ -757,7 +766,8 @@ Returns point if found." (defun coq-end-offset (&optional limit) - "Find the first unclosed open indent item, and returns its column. Stop when reaching limit (defaults tp point-min)." + "Find the first unclosed open indent item, and return its column. +Stop when reaching LIMIT (default to ‘point-min’)." (save-excursion (let ((found nil) (anyreg (proof-regexp-alt "\\`" proof-indent-any-regexp))) @@ -808,7 +818,7 @@ Returns point if found." (defun coq-indent-command-offset (kind prevcol prevpoint) - "Returns the indentation offset of the current line. + "Return the indentation offset of the current line. This function indents a *command* line (the first line of a command). Use `coq-indent-expr-offset' to indent a line belonging to an expression." (let ((diff-goal-save-current @@ -874,10 +884,11 @@ Use `coq-indent-expr-offset' to indent a line belonging to an expression." ;; inside the accolades of a record. (defun coq-indent-expr-offset (kind prevcol prevpoint record) - "Returns the indentation column of the current line. -This function indents a *expression* line (a line inside of a command). Use -`coq-indent-command-offset' to indent a line belonging to a command. The fourth -argument must be t if inside the {}s of a record, nil otherwise." + "Return the indentation column of the current line. +This function indents a *expression* line (a line inside of a +command). Use `coq-indent-command-offset' to indent a line belonging +to a command. The fourth argument RECORD must be t if inside the {}s +of a record, nil otherwise." ;(message "COQ-INDENT-EXPR-OFFSET") (let ((pt (point)) real-start) (save-excursion diff --git a/coq/coq-local-vars.el b/coq/coq-local-vars.el index a097043a..b8c5d7e3 100644 --- a/coq/coq-local-vars.el +++ b/coq/coq-local-vars.el @@ -33,11 +33,11 @@ PROJECT FILE The recommended way of setting coqtop options (-I, -R and others) -is to use a project file. See the coq documentation (\"generating -makefile\") for details. The default name of the project file is +is to use a project file. See the coq documentation (\"generating +makefile\") for details. The default name of the project file is \"_CoqProject\" (can be configured via `coq-project-filename') and its content should be a list of options to be given to -coq_makefile (one option per line). Here is an example: +coq_makefile (one option per line). Here is an example: -R foo bar -I foo2 @@ -45,34 +45,34 @@ coq_makefile (one option per line). Here is an example: ...(optionally followed by all .v files to be compiled) If `coq-use-project-file' is t (default) ProofGeneral reads the -project file and sets coqtop options accordingly (via variables -`coq-load-path' and `coq-prog-args'). In this example the coqtop -invocation will be: +project file and sets coqtop options accordingly (via variable +`coq-load-path' and variable `coq-prog-args'). In this example the +coqtop invocation will be: coqtop -foo3 -R foo bar -I foo2 FILE VARIABLES If for some reason you want to avoid or override the project file -method, you can use the file variables (info:(Emacs)File -Variables). This feature of Emacs allows to set Emacs variables -on a per-file basis. File Variables are (usually) written as a -list at the end of the file. +method, you can use the file variables. See Info node ‘(emacs)File +Variables’. This feature of Emacs allows to set Emacs variables on a +per-file basis. File Variables are (usually) written as a list at the +end of the file. We provide the following feature to help you: \\[coq-ask-insert-coq-prog-name] builds a standard file variable -list for a coq file by asking you some questions. It is +list for a coq file by asking you some questions. It is accessible in the menu `Coq' -> `COQ PROG (ARGS)' -> `Set coq prog *persistently*'. You should be able to use this feature without reading the rest -of this documentation, which explains how it is used for coq. For +of this documentation, which explains how it is used for coq. For more precision, refer to the Emacs info manual at ((Emacs)File Variables). In Coq projects involving multiple directories, it is usually -necessary to set the variable `coq-load-path' for each file. For +necessary to set the variable `coq-load-path' for each file. For example, if the file .../dir/bar/foo.v builds on material in .../dir/theories/, then one would put the following local variable section at the end of foo.v: @@ -84,17 +84,17 @@ variable section at the end of foo.v: *) This way the necessary \"-I\" options are added to all -invocations of `coqtop', `coqdep' and `coqc'. Note that the -option \"-I\" \"../theories\" is specific to file foo.v. Setting +invocations of `coqtop', `coqdep' and `coqc'. Note that the +option \"-I\" \"../theories\" is specific to file foo.v. Setting `coq-load-path' globally via Emacs Customization is therefore -usually inappropriate. With this local variables list, Emacs will +usually inappropriate. With this local variables list, Emacs will set `coq-load-path' only when inside a buffer that visits foo.v. Other buffers can have their own value of `coq-load-path' (probably coming from their own local variable lists). If you use `make' for the compilation of coq modules you can set -`coq-compile-command' as local variable. For instance, if the +`coq-compile-command' as local variable. For instance, if the makefile is located in \".../dir\", you could set \(* @@ -117,8 +117,8 @@ necessary.)") (defun coq-insert-coq-prog-name (progname coqloadpath) "Insert or modify the local variables `coq-prog-name' and `coq-load-path'. -Set them to PROGNAME and PROGARGS respectively. These variables describe the -coqtop command to be launched on this file." +Set them to PROGNAME and COQLOADPATH respectively. These variables +describe the coqtop command to be launched on this file." (add-file-local-variable 'coq-prog-name progname) (add-file-local-variable 'coq-load-path coqloadpath) ;; coq-guess-command-line uses coq-prog-name, so set it @@ -147,7 +147,7 @@ Do not insert the default directory." (defun coq-ask-load-path (&optional olddirs) "Ask for and return the information to put into `coq-load-path'. -Optional argument OLDVALUE specifies the previous value of `coq-load-path', it +Optional argument OLDDIRS specifies the previous value of `coq-load-path', it will be used to suggest values to the user." (let (loadpath option) ;; first suggest previous directories diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el index 17fe12d5..e3daebcd 100644 --- a/coq/coq-par-compile.el +++ b/coq/coq-par-compile.el @@ -16,7 +16,7 @@ ;;; Commentary: ;; -;; This file implements compilation of required modules. The +;; This file implements compilation of required modules. The ;; compilation is done in parallel in the background (in contrast to ;; what you find in coq-seq-compile.el). ;; @@ -202,7 +202,7 @@ ;; modification time of some ancestor ;; value might be an Emacs time or ;; 'just-compiled -;; 'queue-dependant - next top-level job, only present in top-level jobs +;; 'queue-dependant - next top-level job, only present in top-level jobs ;; 'queue-dependant-waiting - t if this is a top-level job that has ;; to wait until previous top-level jobs ;; finish. In this waiting time, modules @@ -211,7 +211,7 @@ ;; this property becomes nil ;; 'src-file - the .v file name ;; 'load-path - value of coq-load-path, propagated to all -;; dependencies +;; dependencies ;; 'ancestors - list of ancestor jobs, for real compilation jobs ;; this list includes the job itself; may contain ;; duplicates @@ -271,10 +271,10 @@ ;; 'coq-process-continuation - the continuation to be called when ;; the process finishes. Either ;; coq-par-process-coqdep-result or -;; coq-par-coqc-continuation +;; coq-par-coqc-continuation ;; 'coq-process-output - the output of the process ;; 'coq-process-command - the command for error reporting -;; (as string list) +;; (as string list) ;; 'coq-par-process-killed - t if this process has been killed ;; 'coq-process-rm - if not nil, a file to be deleted when ;; the process is killed @@ -289,7 +289,7 @@ ;; (get v 'type) ;; (get v 'src-file) ;; (get v 'state) -;; (mapcar (lambda (p) (get p 'name)) +;; (mapcar (lambda (p) (get p 'name)) ;; (get v 'coqc-dependants)) ;; (get v 'queue-dependant)) ;; (mapc (lambda (p) (when (eq (get p 'type) 'clone) @@ -302,7 +302,7 @@ ;; (get v 'type) ;; (get v 'src-file) ;; (get v 'state) -;; (mapcar (lambda (p) (get p 'name)) +;; (mapcar (lambda (p) (get p 'name)) ;; (get v 'coqc-dependants)) ;; (get v 'queue-dependant))) ;; clones)) @@ -314,10 +314,10 @@ (defvar coq--compilation-object-hash nil "Hash for storing the compilation jobs. -This hash only stores real compilation jobs and no clones. They -are stored in order to avoid double compilation. The jobs stored +This hash only stores real compilation jobs and no clones. They +are stored in order to avoid double compilation. The jobs stored in here are uninterned symbols that carry all important -information in their property list. See the documentation in the +information in their property list. See the documentation in the source file \"coq-par-compile.el\". The hash always maps .vo file names to compilation jobs, regardless of ``-quick''.") @@ -399,7 +399,7 @@ latter greater then everything else." (cons nil nil)) (defun coq-par-enqueue (queue x) - "Insert x in queue QUEUE." + "Insert X in queue QUEUE." (push x (car queue))) (defun coq-par-dequeue (queue) @@ -420,7 +420,7 @@ Use `coq-par-job-enqueue' and `coq-par-job-dequeue' to access the queue.") (defun coq-par-job-enqueue (job) - "Insert job in the queue of waiting compilation jobs." + "Insert JOB in the queue of waiting compilation jobs." (coq-par-enqueue coq-par-compilation-queue job) (when coq--debug-auto-compilation (message "%s: enqueue job in waiting queue" (get job 'name)))) @@ -520,7 +520,7 @@ access the queue.") (defun coq-par-find-dependency-circle-for-job (job path) "Find a dependency cycle in the dependency subtree of JOB. -Do a depth-first-search to find the cycle. JOB is the current +Do a depth-first-search to find the cycle. JOB is the current node and PATH the stack of visited nodes." (let (cycle (p path)) ;; path is reversed. A potential cycle goes from the beginning of @@ -766,7 +766,7 @@ Used for unlocking ancestors on compilation errors." (defun coq-par-kill-and-cleanup () "Kill all background compilation, cleanup internal state and unlock ancestors. This is the common core of `coq-par-emergency-cleanup' and -`coq-par-user-interrupt'. Returns t if there actually was a +`coq-par-user-interrupt'. Returns t if there actually was a background job that was killed." (let (proc-killed) (when coq--debug-auto-compilation @@ -787,10 +787,10 @@ background job that was killed." (defun coq-par-emergency-cleanup () "Emergency cleanup for errors in parallel background compilation. This is the function that cleans everything up when some -background compilation process detected a severe error. When -`coq-compile-keep-going' is nil, all errors are severe. When +background compilation process detected a severe error. When +`coq-compile-keep-going' is nil, all errors are severe. When `coq-compile-keep-going' is t, coqc and some coqdep errors are -not severe. This function is also used for the user action to +not severe. This function is also used for the user action to kill all background compilation. On top of `coq-par-kill-and-cleanup', this function resets the @@ -809,16 +809,16 @@ interrupt to the proof shell." "React to a generic user interrupt with cleaning up everything. This function cleans up background compilation when the proof assistant died (`proof-shell-handle-error-or-interrupt-hook') or -when the user interrupted Proof General (with C-c C-c or +when the user interrupted Proof General (with \\[proof-interrupt-process] or `proof-interrupt-process' leading to `proof-shell-signal-interrupt-hook'). On top of `coq-par-kill-and-cleanup', this function only sets the dynamic variable `prover-was-busy' to tell the proof shell that -the user actually had a reason to interrupt. However, in the +the user actually had a reason to interrupt. However, in the special case where `proof-action-list' is nil and `coq--last-compilation-job' not, this function also clears the -queue region and releases the proof shell lock. This has the nice +queue region and releases the proof shell lock. This has the nice side effect, that `proof-interrupt-process' does not send an interrupt signal to the prover." (let (proc-killed @@ -838,7 +838,7 @@ interrupt signal to the prover." (setq prover-was-busy t)))) (defun coq-par-process-filter (process output) - "Store output from coq background compilation." + "Store OUTPUT from coq background compilation." (process-put process 'coq-process-output (concat (process-get process 'coq-process-output) output))) @@ -846,7 +846,7 @@ interrupt signal to the prover." "Start asynchronous compilation job for COMMAND. This function starts COMMAND with arguments ARGUMENTS for compilation job JOB, making sure that CONTINUATION runs when the -process finishes successfully. FILE-RM, if not nil, denotes a +process finishes successfully. FILE-RM, if non-nil, denotes a file to be deleted when the process is killed." (let ((process-connection-type nil) ; use pipes (process-name (format "pro-%s" coq--par-next-id)) @@ -881,9 +881,9 @@ file to be deleted when the process is killed." (defun coq-par-process-sentinel (process event) "Sentinel for all background processes. -Runs when process PROCESS terminated because of EVENT. It +Runs when process PROCESS terminated because of EVENT. It determines the exit status and calls the continuation function -that has been registered with that process. Normal compilation +that has been registered with that process. Normal compilation errors are reported with an error message." (condition-case err (if (process-get process 'coq-par-process-killed) @@ -933,7 +933,7 @@ errors are reported with an error message." (if cycle (signal 'coq-compile-error-circular-dep (mapconcat 'identity cycle " -> ")) - (error "deadlock in parallel compilation")))))) + (error "Deadlock in parallel compilation")))))) (coq-compile-error-command-start (coq-par-emergency-cleanup) (message "%s \"%s\" in \"%s\"" @@ -943,7 +943,7 @@ errors are reported with an error message." (coq-par-emergency-cleanup) (message "%s %s" (get (car err) 'error-message) (cdr err))) (error - (message "error in sentinel of process %s, error %s" + (message "Error in sentinel of process %s, error %s" (process-name process) err) (coq-par-emergency-cleanup) (signal (car err) (cdr err))))) @@ -964,7 +964,7 @@ errors are reported with an error message." (coq-par-start-jobs-until-full)) (defun coq-par-require-processed (race-counter) - "Callback for `proof-action-list' to signal completion of the last require. + "Callback for `proof-action-list' to signal completion of the last Require. This function ensures that vio2vo compilation starts after `coq-compile-vio2vo-delay' seconds after the last module has been loaded into Coq. When background compilation is successful, this @@ -992,16 +992,16 @@ somewhere after the last require command." ;;; background job tasks (defun coq-par-job-coqc-finished (job) - "t if JOB has state 'waiting-queue or 'ready." + "Return t if JOB has state 'waiting-queue or 'ready." (or (eq (get job 'state) 'waiting-queue) (eq (get job 'state) 'ready))) (defun coq-par-job-is-ready (job) - "t if compilation job JOB is ready." + "Return t if compilation job JOB is ready." (eq (get job 'state) 'ready)) (defun coq-par-dependencies-ready (job) - "t if all dependencies of compilation job JOB are ready." + "Return t if all dependencies of compilation job JOB are ready." (eq (get job 'coqc-dependency-count) 0)) (defun coq-par-add-coqc-dependency (dependee dependant) @@ -1025,20 +1025,20 @@ somewhere after the last require command." (get dependee 'name) (get dependant 'name)))) (defun coq-par-job-needs-compilation (job) - "Determine whether job needs to get compiled and do some side effects. + "Determine whether JOB needs to get compiled and do some side effects. This function contains most of the logic nesseary to support -quick compilation according to `coq-compile-quick'. Taking +quick compilation according to `coq-compile-quick'. Taking `coq-compile-quick' into account, it determines if a compilation -is necessary. The property 'required-obj-file is set either to +is necessary. The property 'required-obj-file is set either to the file that we need to produce or to the up-to-date object -file. If compilation is needed, property 'use-quick is set when --quick will be used. If no compilation is needed, property +file. If compilation is needed, property 'use-quick is set when +-quick will be used. If no compilation is needed, property 'obj-mod-time remembers the time stamp of 'required-obj-file. Indepent of whether compilation is required, .vo or .vio files -that are in the way are deleted. Note that the coq documentation +that are in the way are deleted. Note that the coq documentation does not contain a statement, about what file is loaded, if both -a .vo and a .vio file are present. To be on the safe side, I -therefore delete a file if it might be in the way. Sets the +a .vo and a .vio file are present. To be on the safe side, I +therefore delete a file if it might be in the way. Sets the 'vio2vo property on job if necessary." (let* ((vo-file (get job 'vo-file)) (vio-file (coq-library-vio-of-vo-file vo-file)) @@ -1330,12 +1330,12 @@ case, the following actions are taken: (defun coq-par-compile-job-maybe (job) "Choose next action for JOB after dependencies are ready. -First JOB is put into state 'enqueued-coqc. Then it is determined +First JOB is put into state 'enqueued-coqc. Then it is determined if JOB needs compilation, what file must be produced (depending on `coq-compile-quick') and if a .vio or .vo file must be -deleted. If necessary, deletion happens immediately. If JOB needs +deleted. If necessary, deletion happens immediately. If JOB needs compilation, compilation is started or the JOB is enqueued and -JOB stays in 'enqueued-coqc for the time being. Otherwise, the +JOB stays in 'enqueued-coqc for the time being. Otherwise, the transition 'enqueued-coqc -> 'waiting-queue is done and, if possible, also 'waiting-queue -> 'ready." (put job 'state 'enqueued-coqc) @@ -1357,11 +1357,11 @@ possible, also 'waiting-queue -> 'ready." "Clear Coq dependency and update dependee information in DEPENDANT. This function handles a Coq dependency from child dependee to parent dependant when the dependee has finished compilation (ie. -is in state 'waiting-queue). DEPENDANT must be in state -'waiting-dep. The time of the most recent ancestor is updated, if -necessary using DEPENDEE-TIME. DEPENDEE-TIME must be an Emacs -time or 'just-compiled. The ancestors of dependee are propagated -to DEPENDANT. The dependency count of DEPENDANT is decreased and, +is in state 'waiting-queue). DEPENDANT must be in state +'waiting-dep. The time of the most recent ancestor is updated, if +necessary using DEPENDEE-TIME. DEPENDEE-TIME must be an Emacs +time or 'just-compiled. The ancestors of dependee are propagated +to DEPENDANT. The dependency count of DEPENDANT is decreased and, if it reaches 0, the next transition is triggered for DEPENDANT. For 'file jobs this is 'waiting-dep -> 'enqueued-coqc and for 'clone jobs this 'waiting-dep -> 'waiting-queue." @@ -1393,14 +1393,14 @@ For 'file jobs this is 'waiting-dep -> 'enqueued-coqc and for "Handle transition to state 'waiting-queue for JOB. For 'file jobs, this function is called when compilation finished or was not necessary to make the transition 'enqueued-coqc -> -'waiting-queue. For 'clone jobs, this function is called when its +'waiting-queue. For 'clone jobs, this function is called when its real 'file job has completed compilation and is in state 'waiting-queue to make the transition 'waiting-dep -> waiting-queue for JOB. DEP-TIME is either 'just-compiled, when JOB has just finished compilation, or the most recent modification time of all -dependencies of JOB. (If compilation for JOB failed, DEP-TIME is +dependencies of JOB. (If compilation for JOB failed, DEP-TIME is meaningless but should nevertheless be a non-nil valid argument.) This function makes the following actions. @@ -1533,7 +1533,7 @@ coqdep or coqc are started for it." (defun coq-par-start-or-enqueue (new-job) "Start NEW-JOB or put it into the queue of waiting jobs. NEW-JOB goes already into the waiting queue, if the number of -background jobs is one below the limit. This is in order to leave +background jobs is one below the limit. This is in order to leave room for Proof General." (if (< (1+ coq--current-background-jobs) coq--internal-max-jobs) (coq-par-start-task new-job) @@ -1543,15 +1543,15 @@ room for Proof General." require-span dependant) "Create a new compilation job for MODULE-OBJ-FILE. If there is already a job for MODULE-OBJ-FILE a new clone job is -created. This function initializes all necessary properties of +created. This function initializes all necessary properties of the new job. COQ-LOAD-PATH must be the load path from the source file that -originally initiated the compilation. QUEUE-DEP must be a -compilation job or nil. If non-nil, this function makes a queue -dependency from QUEUE-DEP to the new compilation job. If nil, a +originally initiated the compilation. QUEUE-DEP must be a +compilation job or nil. If non-nil, this function makes a queue +dependency from QUEUE-DEP to the new compilation job. If nil, a newly created clone job will proceed to state ready if the -original job is ready. Argument REQUIRE-SPAN should be present +original job is ready. Argument REQUIRE-SPAN should be present when the new job should update the ancestor list in some span. Argument DEPENDANT tells who required MODULE-OBJ-FILE, this is used only for the error message, in case MODULE-OBJ-FILE refers @@ -1563,7 +1563,7 @@ If the new job is a clone job, its state is a queue dependency QUEUE-DEP (which cannot be ready yet) - 'ready otherwise -If the new job is a 'file job its state is 'enqueued-coqdep. If +If the new job is a 'file job its state is 'enqueued-coqdep. If there is space, coqdep is started immediately, otherwise the new job is put into the compilation queue. @@ -1666,7 +1666,7 @@ not yet failed." For a failing job JOB, an ancestor need to stay looked if there is still some compilation going on for which this ancestor is a dependee or if a top level job with JOB as ancestor has finished -it's compilation successfully. In all other cases the ancestor +it's compilation successfully. In all other cases the ancestor must be unlocked." (dolist (anc-job (get job 'ancestors)) (when (and (eq (get anc-job 'lock-state) 'locked) @@ -1701,8 +1701,8 @@ appropriate." (defun coq-par-mark-job-failing (job) "Mark all dependants of JOB as failing and unlock ancestors as appropriate. Set the 'failed property on all direct and indirect dependants of -JOB. Along the way, unlock ancestors as determined by -`coq-par-ongoing-compilation'. Mark queue dependants with +JOB. Along the way, unlock ancestors as determined by +`coq-par-ongoing-compilation'. Mark queue dependants with 'queue-failed." (unless (get job 'failed) (put job 'failed t) @@ -1716,14 +1716,14 @@ JOB. Along the way, unlock ancestors as determined by (defun coq-par-process-coqdep-result (process exit-status) "Coqdep continuation function: Process coqdep output. -This function analyses the coqdep output of PROCESS. In case of +This function analyses the coqdep output of PROCESS. In case of error, the job is marked as failed or compilation is aborted via -a signal (depending on `coq-compile-keep-going'). If there was no +a signal (depending on `coq-compile-keep-going'). If there was no coqdep error, the following actions are taken. - the job that started PROCESS is put into sate 'waiting-dep -- a new job is created for every dependency. If this new job is +- a new job is created for every dependency. If this new job is not immediately ready, a Coq dependency is registered from the - new job to the current job. For dependencies that are 'ready + new job to the current job. For dependencies that are 'ready already, the most recent ancestor modification time is propagated. - if there are no dependencies (especially if coqdep failed) or @@ -1778,7 +1778,7 @@ is directly passed to `coq-par-analyse-coq-dep-exit'." (defun coq-par-coqc-continuation (process exit-status) "Coqc continuation function. If coqc failed, signal an error or mark the job as 'failed, and -unlock ancestors as appropriate. If coqc was successful, trigger +unlock ancestors as appropriate. If coqc was successful, trigger the transition 'enqueued-coqc -> 'waiting-queue for the job behind PROCESS." (let ((job (process-get process 'coq-compilation-job))) @@ -1803,7 +1803,7 @@ behind PROCESS." (get (process-get process 'coq-compilation-job) 'src-file)))))) (defun coq-par-vio2vo-continuation (process exit-status) - "vio2vo continuation function." + "Vio2vo continuation function." (let ((job (process-get process 'coq-compilation-job))) (if (eq exit-status 0) ;; success - nothing to do @@ -1827,7 +1827,7 @@ behind PROCESS." (defun coq-par-handle-module (module-id span &optional from) "Handle compilation of module MODULE-ID. -This function translates MODULE-ID to a file name. If compilation +This function translates MODULE-ID to a file name. If compilation for this file is not ignored, a new top-level compilation job is created. If there is a new top-level compilation job, it is saved in `coq--last-compilation-job'. @@ -1917,7 +1917,7 @@ there is no last compilation job." (defun coq-par-item-require-predicate (item) - "Return t if ITEM contains a require command. + "Return t if ITEM contains a Require command. Predicate for `split-list-at-predicate', used to split the new queue items at each Require command." (let ((string (mapconcat 'identity (nth 1 item) " "))) @@ -1937,21 +1937,21 @@ ansynchronously in parallel in the background. If there is a last compilation job (`coq--last-compilation-job') then the queue region is extended, while some background -compilation is still running. In this case I have to preserve the -internal state. Otherwise the hash of the compilation jobs and +compilation is still running. In this case I have to preserve the +internal state. Otherwise the hash of the compilation jobs and the ancestor hash are initialized. As next action the new queue items are splitted at each Require -command. The items before the first Require are appended to the -last compilation job or put back into proof-action-list. The +command. The items before the first Require are appended to the +last compilation job or put back into ‘proof-action-list’. The remaining batches of items that each start with a Require are then processed by `coq-par-handle-require-list', which creates -top-level compilation jobs as necessary. Before processing the +top-level compilation jobs as necessary. Before processing the first of these batches, buffers are saved with `coq-compile-save-some-buffers'. Finally, `proof-second-action-list-active' is set if I keep some -queue items because they have to wait for a compilation job. Then +queue items because they have to wait for a compilation job. Then the maximal number of background compilation jobs is started." (when coq--debug-auto-compilation (message "%d items were added to the queue, scan for require" @@ -2004,7 +2004,7 @@ the maximal number of background compilation jobs is started." "Coq function for `proof-shell-extend-queue-hook' doing parallel compilation. If `coq-compile-before-require' is non-nil, this function starts the compilation (if necessary) of the dependencies -ansynchronously in parallel in the background. This function only +ansynchronously in parallel in the background. This function only does the error checking/reporting for `coq-par-preprocess-require-commands-internal', which does all the work." (when coq-compile-before-require @@ -2025,7 +2025,7 @@ does the error checking/reporting for (coq-par-emergency-cleanup) (message "Error: %s" (mapconcat 'identity (cdr err) ": "))) (error - (message "unexpected error during parallel compilation: %s" + (message "Unexpected error during parallel compilation: %s" err) (coq-par-emergency-cleanup) (signal (car err) (cdr err)))))) diff --git a/coq/coq-par-test.el b/coq/coq-par-test.el index 8e83d1d4..ebc5ecd7 100644 --- a/coq/coq-par-test.el +++ b/coq/coq-par-test.el @@ -22,7 +22,7 @@ ;; of `coq-par-job-needs-compilation'. ;; ;; Run the tests with -;; emacs -batch -L . -L ../generic -L ../lib -load coq-par-test.el +;; Emacs -batch -L . -L ../generic -L ../lib -load coq-par-test.el ;; ;;; TODO: ;; @@ -48,7 +48,7 @@ (quick nil nil vio) (ensure-vo nil nil vo )) - ((src vo dep vio) + ((src vo dep vio) (no-quick nil vo vio) (quick nil vo vio) (ensure-vo t nil vo )) @@ -705,15 +705,15 @@ ) "Test and result specification for `coq-par-job-needs-compilation'. -List of tests. A test is a list of 4 elements. The first element, -a list, specifies the existing files and their relative age. In +List of tests. A test is a list of 4 elements. The first element, +a list, specifies the existing files and their relative age. In there, `src' stands for the source (x.v) file, `dep' for a (already compiled) dependency (dep.vo or dep.vio), `vo' for the -.vo file (x.vo) and `vio' for the .vio file (x.vio). A label in +.vo file (x.vo) and `vio' for the .vio file (x.vio). A label in the list denotes an existing file, a missing label a missing -file. The first element is the oldest file, the last element the -newest file. A sublist specifies a set of files with identical -time stamps. For example, ``(src (vo vio) dep)'' specifies source +file. The first element is the oldest file, the last element the +newest file. A sublist specifies a set of files with identical +time stamps. For example, ``(src (vo vio) dep)'' specifies source is older than .vo and .vio, .vo and .vio have identical last modification time stamps and .vo and .vio are older than the dependency. @@ -722,17 +722,17 @@ Elements 2-4 of a test specify the results and side effects of `coq-par-job-needs-compilation' for all setting of `coq-compile-quick' on the file configuration described in element 1. The options `quick-no-vio2vo' and `quick-and-vio2vo' -are specified together with label `quick'. Each result and side +are specified together with label `quick'. Each result and side effect specification (also called a variant in the source code -below) is itself a list of 4 elements. Element 1 is the value for +below) is itself a list of 4 elements. Element 1 is the value for `coq-compile-quick', where `quick' denotes both `quick-no-vio2vo' -and `quick-and-vio2vo'. Element 2 specifies the result of +and `quick-and-vio2vo'. Element 2 specifies the result of `coq-par-job-needs-compilation', nil for don't compile, t for do -compile. Elements 3-5 specify side effects. Element 3 which file -must be deleted, where nil means no file must be deleted. Element +compile. Elements 3-5 specify side effects. Element 3 which file +must be deleted, where nil means no file must be deleted. Element 4 specifies which file name must be stored in the -`required-obj-file' property of the job. This file will be used -as the compiled module library. In case compilation is +`required-obj-file' property of the job. This file will be used +as the compiled module library. In case compilation is needed (element 2 equals t), this is the target of the compilation. @@ -740,7 +740,7 @@ This list contains 1 test for all possible file configuration and relative ages.") (defun coq-par-test-flatten-files (file-descr) - "Flatten a file description test case list into a list of files." + "Flatten a file description test case list FILE-DESCR into a list of files." (let (result) (dolist (f file-descr result) (if (listp f) diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el index 90bd3c3d..5875908c 100644 --- a/coq/coq-seq-compile.el +++ b/coq/coq-seq-compile.el @@ -16,8 +16,8 @@ ;;; Commentary: ;; -;; This file implements compilation of required modules. The -;; compilation is done synchonously and sequentially. That is, Proof +;; This file implements compilation of required modules. The +;; compilation is done synchonously and sequentially. That is, Proof ;; General blocks before putting newly asserted items into ;; proof-action-list and compiles one module after the other. ;; @@ -43,9 +43,9 @@ (defun coq-seq-lock-ancestor (span ancestor-src) "Lock ancestor ANCESTOR-SRC and register it in SPAN. -Lock only if `coq-lock-ancestor' is non-nil. Further, do nothing, +Lock only if `coq-lock-ancestor' is non-nil. Further, do nothing, if ANCESTOR-SRC is already a member of -`proof-included-files-list'. Otherwise ANCESTOR-SRC is locked and +`proof-included-files-list'. Otherwise ANCESTOR-SRC is locked and registered in the 'coq-locked-ancestors property of the SPAN to properly unlock ANCESTOR-SRC on retract." (if coq-lock-ancestors @@ -63,18 +63,18 @@ properly unlock ANCESTOR-SRC on retract." "Compute dependencies of LIB-SRC-FILE. Invoke \"coqdep\" on LIB-SRC-FILE and parse the output to compute the compiled coq library object files on which -LIB-SRC-FILE depends. The return value is either a string or a -list. If it is a string then an error occurred and the string is -the core of the error message. If the return value is a list no +LIB-SRC-FILE depends. The return value is either a string or a +list. If it is a string then an error occurred and the string is +the core of the error message. If the return value is a list no error occurred and the returned list is the (possibly empty) list of file names LIB-SRC-FILE depends on. If an error occurs this funtion displays `coq--compile-response-buffer' with the complete command and its -output. The optional argument COMMAND-INTRO is only used in the -error case. It is prepended to the displayed command. +output. The optional argument COMMAND-INTRO is only used in the +error case. It is prepended to the displayed command. -LIB-SRC-FILE should be an absolute file name. If it is, the +LIB-SRC-FILE should be an absolute file name. If it is, the dependencies are absolute too and the simplified treatment of `coq-load-path-include-current' in `coq-include-options' won't break." @@ -152,7 +152,7 @@ if one of the following conditions is true: - OBJ is older than the the youngest object file of the dependencies. Argument MAX-DEP-OBJ-TIME provides the information about the -dependencies. It is either +dependencies. It is either - 'just-compiled if one of the dependencies of SRC has just been compiled - the time value (see`time-less-or-equal') of the youngest (most @@ -160,11 +160,11 @@ dependencies. It is either - nil if there are no dependencies, or if they are all ignored If this function decides to compile SRC to OBJ it returns -'just-compiled. Otherwise it returns the modification time of +'just-compiled. Otherwise it returns the modification time of OBJ. Note that file modification times inside Emacs have only a -precisision of 1 second. To avoid spurious recompilations we do +precisision of 1 second. To avoid spurious recompilations we do not recompile if the youngest object file of the dependencies and OBJ have identical modification times." (let (src-time obj-time) @@ -191,9 +191,9 @@ OBJ have identical modification times." (defun coq-seq-make-lib-up-to-date (coq-obj-hash span lib-obj-file) "Make library object file LIB-OBJ-FILE up-to-date. Check if LIB-OBJ-FILE and all it dependencies are up-to-date -compiled coq library objects. Recompile the necessary objects, if -not. This function returns 'just-compiled if it compiled -LIB-OBJ-FILE. Otherwise it returns the modification time of +compiled coq library objects. Recompile the necessary objects, if +not. This function returns 'just-compiled if it compiled +LIB-OBJ-FILE. Otherwise it returns the modification time of LIB-OBJ-FILE as time value (see `time-less-or-equal'). Either LIB-OBJ-FILE or its source file (or both) must exist when @@ -256,7 +256,7 @@ If `coq-confirm-external-compilation' is t then the user must confirm the external command in the minibuffer, otherwise the command is executed without confirmation. -Argument SPAN is the span of the \"Require\" command. The +Argument SPAN is the span of the \"Require\" command. The ancestor ABSOLUTE-MODULE-OBJ-FILE is locked and registered in the span for for proper unlocking on retract. @@ -292,11 +292,11 @@ therefore the customizations for `compile' do not apply." (defun coq-seq-map-module-id-to-obj-file (module-id span &optional from) "Map MODULE-ID to the appropriate coq object file. -The mapping depends of course on `coq-load-path'. The current +The mapping depends of course on `coq-load-path'. The current implementation invokes coqdep with a one-line require command. This is probably slower but much simpler than modelling coq file -loading inside ProofGeneral. Argument SPAN is only used for error -handling. It provides the location information of MODULE-ID for a +loading inside ProofGeneral. Argument SPAN is only used for error +handling. It provides the location information of MODULE-ID for a decent error message. A peculiar consequence of the current implementation is that this @@ -347,19 +347,18 @@ function returns () if MODULE-ID comes from the standard library." "Locate MODULE-ID and compile if necessary. If `coq-compile-command' is not nil the whole task of checking which modules need compilation and the compilation itself is done by an external -process. If `coq-compile-command' is nil ProofGeneral computes the -dependencies with \"coqdep\" and compiles modules as necessary. This internal -checking does currently not handle ML modules. +process. If `coq-compile-command' is nil ProofGeneral computes the +dependencies with \"coqdep\" and compiles modules as necessary. +This internal checking does currently not handle ML modules. -Argument SPAN is the span of the \"Require\" command. Locked +Argument SPAN is the span of the \"Require\" command. Locked ancestors are registered in its 'coq-locked-ancestors property for proper unlocking on retract. Argument COQ-OBJECT-LOCAL-HASH-SYMBOL provides a place to store the coq-obj-hash, which is used during internal -compilation (see `coq-seq-make-lib-up-to-date'). This way one hash -will be used for all \"Require\" commands added at once to the -queue." +compilation (see `coq-seq-make-lib-up-to-date'). This way one hash +will be used for all \"Require\" commands added at once to the queue." (let ((module-obj-file (coq-seq-map-module-id-to-obj-file module-id span from))) ;; coq-seq-map-module-id-to-obj-file currently returns () for ;; standard library modules! diff --git a/coq/coq-smie.el b/coq/coq-smie.el index 59d84e36..15697354 100644 --- a/coq/coq-smie.el +++ b/coq/coq-smie.el @@ -20,7 +20,7 @@ ;; Lexer. ;; Due to the verycomplex grammar of Coq, and to the architecture of -;; smie, we deambiguate all kinds of tokens during lexing. This is a +;; smie, we deambiguate all kinds of tokens during lexing. This is a ;; complex piece of code but it allows for all smie goodies. ;; Some examples of deambigations: ;; - We distinguish ":=" from ":= inductive" to avoid the circular precedence @@ -52,11 +52,11 @@ (defcustom coq-smie-user-tokens nil "Alist of (syntax . token) pairs to extend the coq smie parser. -These are user configurable additional syntax for smie tokens. It -allows to define alternative syntax for smie token. Typical +These are user configurable additional syntax for smie tokens. It +allows to define alternative syntax for smie token. Typical example: if you define a infix operator \"xor\" you may want to define it as a new syntax for token \"or\" in order to have the -indentation rules of or applied to xor. Other exemple: if you +indentation rules of or applied to xor. Other exemple: if you want to define a new notation \"ifb\" ... \"then\" \"else\" then you need to declare \"ifb\" as a new syntax for \"if\" to make indentation work well." @@ -113,7 +113,7 @@ attention to case differences." (defun coq-smie-is-ltacdef () (let ((case-fold-search nil)) - (save-excursion + (save-excursion (coq-find-real-start) (looking-at "\\(\\(Local\\|Global\\)\\s-+\\)?\\(Ltac\\|Tactic\\s-+Notation\\)\\s-")))) @@ -237,11 +237,11 @@ the token of \".\" is simply \".\"." ;; tokens and ignore-bteween are not disjoint (defun coq-smie-search-token-forward (tokens &optional end ignore-between) "Search for one of TOKENS between point and END. -If some enclosing parenthesis is reached, stop there and return -nil. Token \".\" is considered only if followed by a space. -optional IGNORE-BETWEEN defines opener/closer to ignore during -search. Careful: the search for a opener stays inside the current -command (and inside parenthesis)." +If some enclosing parenthesis is reached, stop there and return nil. +Token \".\" is considered only if followed by a space. Optional +IGNORE-BETWEEN defines opener/closer to ignore during search. +Careful: the search for a opener stays inside the current command (and +inside parenthesis)." (unless end (setq end (point-max))) (condition-case nil (catch 'found @@ -282,11 +282,12 @@ command (and inside parenthesis)." ;; tokens and ignore-bteween are not disjoint (defun coq-smie-search-token-backward (tokens &optional end ignore-between) "Search for one of TOKENS between point and END. -If some enclosing parenthesis is reached, stop there and return -nil. Token \".\" is considered only if followed by a space. +If some enclosing parenthesis is reached, stop there and return nil. +Token \".\" is considered only if followed by a space. optional IGNORE-BETWEEN defines opener/closer to ignore during -search. Careful: the search for a opener stays inside the current -command (and inside parenthesis). " +search. +Careful: the search for a opener stays inside the current command (and +inside parenthesis)." (unless end (setq end (point-min))) (condition-case nil (catch 'found @@ -343,9 +344,9 @@ proof-mode starter in Coq." ;; each goal anyway. (defun coq-smie-detect-goal-command () "Return t if the next command is a goal starting to be indented. -The point should be at the beginning of the command name. As -false positive are more annoying than false negative, return t -only if it is FOR SURE a goal opener. Put a \"Proof.\" when you want to +The point should be at the beginning of the command name. +As false positive are more annoying than false negative, return t only +if it is FOR SURE a goal opener. Put a \"Proof.\" when you want to force indentation." (save-excursion ; FIXME add other commands that potentialy open goals (when (proof-looking-at "\\(Local\\|Global\\)?\ @@ -362,7 +363,7 @@ force indentation." The point should be at the beginning of the command name." (save-excursion ; FIXME Is there other module starting commands? (cond - ((looking-back "with\\s-+" nil) "module") ; lowecase means Module that is not a declaration keyword (like in with Module) + ((looking-back "with\\s-+" nil) "module") ; lowecase means Module that is not a declaration keyword (like in with Module) ((proof-looking-at "\\(Module\\|Section\\)\\>") (if (coq-lonely-:=-in-this-command) "Module start" "Module def"))))) @@ -557,7 +558,7 @@ The point should be at the beginning of the command name." (equal (coq-smie-backward-token) "; tactic")) ;; recursive "|| tactic") ;; this is wrong half of the time but should not harm indentation - ((and (equal backtok nil) (looking-back "(" nil)) "||") + ((and (equal backtok nil) (looking-back "(" nil)) "||") ((equal backtok nil) (if (or (looking-back "\\[" nil) (and (looking-back "{" nil) @@ -769,8 +770,7 @@ Lemma foo: forall n, instead of: Lemma foo: forall n, - n = n. -" + n = n." :type 'boolean :group 'coq) @@ -784,19 +784,18 @@ Lemma foo: forall n, :safe #'coq-indent-safep) (defcustom coq-indent-semicolon-tactical 2 - "Number of spaces used to indent after the first tactical semi colon of a serie. - If set to 0, indetation is as follows: - tac1; - tac2; - tac3; - tac4. - - if set to 2 (default): - - tac1; - tac2; - tac3; - tac4." + "Number of spaces used to indent after the 1st tactical semicolon of a serie. +If set to 0, indentation is as follows: +tac1; +tac2; +tac3; +tac4. + +If set to 2 (default): +tac1; + tac2; + tac3; + tac4." :type 'integer :group 'coq :safe #'coq-indent-safep) @@ -820,8 +819,7 @@ for example, if set to 0 the indentation is as follows: If it is set to 2 (default) it is as follows: Lemma foo: forall x:nat, - x <= 0 -> x = 0. -" + x <= 0 -> x = 0." :type 'integer :group 'coq :safe #'coq-indent-safep) @@ -1006,7 +1004,7 @@ Typical values are 2 or 4." ;; copied from elixir-smie.el (defun coq-smie--same-line-as-parent (parent-pos child-pos) - "Return non-nil if `child-pos' is on same line as `parent-pos'." + "Return non-nil if PARENT-POS is on same line as CHILD-POS." (= (line-number-at-pos parent-pos) (line-number-at-pos child-pos))) (defun coq-smie-rules (kind token) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index c55c93fc..bb32fc52 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -27,9 +27,9 @@ ;;; keyword databases (defcustom coq-user-tactics-db nil - "User defined tactic information. See `coq-syntax-db' for -syntax. It is not necessary to add your own tactics here (it is not -needed by the synchronizing/backtracking system). You may however do + "User defined tactic information. See `coq-syntax-db' for syntax. +It is not necessary to add your own tactics here (it is not +needed by the synchronizing/backtracking system). You may however do so for the following reasons: 1 your tactics will be colorized by font-lock @@ -44,10 +44,10 @@ so for the following reasons: (defcustom coq-user-commands-db nil - "User defined command information. See `coq-syntax-db' for - syntax. It is not necessary to add your own commands here (it is not - needed by the synchronizing/backtracking system). You may however do - so for the following reasons: + "User defined command information. See `coq-syntax-db' for syntax. +It is not necessary to add your own commands here (it is not +needed by the synchronizing/backtracking system). You may however do +so for the following reasons: 1 your commands will be colorized by font-lock @@ -60,10 +60,10 @@ so for the following reasons: :group 'coq) (defcustom coq-user-tacticals-db nil - "User defined tactical information. See `coq-syntax-db' for - syntax. It is not necessary to add your own commands here (it is not - needed by the synchronizing/backtracking system). You may however do - so for the following reasons: + "User defined tactical information. See `coq-syntax-db' for syntax. +It is not necessary to add your own commands here (it is not +needed by the synchronizing/backtracking system). You may however do +so for the following reasons: 1 your commands will be colorized by font-lock @@ -76,10 +76,10 @@ so for the following reasons: :group 'coq) (defcustom coq-user-solve-tactics-db nil - "User defined closing tactics. See `coq-syntax-db' for - syntax. It is not necessary to add your own commands here (it is not - needed by the synchronizing/backtracking system). You may however do - so for the following reasons: + "User defined closing tactics. See `coq-syntax-db' for syntax. +It is not necessary to add your own commands here (it is not +needed by the synchronizing/backtracking system). You may however do +so for the following reasons: 1 your commands will be colorized by font-lock @@ -93,10 +93,10 @@ so for the following reasons: (defcustom coq-user-cheat-tactics-db nil "User defined closing tactics BY CHEATING (ex: admit). - See `coq-syntax-db' for syntax. It is not necessary to add your - own commands here (it is not needed by the - synchronizing/backtracking system). You may however do so for - the following reasons: +See `coq-syntax-db' for syntax. It is not necessary to add your +own commands here (it is not needed by the +synchronizing/backtracking system). You may however do so for +the following reasons: 1 your commands will be colorized by font-lock @@ -111,10 +111,10 @@ so for the following reasons: (defcustom coq-user-reserved-db nil - "User defined reserved keywords information. See `coq-syntax-db' for - syntax. It is not necessary to add your own commands here (it is not - needed by the synchronizing/backtracking system). You may however do - so for the following reasons: + "User defined reserved keywords information. See `coq-syntax-db' for syntax. +It is not necessary to add your own commands here (it is not +needed by the synchronizing/backtracking system). You may however do +so for the following reasons: 1 your commands will be colorized by font-lock @@ -328,7 +328,7 @@ so for the following reasons: ("suff" "suff" "suff # : #" t "suff") ) coq-user-tactics-db) - "Coq tactics information list. See `coq-syntax-db' for syntax. " + "Coq tactics information list. See `coq-syntax-db' for syntax." ) ;; user shortcuts are prioritized by being put at the end @@ -445,7 +445,7 @@ so for the following reasons: ("Local Coercion" nil "Local Coercion @{id} : @{typ1} >-> @{typ2}." t "Local\\s-+Coercion") ("Coercion" "coerc" "Coercion @{id} : @{typ1} >-> @{typ2}." t "Coercion") ) - "Coq declaration keywords information list. See `coq-syntax-db' for syntax." + "Coq declaration keywords information list. See `coq-syntax-db' for syntax." ) (defvar coq-defn-db @@ -505,7 +505,7 @@ so for the following reasons: ("Structure" "str" "Structure # : # := {\n# : #;\n# : # }" t "Structure") ("Variant" "varv" "Variant # : # := # : #." t "Variant") ) - "Coq definition keywords information list. See `coq-syntax-db' for syntax. " + "Coq definition keywords information list. See `coq-syntax-db' for syntax." ) ;; modules and section are indented like goal starters @@ -543,7 +543,7 @@ so for the following reasons: ("Obligations" "obls" "Obligations #.\n#\nQed." nil "Obligations") ("Next Obligation" "nobl" "Next Obligation.\n#\nQed." t "Next Obligation") ) - "Coq goal starters keywords information list. See `coq-syntax-db' for syntax. " + "Coq goal starters keywords information list. See `coq-syntax-db' for syntax." ) ;; TODO: dig other queries from the refman. @@ -572,7 +572,7 @@ so for the following reasons: ("Test" nil "Test" nil "Test" nil t) ; let us not highlight all possible options for Test ("Timeout" nil "Timeout" nil "Timeout") ) - "Coq queries command, that deserve a separate menu for sending them to coq without insertion. " + "Coq queries command, that deserve a separate menu for sending them to coq without insertion." ) ;; command that are not declarations, definition or goal starters @@ -920,7 +920,7 @@ so for the following reasons: (append coq-decl-db coq-defn-db coq-goal-starters-db coq-queries-commands-db coq-other-commands-db coq-ssreflect-commands-db coq-user-commands-db) - "Coq all commands keywords information list. See `coq-syntax-db' for syntax. " + "Coq all commands keywords information list. See `coq-syntax-db' for syntax." ) @@ -943,7 +943,7 @@ so for the following reasons: ("match with 4" "m4" "match # with\n| # => #\n| # => #\n| # => #\n| # => #\nend") ("match with 5" "m5" "match # with\n| # => #\n| # => #\n| # => #\n| # => #\n| # => #\nend") ) - "Coq terms keywords information list. See `coq-syntax-db' for syntax. " + "Coq terms keywords information list. See `coq-syntax-db' for syntax." ) @@ -987,8 +987,8 @@ so for the following reasons: ;; (la fonction vernac_declare_module dans toplevel/vernacentries) (defun coq-count-match (regexp strg) - "Count the number of (maximum, non overlapping) matching substring - of STRG matching REGEXP. Empty match are counted once." + "Count the number of max. non-overlapping substring of STRG matching REGEXP. +Empty matches are counted once." (let ((nbmatch 0) (str strg)) (while (and (proof-string-match regexp str) (not (string-equal str ""))) (incf nbmatch) @@ -1017,8 +1017,8 @@ Used by `coq-goal-command-p'" ;; unused anymore (for good) (defun coq-goal-command-str-p (str) - "Decide syntactically whether STR is a goal start or not. Use -`coq-goal-command-p' on a span instead if possible." + "Decide syntactically whether STR is a goal start or not. +Use ‘coq-goal-command-p’ on a span instead if possible." (let* ((match (coq-count-match "\\_<match\\_>" str)) (with (- (coq-count-match "\\_<with\\_>" str) (coq-count-match "\\_<with\\s-+signature\\_>" str))) (letwith (+ (coq-count-match "\\_<let\\_>" str) (- with match))) @@ -1043,7 +1043,6 @@ Used by `coq-goal-command-p'" ;; to look at Modules and section (actually indentation will still ;; need it) (defun coq-goal-command-p (span) - "see `coq-goal-command-p'" (or (span-property span 'goalcmd) ;; module and section starts are detected here (let ((str (or (span-property span 'cmd) ""))) @@ -1065,7 +1064,7 @@ It is used: (defun coq-save-command-p (span str) - "Decide whether argument is a Save command or not" + "Decide whether argument is a Save command or not." (or (proof-string-match coq-save-command-regexp-strict str) (and (proof-string-match "\\`Proof\\_>" str) (not (proof-string-match "\\`Proof\\s-*\\(\\.\\|\\_<with\\_>\\|\\_<using\\_>\\)" str))))) @@ -1238,12 +1237,12 @@ It is used: (concat paren "\\s-*\\(" coq-ids "\\)\\s-*" end)) (defcustom coq-variable-highlight-enable t - "Activates partial bound variable highlighting" + "Activates partial bound variable highlighting." :type 'boolean :group 'coq) (defcustom coq-symbol-highlight-enable nil - "Activates partial bound variable highlighting" + "Activates symbol highlighting." :type 'boolean :group 'coq) @@ -1367,7 +1366,7 @@ It is used: ;; necessary anymore. (defvar coq-hyp-name-in-goal-or-response-regexp "\\(?:\\(?1:^\\)\\|\\(?1:^ \\)\\|\\(?:[^ ] \\)\\(?1: \\)\\)\\(?2:\\(?:[^\n :(),=]\\|, \\)+\\)\\(?: *:=?[ \n]\\|,$\\)" - "regexp matching hypothesis names in goal or response buffer. + "Regexp matching hypothesis names in goal or response buffer. Subexpr 2 contains the real name of the function. Subexpr 1 contains the prefix context (spaces mainly) that is not part of another hypothesis.") @@ -1384,9 +1383,8 @@ part of another hypothesis.") (match-beginning 2)))) (defun coq-detect-hyps-positions (buf &optional limit) - "Detect all hypothesis displayed in buffer BUF and returns positions. -5 positions are created for each hyp: (begcross beghypname -endhypname beg end)." + "Detect all hypotheses displayed in buffer BUF and returns positions. +5 positions are created for each hyp: (begcross beghypname endhypname beg end)." (with-current-buffer buf (save-excursion (goto-char (point-min)) @@ -1407,7 +1405,7 @@ endhypname beg end)." (point)))) ; if several hyp names, we name the overlays with the first hyp name (setq res - (cons + (cons (cons (mapcar (lambda (s) (substring-no-properties s)) splitstr) (list begcross beghypname endhypname beg end)) res)))) diff --git a/coq/coq-system.el b/coq/coq-system.el index 93c9dd7e..63ee57ac 100644 --- a/coq/coq-system.el +++ b/coq/coq-system.el @@ -17,7 +17,7 @@ ;;; Commentary: ;; ;; This file holds constants, options and some general functions for -;; setting coq command arguments. Some code is dedicated as a light +;; setting coq command arguments. Some code is dedicated as a light ;; support for older versions of coq. ;; @@ -51,12 +51,12 @@ On Windows you might need something like: (defcustom coq-prog-name (if (executable-find "coqtop") "coqtop" (proof-locate-executable "coqtop" t '("C:/Program Files/Coq/bin"))) - "*Name of program to run as Coq. See `proof-prog-name', set from this. + "*Name of program to run as Coq. See `proof-prog-name', set from this. On Windows with latest Coq package you might need something like: C:/Program Files/Coq/bin/coqtop.opt.exe instead of just \"coqtop\". -This must be a single program name with no arguments; see `coq-prog-args' -to manually adjust the arguments to the Coq process. +This must be a single program name with no arguments. See option +`coq-prog-args' to manually adjust the arguments to the Coq process. See also `coq-prog-env' to adjust the environment." :type 'string :group 'coq) @@ -94,8 +94,8 @@ See also `coq-prog-env' to adjust the environment." (defcustom coq-pinned-version nil "Which version of Coq you are using. There should be no need to set this value unless you use the trunk from -the Coq github repository. For Coq versions with decent version numbers -Proof General detects the version automatically and adjusts itself. This +the Coq github repository. For Coq versions with decent version numbers +Proof General detects the version automatically and adjusts itself. This variable should contain nil or a version string." :type 'string :group 'coq) @@ -245,12 +245,12 @@ Set to t if you want this feature, but note that it is deprecated." (defcustom coq-load-path nil "Non-standard coq library load path. This list specifies the LoadPath extension for coqdep, coqc and -coqtop. Usually, the elements of this list are strings (for +coqtop. Usually, the elements of this list are strings (for \"-I\") or lists of two strings (for \"-R\" dir path and \"-Q\" dir path). The possible forms of elements of this list correspond to the 4 -forms of include options (`-I' `-Q' and `-R'). An element can be +forms of include options (`-I' `-Q' and `-R'). An element can be - A list of the form `(\\='ocamlimport dir)', specifying (in 8.5) a directory to be added to ocaml path (`-I'). @@ -303,10 +303,10 @@ not the same (-I is for coq path)." (make-variable-buffer-local 'coq-load-path) (defcustom coq-load-path-include-current t - "If `t' let coqdep search the current directory too. -Should be `t' for normal users. If `t' pass -Q dir \"\" to coqdep when -processing files in directory \"dir\" in addition to any entries -in `coq-load-path'. + "If t, let coqdep search the current directory too. +Should be t for normal users. If t, pass -Q dir \"\" to coqdep when +processing files in directory \"dir\" in addition to any entries in +`coq-load-path'. This setting is only relevant with Coq < 8.5." :type 'boolean @@ -417,7 +417,7 @@ LOADPATH, CURRENT-DIRECTORY, PRE-V85: see `coq-include-options'." ;; coqtop always adds the current directory to the LoadPath, so don't ;; include it in the -Q options. This is not true for coqdep. "Build a list of options for coqc. -LOAD-PATH, CURRENT-DIRECTORY, PRE-V85: see `coq-coqc-prog-args'." +LOADPATH, CURRENT-DIRECTORY, PRE-V85: see `coq-coqc-prog-args'." (cons "-emacs" (coq-coqc-prog-args loadpath current-directory pre-v85))) (defun coq-prog-args () @@ -440,17 +440,16 @@ path (including the -R lib options) (see `coq-load-path')." (defcustom coq-project-filename "_CoqProject" "The name of coq project file. -The coq project file of a coq developpement (Cf Coq documentation -on \"makefile generation\") should contain the arguments given to +The coq project file of a coq developpement (cf. Coq documentation on +\"makefile generation\") should contain the arguments given to coq_makefile. In particular it contains the -I and -R -options (preferably one per line). If `coq-use-coqproject' is -t (default) the content of this file will be used by proofgeneral -to infer the `coq-load-path' and the `coq-prog-args' variables -that set the coqtop invocation by proofgeneral. This is now the -recommended way of configuring the coqtop invocation. Local file -variables may still be used to override the coq project file's -configuration. .dir-locals.el files also work and override -project file settings." +options (preferably one per line). If `coq-use-coqproject' is +t (default) the content of this file will be used by proofgeneral to +infer the `coq-load-path' and the `coq-prog-args' variables that set +the coqtop invocation by proofgeneral. This is now the recommended +way of configuring the coqtop invocation. Local file variables may +still be used to override the coq project file's configuration. +.dir-locals.el files also work and override project file settings." :type 'string :safe 'stringp :group 'coq) @@ -569,12 +568,10 @@ variable." (defun coq-load-project-file () "Set `coq-prog-args' and `coq-load-path' according to _CoqProject file. -Obeys `coq-use-project-file'. Note that if a variable is already -set by dir/file local variables, this function will not override -its value. -See `coq-project-filename' to change the name of the -project file, and `coq-use-project-file' to disable this -feature." +Obeys `coq-use-project-file'. Note that if a variable is already set +by dir/file local variables, this function will not override its value. +See `coq-project-filename' to change the name of the project file, and +`coq-use-project-file' to disable this feature." (when coq-use-project-file ;; Let us reread dir/file local vars, in case the user mmodified them (let* ((oldargs (assoc 'coq-prog-args file-local-variables-alist)) @@ -641,11 +638,11 @@ Does nothing if `coq-use-project-file' is nil." ;; OBSOLETE, should take _CoqProject into account. (defun coq-guess-command-line (filename) "Guess the right command line options to compile FILENAME using `make -n'. -This function is obsolete, the recommended way of setting the -coqtop options is to use a _Coqproject file as described in coq -documentation. ProofGeneral reads this file and sets compilation -options according to its contents. See `coq-project-filename'. Per file configuration may -then be set using local file variables." +This function is obsolete, the recommended way of setting the coqtop +options is to use a _Coqproject file as described in coq +documentation. ProofGeneral reads this file and sets compilation +options according to its contents. See `coq-project-filename'. Per +file configuration may then be set using local file variables." (if (local-variable-p 'coq-prog-name (current-buffer)) coq-prog-name (let* ((dir (or (file-name-directory filename) ".")) diff --git a/coq/coq-unicode-tokens.el b/coq/coq-unicode-tokens.el index 5f2cd0c6..349038c1 100644 --- a/coq/coq-unicode-tokens.el +++ b/coq/coq-unicode-tokens.el @@ -20,7 +20,7 @@ ;; variable for documentation. ;; ;; For Coq, there is no dedicated token syntax, it's probably -;; preferable to use UTF-8 notation directly (see utf8.v). +;; preferable to use UTF-8 notation directly (see utf8.v). ;; ;; On the other hand, for easily portable files, one can fix ;; ordinary character sequences as tokens, like the old X-Symbol @@ -31,7 +31,7 @@ ;; Unicode characters, whereas ordinary character sequences are ;; displayed as those characters. ;; -;; Recommended ways to work: +;; Recommended ways to work: ;; ;; 1) UTF-8 buffers: ☑ Show Symbol Tokens (ON) ;; ☑ Enable Shortcuts (ON) @@ -45,6 +45,8 @@ (require 'proof-unicode-tokens) +;;; Code: + (defconst coq-token-format "") ; Let generic code do the job (defconst coq-token-match nil) (defconst coq-hexcode-match nil) @@ -103,7 +105,7 @@ ("false" "false" bold sans) ("true" "true" bold sans) - ;; example tokens used in Benjamin C. Pierce et al's + ;; example tokens used in Benjamin C. Pierce et al's ;; Software Foundations course ("WHILE" "WHILE" bold sans) ("DO" "DO" bold sans) @@ -123,7 +125,7 @@ (">=" "≥") ("=>" "⇒") ("->" "→") ; or ⟶ or ⟹ if you prefer - ("<-" "←") ; or ⟵ or ⟸ + ("<-" "←") ; or ⟵ or ⟸ ("<->" "↔") ; or ⟷ ... ("++" "⧺") ("<<" "《") @@ -151,8 +153,8 @@ ("~" "¬") ;; A dirty hack for the goals window, shouldn't be input syntax! - ("============================" - "⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯" + ("============================" + "⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯" bold tactical) ) ;; an alist of token name, unicode char sequence @@ -106,8 +106,8 @@ These are appended at the end of `coq-shell-init-cmd'." :group 'coq) (defcustom coq-prefer-top-of-conclusion nil - "Prefer start of the conclusion over its end when displaying goals -that do not fit in the goals window." + "Prefer start of the conclusion over its end when displaying large goals. +Namely, goals that do not fit in the goals window." :type 'boolean :group 'coq) @@ -156,7 +156,7 @@ that do not fit in the goals window." (defcustom coq-end-goals-regexp-show-subgoals "\n(dependent evars:" "Regexp for `proof-shell-end-goals-regexp' when showing all subgoals. -A setting of nil means show all output from Coq. See also +A setting of nil means show all output from Coq. See also option `coq-hide-additional-subgoals'." :type '(choice regexp (const nil)) :group 'coq) @@ -164,7 +164,7 @@ A setting of nil means show all output from Coq. See also (defcustom coq-end-goals-regexp-hide-subgoals (concat "\\(\nsubgoal 2 \\)\\|\\(" coq-end-goals-regexp-show-subgoals "\\)") "Regexp for `proof-shell-end-goals-regexp' when hiding additional subgoals. -See also `coq-hide-additional-subgoals'." +See also option `coq-hide-additional-subgoals'." :type '(choice regexp (const nil)) :group 'coq) @@ -337,7 +337,7 @@ See also `coq-hide-additional-subgoals'." ;; Indentation and navigation support via SMIE. (defcustom coq-use-smie t - "OBSOLETE. smie code is always used now. + "OBSOLETE. smie code is always used now. If non-nil, Coq mode will try to use SMIE for indentation. SMIE is a navigation and indentation framework available in Emacs >= 23.3." @@ -376,8 +376,8 @@ SMIE is a navigation and indentation framework available in Emacs >= 23.3." ;; would not be shown in response buffer. If it is before, then we want it ;; urgent so that it is displayed. (defvar coq-eager-no-urgent-regex "\\s-*Finished " - "Regexp of commands matching proof-shell-eager-annotation-start - that should maybe not be classified as urgent messages.") + "Regexp of commands matching ‘proof-shell-eager-annotation-start’ +that should maybe not be classified as urgent messages.") ;; return the end position if found, nil otherwise (defun coq-non-urgent-eager-annotation () @@ -775,7 +775,7 @@ If locked span already has a state number, then do nothing. Also updates (defun coq-hide-additional-subgoals-switch () - "Function invoked when the user switches `coq-hide-additional-subgoals'." + "Function invoked when the user switches option `coq-hide-additional-subgoals'." (if coq-time-commands (progn (setq coq-hide-additional-subgoals nil) @@ -786,8 +786,8 @@ If locked span already has a state number, then do nothing. Also updates (setq proof-shell-end-goals-regexp coq-end-goals-regexp-show-subgoals)))) (defun coq-time-commands-switch () - "Function invoked when the user switches `coq-time-commands'. -Resets `coq-hide-additional-subgoals' and puts nil into + "Function invoked when the user switches option `coq-time-commands'. +Reset option `coq-hide-additional-subgoals' and puts nil into `proof-shell-end-goals-regexp' to ensure the timing is visible in the *goals* buffer." (if coq-time-commands @@ -806,7 +806,7 @@ the *goals* buffer." "Enumerates the different kinds of notation information one can ask to coq.") (defun coq-PrintScope () - "Show information on notations. Coq specific." + "Show information on notations. Coq specific." (interactive) (let* ((mods @@ -898,7 +898,7 @@ Support dot.notation.of.modules." "Whether Coq mode should remap mouse button 1 to Coq queries. This overrides the default global binding of (control mouse-1) and -(shift mouse-1) (buffers and faces menus). Hence it is nil by +\(shift mouse-1) (buffers and faces menus). Hence it is nil by default." :type 'boolean :group 'coq) @@ -963,9 +963,9 @@ Otherwise propose identifier at point if any." (string-match "is on\\>" resp))) (defun coq-command-with-set-unset (setcmd cmd unsetcmd &optional postformatcmd testcmd) - "Play commands SETCMD then CMD and then silently UNSETCMD. The -last UNSETCMD is performed with tag 'empty-action-list so that it -does not trigger 'proof-shell-empty-action (which dos \"Shwo\" at + "Play commands SETCMD then CMD and then silently UNSETCMD. +The last UNSETCMD is performed with tag 'empty-action-list so that it +does not trigger ‘proof-shell-empty-action’ (which does \"Show\" at the time of writing this documentation)." (let* ((postform (if (eq postformatcmd nil) 'identity postformatcmd)) (flag-is-on (and testcmd (coq-flag-is-on-p testcmd)))) @@ -984,8 +984,8 @@ the time of writing this documentation)." (defun coq-ask-do-set-unset (ask do setcmd unsetcmd &optional dontguess postformatcmd tescmd) "Ask for an ident id and execute command DO in SETCMD mode. -More precisely it executes SETCMD, then DO id and finally -silently UNSETCMD. See `coq-command-with-set-unset'." +More precisely it executes SETCMD, then DO id and finally silently +UNSETCMD. See `coq-command-with-set-unset'." (let* ((cmd) (postform (if (eq postformatcmd nil) 'identity postformatcmd tescmd))) (proof-shell-ready-prover) (setq cmd (coq-guess-or-ask-for-string ask dontguess)) @@ -1159,8 +1159,8 @@ With flag Printing All if some prefix arg is given (C-u)." (defun coq-get-response-string-at (&optional pt) "Go forward from PT until reaching a 'response property, and return it. Response span only starts at first non space character of a -command, so we may have to go forward to find it. Starts -from (point) if pt is nil. Precondition: pt (or point if nil) +command, so we may have to go forward to find it. Starts +from (point) if pt is nil. Precondition: pt (or point if nil) must be in locked region." (let ((pt (or pt (point)))) (save-excursion @@ -1171,10 +1171,10 @@ must be in locked region." (span-property (span-at (point) 'response) 'response)))) (defun coq-Show (withprintingall) - "Ask for a number i and show the ith goal. -Ask for a number i and show the ith current goal. With non-nil -prefix argument and not on the locked span, show the goal with -flag Printing All set." + "Ask for a number I and show the Ith goal. +Ask for a number I and show the ith current goal. With non-nil prefix +argument and not on the locked span, show the goal with flag +Printing All set." ; Disabled: ; "Ask for a number i and show the ith goal, or show ancient goal. ;If point is on a locked span, show the corresponding coq @@ -1222,7 +1222,7 @@ flag Printing All set." ;; FIXME: hopefully this will eventually become a non synchronized option and ;; we can remove this. (defun coq-set-auto-adapt-printing-width (&optional symb val); args are for :set compatibility - "Function called when setting `auto-adapt-printing-width'" + "Function called when setting `auto-adapt-printing-width'." (setq symb val) ;; FIXME this is wrong (it should be 'set', but it would set nil sometimes) (if coq-auto-adapt-printing-width (progn @@ -1239,10 +1239,10 @@ flag Printing All set." ;; command and *not* have the goal redisplayed, the command must be tagged with ;; 'empty-action-list. (defun coq-empty-action-list-command (cmd) - "Return the list of commands to send to coq after CMD if it is -the last command of the action list. + "Return the list of commands to send to Coq after CMD +if it is the last command of the action list. If CMD is tagged with 'empty-action-list then this function won't -be called and no command will be sent to coq. " +be called and no command will be sent to Coq." (cond ((or ;; If closing a nested proof, Show the enclosing goal. @@ -1344,9 +1344,9 @@ present, current pg display mode and current geometry otherwise." ))) (defun coq-adapt-printing-width (&optional show width) - "Sends a Set Printing Width command to coq to fit the response window's width. -A Show command is also issued if SHOW is non-nil, so that the -goal is redisplayed." + "Sends a Set Printing Width command to Coq to fit the response window's WIDTH. +A Show command is also issued if SHOW is non-nil, so that the goal is +redisplayed." (interactive) (let ((wdth (or width (coq-guess-goal-buffer-at-next-command)))) ;; if no available width, or unchanged, do nothing @@ -1381,8 +1381,8 @@ goal is redisplayed." ;;;;;;;;;; Hypothesis tracking ;;;;;;;;;; ;;; Facilities to build overlays for hyp names and hyp+type + hypcross ;;; ((un)folding buttons). -(defvar coq-hypname-map (make-sparse-keymap) "Keymap for visible hypothesis") -(defvar coq-hypcross-map (make-sparse-keymap) "Keymap for visible hypothesis") +(defvar coq-hypname-map (make-sparse-keymap) "Keymap for visible hypothesis.") +(defvar coq-hypcross-map (make-sparse-keymap) "Keymap for visible hypothesis.") (defvar coq-hypcross-hovering-help t "Whether hyps fold cross pops up a help when hovered.") @@ -1503,11 +1503,10 @@ Maintained by a hook in `proof-shell-handle-delayed-output-hook'.") (defun coq-detect-hyps-in-goals () - "Detect all hypothesis displayed in goals buffer and create overlays. -Three overlays are created for each hyp: (hypov hypnameov hypcrossov), respectively -for the whole hyp, only its name and the overlay for fold/unfold cross. -Returnns the list of mappings hypname -> overlays. -" + "Detect all hypotheses displayed in goals buffer and create overlays. +Three overlays are created for each hyp: (hypov hypnameov hypcrossov), +respectively for the whole hyp, only its name and the overlay for +fold/unfold cross. Return the list of mappings hypname -> overlays." (let* ((fsthyp-pos (coq-find-first-hyp)) (fsthyp-ov (when fsthyp-pos (with-current-buffer proof-goals-buffer @@ -1649,7 +1648,7 @@ See `coq-highlight-hyp'." (insert hyp-name))) ;;;;;;;;;;; Hiding Hypothesis ;;;;;;;;;;; -(defvar coq-hidden-hyp-map (make-sparse-keymap) "Keymap for hidden hypothesis") +(defvar coq-hidden-hyp-map (make-sparse-keymap) "Keymap for hidden hypothesis.") (defvar coq-hidden-hyps nil "List of hypothesis that should be hidden in goals buffer. @@ -1715,12 +1714,11 @@ hiding to be maintain when scripting/undoing." (defun coq-fold-hyp (h) "Fold hypothesis H's type from the context durably. -(displays \".......\" instead). This function relies on variable -coq-hyps-positions. The hiding maintained as the goals buffer is -changed, thanks to a hook on -`proof-shell-handle-delayed-output-hook', consider using -`coq-fold-hyp' if you want the hiding to be maintain when -scripting/undoing." +\(displays \".......\" instead). This function relies on variable +‘coq-hyps-positions’. The hiding maintained as the goals buffer is +changed, thanks to a hook on `proof-shell-handle-delayed-output-hook', +consider using `coq-fold-hyp' if you want the hiding to be maintain +when scripting/undoing." (interactive) (unless (member h coq-hidden-hyps) (setq coq-hidden-hyps (cons h coq-hidden-hyps)) @@ -1858,15 +1856,17 @@ See `coq-fold-hyp'." (defun coq-get-comment-region (pt) - "Return a list of the forme (beg end) where beg,end is the comment region arount position PT. -Return nil if PT is not inside a comment" + "Return a list of the form (BEG END). +BEG,END being the comment region arount position PT. +Return nil if PT is not inside a comment." (save-excursion (goto-char pt) `(,(save-excursion (coq-find-comment-start)) ,(save-excursion (coq-find-comment-end))))) (defun coq-near-comment-region () - "Return a list of the forme (beg end) where beg,end is the comment region near position PT. + "Return a list of the forme (BEG END). +BEG,END being is the comment region near position PT. Return nil if PT is not near a comment. Near here means PT is either inside or just aside of a comment." (save-excursion @@ -2263,7 +2263,7 @@ Near here means PT is either inside or just aside of a comment." (defun coq-extract-instantiated-existentials (start end) "Coq specific function for `proof-tree-extract-instantiated-existentials'. -Returns the list of currently instantiated existential variables." +Return the list of currently instantiated existential variables." (proof-tree-extract-list start end coq-proof-tree-existentials-state-start-regexp @@ -2276,11 +2276,11 @@ Returns the list of currently instantiated existential variables." (defun coq-proof-tree-get-new-subgoals () "Check for new subgoals and issue appropriate Show commands. -This is a hook function for `proof-tree-urgent-action-hook'. This +This is a hook function for `proof-tree-urgent-action-hook'. This function examines the current goal output and searches for new -unknown subgoals. Those subgoals have been generated by the last +unknown subgoals. Those subgoals have been generated by the last proof command and we must send their complete sequent text -eventually to prooftree. Because subgoals may change with +eventually to prooftree. Because subgoals may change with the next proof command, we must execute the additionally needed Show commands before the next real proof command. @@ -2288,18 +2288,18 @@ The ID's of the open goals are checked with `proof-tree-sequent-hash' in order to find out if they are new. For any new goal an appropriate Show Goal command with a 'proof-tree-show-subgoal flag is inserted into -`proof-action-list'. Then, in the normal delayed output +`proof-action-list'. Then, in the normal delayed output processing, the sequent text is send to prooftree as a sequent update (see `proof-tree-update-sequent') and the ID of the sequent is registered as known in `proof-tree-sequent-hash'. Searching for new subgoals must only be done when the proof is not finished, because Coq 8.5 lists open existential variables -as (new) open subgoals. For this test we assume that +as (new) open subgoals. For this test we assume that `proof-marker' has not yet been moved. The `proof-tree-urgent-action-hook' is also called for undo -commands. For those, nothing is done. +commands. For those, nothing is done. The not yet delayed output is in the region \[proof-shell-delayed-output-start, proof-shell-delayed-output-end]." @@ -2383,9 +2383,9 @@ This is the Coq incarnation of `proof-tree-find-undo-position'." (defun coq-proof-tree-enable-evar-callback (span) "Callback for the evar printing status test. -This is the callback for the command ``Test Printing Dependent -Evars Line''. It checks whether evar printing was off and -remembers that fact in `coq--proof-tree-must-disable-evars'." +This is the callback for the command ``Test Printing Dependent Evars Line''. +It checks whether evar printing was off and remembers that +fact in `coq--proof-tree-must-disable-evars'." (with-current-buffer proof-shell-buffer (save-excursion ;; When the callback runs, the next item is sent to Coq already and @@ -2426,11 +2426,11 @@ properly after the proof and enable the evar printing." (defun coq-proof-tree-disable-evars () "Disable evar printing if necessary. This function switches off evar printing after the proof, if it -was off before the proof. For undo commands, we rely on the fact +was off before the proof. For undo commands, we rely on the fact that Coq itself undos the effect of the evar printing change that -we inserted after the goal statement. We also rely on the fact +we inserted after the goal statement. We also rely on the fact that Proof General never backtracks into the middle of a -proof. (If this would happen, Coq would switch evar printing on +proof. (If this would happen, Coq would switch evar printing on and the code here would not switch it off after the proof.) Being called from `proof-tree-urgent-action-hook', this function @@ -2444,10 +2444,10 @@ result of `coq-proof-tree-get-proof-info'." (defun coq-proof-tree-evar-display-toggle () "Urgent action hook function for changing the evar printing status in Coq. This function is for `proof-tree-urgent-action-hook' (which is -called only if external proof disaply is switched on). It checks +called only if external proof disaply is switched on). It checks whether a proof was started or stopped and inserts commands for enableing and disabling the evar status line for Coq 8.6 or -later. Without the evar status line being enabled, prooftree +later. Without the evar status line being enabled, prooftree crashes. Must only be called via `proof-tree-urgent-action-hook' to ensure @@ -2651,7 +2651,7 @@ tacitcs like destruct and induction reuse hypothesis names by default, which makes the detection of new hypothesis incorrect. the hack consists in adding the \"!\" modifier on the argument destructed, so that it is left in the goal and the name cannot be -reused. We also had a \"clear\" at the end of the tactic so that +reused. We also had a \"clear\" at the end of the tactic so that the whole tactic behaves correctly. Warning: this makes the error messages (and location) wrong.") @@ -2980,8 +2980,9 @@ buffer." (defun coq-highlight-error (&optional parseresp clean) - "Parses the last coq output looking at an error message. Highlight the text -pointed by it. Coq error message must be like this: + "Parse the last Coq output looking at an error message. +Highlight the text pointed by it. +Coq error message must be like this: \" > command with an error here ... @@ -3195,24 +3196,24 @@ Only when three-buffer-mode is enabled." (defcustom coq-double-hit-enable nil "* Experimental: Whether or not double hit should be enabled in coq mode. -A double hit is performed by pressing twice a key quickly. If +A double hit is performed by pressing twice a key quickly. If this variable is not nil, then 1) it means that electric terminator is off and 2) a double hit on the terminator act as -the usual electric terminator. See `proof-electric-terminator'. -" +the usual electric terminator. See `proof-electric-terminator'." :type 'boolean :set 'proof-set-value :group 'proof-user-options) (defvar coq-double-hit-hot-key "." - "The key used for double hit electric terminator. By default this -is the coq terminator \".\" key. For example one can do this: + "The key used for double hit electric terminator. +By default this is the coq terminator \".\" key. +For example one can do this: -(setq coq-double-hit-hot-key (kbd \";\")) +\(setq coq-double-hit-hot-key (kbd \";\")) -to use semi-colon instead (on french keyboard, it is the same key -as \".\" but without shift.") +to use semi-colon instead (on French keyboard, it is the same key as +\".\" but without shift.") (defvar coq-double-hit-hot-keybinding nil "The keybinding that was erased by double hit terminator enabling. @@ -3253,7 +3254,7 @@ This is an advice to pg `proof-electric-terminator-enable' function." "The maximum delay between the two hit of a double hit in coq/proofgeneral.") (defvar coq-double-hit-timer nil - "the timer used to watch for double hits.") + "The timer used to watch for double hits.") (defvar coq-double-hit-hot nil "The variable telling that a double hit is still possible.") @@ -3261,8 +3262,8 @@ This is an advice to pg `proof-electric-terminator-enable' function." (defun coq-unset-double-hit-hot () - "Disable timer `coq-double-hit-timer' and set it to nil. Shut -off the current double hit if any. This function is supposed to + "Disable timer `coq-double-hit-timer' and set it to nil. +Shut off the current double hit if any. This function is supposed to be called at double hit timeout." (when coq-double-hit-timer (cancel-timer coq-double-hit-timer)) (setq coq-double-hit-hot nil) @@ -3285,9 +3286,11 @@ Starts a timer for a double hit otherwise." nil 'coq-unset-double-hit-hot)))) (defun coq-terminator-insert (&optional count) - "A wrapper on `proof-electric-terminator' to accept double hits instead if enabled. -If by accident `proof-electric-terminator-enable' and `coq-double-hit-enable' -are non-nil at the same time, this gives priority to the former." + "A wrapper on `proof-electric-terminator'. +Used to accept double hits instead if enabled. +If by accident option `proof-electric-terminator-enable' and option +`coq-double-hit-enable' are non-nil at the same time, this gives +priority to the former." (interactive) (if (and (not proof-electric-terminator-enable) coq-double-hit-enable (null count)) diff --git a/doc/docstring-magic.el b/doc/docstring-magic.el index 614b56e2..409fd22a 100644 --- a/doc/docstring-magic.el +++ b/doc/docstring-magic.el @@ -36,15 +36,15 @@ (let ((assistants (mapcar (function car) proof-assistant-table))) ; assume not customized (while assistants - (let* + (let* ((assistant (car assistants)) ; compiler bogus warning here - (nameregexp - (or - (cdr-safe + (nameregexp + (or + (cdr-safe (assoc assistant proof-assistant-table)) - (error "proof-site: symbol " (symbol-name assistant) - "is not in proof-assistant-table"))) + (error "Symbol %s is not in proof-assistant-table (in docstring-magic)" + (symbol-name assistant)))) (assistant-name (car nameregexp)) (sname (symbol-name assistant)) (elisp-file sname)) @@ -85,3 +85,6 @@ (setq func-menu 'markup-hack) (load "texi-docstring-magic.el") + +(provide 'docstring-magic) +;;; docstring-magic.el ends here diff --git a/easycrypt/easycrypt-abbrev.el b/easycrypt/easycrypt-abbrev.el index 3850ffb7..fa9cdcfc 100644 --- a/easycrypt/easycrypt-abbrev.el +++ b/easycrypt/easycrypt-abbrev.el @@ -1,3 +1,5 @@ +;;; easycrypt-abbrev.el --- Abbrev table and menus for EasyCrypt mode + ;; -------------------------------------------------------------------- ;; Copyright (c) - 2012--2016 - IMDEA Software Institute ;; Copyright (c) - 2012--2016 - Inria @@ -5,9 +7,14 @@ ;; Distributed under the terms of the GPL-v3 license ;; -------------------------------------------------------------------- +;;; Commentary: +;; + (require 'proof) (require 'easycrypt-syntax) +;;; Code: + (defpgdefault menu-entries '( ["Use Three Panes" proof-three-window-toggle @@ -23,3 +30,5 @@ )) (provide 'easycrypt-abbrev) + +;;; easycrypt-abbrev.el ends here diff --git a/easycrypt/easycrypt-hooks.el b/easycrypt/easycrypt-hooks.el index 3cf891e3..67592973 100644 --- a/easycrypt/easycrypt-hooks.el +++ b/easycrypt/easycrypt-hooks.el @@ -1,3 +1,5 @@ +;;; easycrypt-hooks.el --- Auxiliary functions for EasyCrypt mode + ;; -------------------------------------------------------------------- ;; Copyright (c) - 2012--2016 - IMDEA Software Institute ;; Copyright (c) - 2012--2016 - Inria @@ -5,9 +7,14 @@ ;; Distributed under the terms of the GPL-v3 license ;; -------------------------------------------------------------------- +;;; Commentary: +;; + (require 'span) (require 'proof) +;;; Code: + (defvar easycrypt-last-but-one-statenum 0) (defvar easycrypt-proof-weak-mode nil) @@ -38,7 +45,7 @@ (defun easycrypt-last-prompt-info (s) "Extract the information from prompt." - (let ((lastprompt (or s (error "no prompt")))) + (let ((lastprompt (or s (error "No prompt")))) (when (string-match "\\[\\([0-9]+\\)|\\(\\sw+\\)\\]" lastprompt) (list (string-to-number (match-string 1 lastprompt)) (if (equal (match-string 2 lastprompt) "weakcheck") t nil))))) @@ -68,3 +75,5 @@ (list (format "undo %s." (int-to-string span-staten))))) (provide 'easycrypt-hooks) + +;;; easycrypt-hooks.el ends here diff --git a/easycrypt/easycrypt-keywords.el b/easycrypt/easycrypt-keywords.el index e0b9d369..feb64fb1 100644 --- a/easycrypt/easycrypt-keywords.el +++ b/easycrypt/easycrypt-keywords.el @@ -1,3 +1,5 @@ +;;; easycrypt-keywords.el --- Definition of keywords for EasyCrypt mode + ;; -------------------------------------------------------------------- ;; Copyright (c) - 2012--2016 - IMDEA Software Institute ;; Copyright (c) - 2012--2016 - Inria @@ -5,7 +7,12 @@ ;; Distributed under the terms of the GPL-v3 license ;; -------------------------------------------------------------------- -; Generated on Tue Feb 21 23:37:34 2017 +;;; Commentary: +;; +;; Generated on Tue Feb 21 23:37:34 2017 +;; + +;;; Code: (defvar easycrypt-bytac-keywords '( "exact" @@ -175,3 +182,5 @@ )) (provide 'easycrypt-keywords) + +;;; easycrypt-keywords.el ends here diff --git a/easycrypt/easycrypt-syntax.el b/easycrypt/easycrypt-syntax.el index a784395b..48e64a57 100644 --- a/easycrypt/easycrypt-syntax.el +++ b/easycrypt/easycrypt-syntax.el @@ -1,3 +1,5 @@ +;;; easycrypt-syntax.el --- Syntax definitions for EasyCrypt mode + ;; -------------------------------------------------------------------- ;; Copyright (c) - 2012--2016 - IMDEA Software Institute ;; Copyright (c) - 2012--2016 - Inria @@ -5,10 +7,15 @@ ;; Distributed under the terms of the GPL-v3 license ;; -------------------------------------------------------------------- +;;; Commentary: +;; + (require 'proof-syntax) (require 'easycrypt-keywords) (require 'easycrypt-hooks) +;;; Code: + (defconst easycrypt-id "[A-Za-z_]+") (defconst easycrypt-terminal-string ".") @@ -20,7 +27,7 @@ (defconst easycrypt-non-undoables-regexp "^pragma\\b") (defconst easycrypt-keywords-code-open '("{")) -(defconst easycrypt-keywords-code-close '("}")) +(defconst easycrypt-keywords-code-close '("}")) (defconst easycrypt-keywords-code-end '(";")) (defvar easycrypt-other-symbols "\\(\\.\\.\\|\\[\\]\\)") @@ -45,7 +52,7 @@ "\\s-+\\(?:nosmt\\s-+\\)?\\(\\sw+\\)")) (defun easycrypt-save-command-p (span str) - "Decide whether argument is a [save|qed] command or not" + "Decide whether argument is a [save|qed] command or not." (let ((txt (or (span-property span 'cmd) ""))) (proof-string-match-safe easycrypt-proof-save-regexp txt))) @@ -61,7 +68,7 @@ (modify-syntax-entry ?_ "_") ;; For comments - (modify-syntax-entry ?\* ". 23") + (modify-syntax-entry ?\* ". 23") ;; For blocks (modify-syntax-entry ?\( "()1") @@ -84,7 +91,7 @@ ;; FIXME: really needs change in generic function to take account of this, ;; since the end character of a command is not the start (concat "\\(\\s(\\|\\s)\\|\\sw\\|\\s \\|\\s_\\)*=" ;match assignments - "\\|;;\\|;\\|" + "\\|;;\\|;\\|" (proof-ids-to-regexp easycrypt-global-keywords)) "Regexp matching any EasyCrypt command start or the terminator character.") @@ -176,3 +183,5 @@ (modify-syntax-entry ?\) ")(4")) (provide 'easycrypt-syntax) + +;;; easycrypt-syntax.el ends here diff --git a/easycrypt/easycrypt.el b/easycrypt/easycrypt.el index f7f0059f..e9b40358 100644 --- a/easycrypt/easycrypt.el +++ b/easycrypt/easycrypt.el @@ -1,3 +1,5 @@ +;;; easycrypt.el --- Major mode for EasyCrypt + ;; -------------------------------------------------------------------- ;; Copyright (c) - 2012--2016 - IMDEA Software Institute ;; Copyright (c) - 2012--2016 - Inria @@ -5,11 +7,16 @@ ;; Distributed under the terms of the GPL-v3 license ;; -------------------------------------------------------------------- +;;; Commentary: +;; + (require 'proof) (require 'easycrypt-syntax) (require 'easycrypt-hooks) (require 'easycrypt-abbrev) +;;; Code: + (add-to-list 'hs-special-modes-alist '(easycrypt-mode "{" "}" "/[*/]" nil nil)) @@ -27,7 +34,7 @@ (defcustom easycrypt-load-path nil "Non-standard EasyCrypt library load path. -This list specifies the include path for EasyCrypt. The elements of +This list specifies the include path for EasyCrypt. The elements of this list are strings." :type '(repeat (string :tag "simple directory (-I)")) :safe 'easycrypt-load-path-safep @@ -102,7 +109,7 @@ this list are strings." proof-three-window-mode-policy (quote hybrid) proof-auto-multiple-files t) - ; Setting indents + ; Setting indents (set (make-local-variable 'indent-tabs-mode) nil) (setq proof-indent-enclose-offset (- proof-indent) proof-indent-open-offset 0 @@ -158,20 +165,20 @@ this list are strings." (define-derived-mode easycrypt-response-mode proof-response-mode "EasyCrypt response" nil (easycrypt-init-output-syntax-table) - (setq proof-response-font-lock-keywords + (setq proof-response-font-lock-keywords easycrypt-font-lock-keywords) (proof-response-config-done)) (define-derived-mode easycrypt-goals-mode proof-goals-mode "EasyCrypt goals" nil (easycrypt-init-output-syntax-table) - (setq proof-goals-font-lock-keywords + (setq proof-goals-font-lock-keywords easycrypt-font-lock-keywords) (proof-goals-config-done)) -(defun easycrypt-get-last-error-location () - "Remove [error] in the error message and extract the position - and length of the error " +(defun easycrypt-get-last-error-location () + "Remove [error] in the error message and extract the position and +length of the error." (proof-with-current-buffer-if-exists proof-response-buffer (goto-char (point-max)) @@ -188,8 +195,8 @@ this list are strings." (while (proof-looking-at "\\s-") (forward-char 1))) (defun easycrypt-highlight-error () - "Use 'easycrypt-get-last-error-location' to know the position - of the error and then highlight in the script buffer" + "Use ‘easycrypt-get-last-error-location’ to know the position of the +error and then highlight in the script buffer." (proof-with-current-buffer-if-exists proof-script-buffer (let ((mtch (easycrypt-get-last-error-location))) (when mtch @@ -260,4 +267,7 @@ this list are strings." '(lambda () (when proof-three-window-enable (proof-layout-windows)))) ;; -------------------------------------------------------------------- + (provide 'easycrypt) + +;;; easycrypt.el ends here diff --git a/generic/pg-assoc.el b/generic/pg-assoc.el index 714429b7..b06b4ec5 100644 --- a/generic/pg-assoc.el +++ b/generic/pg-assoc.el @@ -48,7 +48,7 @@ Some may be dead/nil." ;;;###autoload (defun proof-associated-windows (&optional all-frames) "Return a list of the associated buffers windows. -Dead or nil buffers are not represented in the list. Optional +Dead or nil buffers are not represented in the list. Optional argument ALL-FRAMES has the same meaning than for `get-buffer-window'." (let ((bufs (proof-associated-buffers)) diff --git a/generic/pg-autotest.el b/generic/pg-autotest.el index bc3ab9c5..e7cb19a9 100644 --- a/generic/pg-autotest.el +++ b/generic/pg-autotest.el @@ -104,7 +104,7 @@ (format-time-string "%D %H:%M"))))) (defun pg-autotest-message (msg &rest args) - "Give message MSG in log file output and on display." + "Give message MSG (formatted using ARGS) in log file output and on display." (let ((fmsg (if args (apply 'format msg args) msg))) (proof-with-current-buffer-if-exists pg-autotest-log @@ -217,7 +217,7 @@ completely processing the buffer as the last step." (proof-shell-wait) (decf jumps)) - ((and (eq random-thing 1) + ((and (eq random-thing 1) (not (proof-locked-region-empty-p))) (pg-autotest-message " random jump: retracting whole buffer") @@ -280,7 +280,7 @@ completely processing the buffer as the last step." (defun pg-autotest-test-quit-prover () "Exit prover process." (if (buffer-live-p proof-shell-buffer) - (let ((kill-buffer-query-functions nil)) + (let ((kill-buffer-query-functions nil)) (kill-buffer proof-shell-buffer)) (error "No proof shell buffer to kill"))) diff --git a/generic/pg-custom.el b/generic/pg-custom.el index 8a7bb793..0c67c7a2 100644 --- a/generic/pg-custom.el +++ b/generic/pg-custom.el @@ -115,7 +115,7 @@ For example for coq on Windows you might need something like: :type '(repeat string) :group 'proof-shell) -(defpgcustom quit-timeout +(defpgcustom quit-timeout (cond ((eq proof-assistant-symbol 'isar) 45) (t 5)) diff --git a/generic/pg-goals.el b/generic/pg-goals.el index c35f0f29..baab5561 100644 --- a/generic/pg-goals.el +++ b/generic/pg-goals.el @@ -89,7 +89,7 @@ function tries to do that by calling `pg-response-maybe-erase'. If KEEPRESPONSE is non-nil, we assume that a response message corresponding to this goals message has already been displayed -before this goals message (see `proof-shell-handle-delayed-output'), +before this goals message (see `proof-shell-handle-delayed-output'), so the response buffer should not be cleared." (save-excursion ;; Response buffer may be out of date. It may contain (error) diff --git a/generic/pg-movie.el b/generic/pg-movie.el index ba641c20..9be95972 100644 --- a/generic/pg-movie.el +++ b/generic/pg-movie.el @@ -52,15 +52,15 @@ (let* ((tokens (proof-ass unicode-tokens-enable)) (cmd (buffer-substring-no-properties (span-start span) (span-end span))) - (tcmd (if tokens + (tcmd (if tokens ;; no subscripts of course (unicode-tokens-encode-str cmd) cmd)) (helpspan (span-property span 'pg-helpspan)) - (resp (when helpspan + (resp (when helpspan (span-property helpspan 'response))) (tresp (if resp - (if tokens + (if tokens (unicode-tokens-encode-str resp) resp) "")) @@ -99,7 +99,7 @@ If FORCE, overwrite existing file without asking." (point-min) (point-max))) (movie-file-name - (concat + (concat (file-name-sans-extension (buffer-file-name)) ".xml"))) @@ -114,7 +114,7 @@ If FORCE, overwrite existing file without asking." ;;;###autoload (defun pg-movie-export-from (script &optional force) "Export the movie file that results from processing SCRIPT." - (interactive "fFile: + (interactive "fFile: P") (let ((proof-full-annotation t) ; dynamic (proof-fast-process-buffer t)) @@ -126,10 +126,10 @@ P") (defun pg-movie-export-directory (dir extn) "Export movie files from directory DIR with extension EXTN. Existing XML files are overwritten." - (interactive "DDirectory: + (interactive "DDirectory: sFile extension: ") - (let ((files (directory-files - dir t + (let ((files (directory-files + dir t (concat "\\." extn "$")))) (dolist (f files) (pg-movie-export-from f 'force)) diff --git a/generic/pg-pamacs.el b/generic/pg-pamacs.el index 9792dfd0..1492e0ca 100644 --- a/generic/pg-pamacs.el +++ b/generic/pg-pamacs.el @@ -39,10 +39,10 @@ (require 'proof-compat) ; pg-custom-undeclare-variable (require 'proof-autoloads) ; proof-debug -(defmacro deflocal (var value &optional docstring) - "Define a buffer local variable VAR with default value VALUE." +(defmacro deflocal (var value &optional doc) + "Define a buffer local variable VAR with default value VALUE and docstring DOC." `(progn - (defvar ,var nil ,docstring) + (defvar ,var nil ,doc) (make-variable-buffer-local (quote ,var)) (setq-default ,var ,value))) @@ -79,13 +79,13 @@ This macro should only be invoked once a specific prover is engaged." (symbol-value pasym))))) (defun proof-defpgcustom-fn (sym args) - "Define a new customization variable <PA>-sym for current proof assistant. + "Define a new customization variable <PA>-SYM for current proof assistant. Helper for macro `defpgcustom'." (let ((specific-var (proof-ass-symv sym)) (generic-var (intern (concat "proof-assistant-" (symbol-name sym)))) - (newargs (if (member :group args) - args - (append (list :group + (newargs (if (member :group args) + args + (append (list :group proof-assistant-internals-cusgrp) args)))) (eval @@ -116,7 +116,7 @@ but which the user may require different values of across provers. The function proof-assistant-<SYM> is also defined, which can be used in the generic portion of Proof General to access the value for the current prover. -Arguments are as for `defcustom', which see. If a :group argument is +Arguments ARGS are as for `defcustom', which see. If a :group argument is not supplied, the setting will be added to the internal settings for the current prover (named <PA>-config)." `(proof-defpgcustom-fn (quote ,sym) (quote ,args))) @@ -183,7 +183,7 @@ Usage: (defpgdefault SYM VALUE)" (setq name (intern (concat (downcase (cadr args)) ":" (symbol-name name)))) (put name 'pggroup (cadr args)) (setq args (cdr args))) - ((eq (car args) :pgdynamic) + ((eq (car args) :pgdynamic) (put name 'pgdynamic (cadr args)) (setq args (cdr args))) ((eq (car args) :type) @@ -202,11 +202,11 @@ Usage: (defpgdefault SYM VALUE)" (eq (eval type) 'integer) (eq (eval type) 'number) (eq (eval type) 'string))) - (error "defpacustom: missing :type keyword or wrong :type value")) + (error "Macro defpacustom: missing :type keyword or wrong :type value")) ;; Error in case a defpacustom is repeated. (when (assq name proof-assistant-settings) - (error "defpacustom: Proof assistant setting %s re-defined!" + (error "Macro defpacustom: Proof assistant setting %s re-defined!" name)) (eval @@ -237,8 +237,8 @@ which can be changed by sending commands. In this case, NAME stands for the internal setting, flag, etc, for the proof assistant, and a :setting and :type value should be provided. The :type of NAME should be one of 'integer, 'float, -'boolean, 'string. Other types are not supported (see -`proof-menu-entry-for-setting'). They will yield an error when +'boolean, 'string. Other types are not supported (see +`proof-menu-entry-for-setting'). They will yield an error when constructing the proof assistant menu. The function `proof-assistant-format' is used to format VAL. @@ -262,7 +262,7 @@ Additional properties in the ARGS prop list may include: pgdynamic flag If flag is non-nil, this setting is a dynamic one that is particular to the running instance of the prover. - Automatically set by preferences configured from PGIP + Automatically set by preferences configured from PGIP askprefs message. This macro also extends the `proof-assistant-settings' list." diff --git a/generic/pg-pbrpm.el b/generic/pg-pbrpm.el index 6436871f..619a5d6c 100644 --- a/generic/pg-pbrpm.el +++ b/generic/pg-pbrpm.el @@ -125,22 +125,22 @@ Matches the region to be returned.") (set-buffer pg-pbrpm-buffer-menu)) (defun pg-pbrpm-analyse-goal-buffer () - "This function analyses the goal buffer and produces a table to find goals and hypothesis. -If stores, in the variable pg-pbrpm-goal-description, a list with shape - - (start-goal end-goal goal-name start-concl hyps ...) with 5 elements for each goal: - - start-goal: the position of the first char of the goal - end-goal: the position of the last char of the goal - goal-name: the goal name (or number) - start-concl: the position of first char of the conclusion of the goal - hyps: the list of hypothesis with the shape: - - (start-hyp start-hyp-text end-hyp hyp-name ...) with 4 elemets per hypothesis: - start-hyp: the position of the first char of the hypothesis (including its name) - start-hyp-text: the position of the first char of the hypothesis formula (no name) - end-hyp: the position of the last char of the hypothesis - hyp-name: then name of the hypothesis." + "Analyse the goal buffer and produce a table to find goals and hypothesis. + +It stores, in the variable ‘pg-pbrpm-goal-description’, a list with shape + +(start-goal end-goal goal-name start-concl hyps ...) with 5 elements per goal: + start-goal: the position of the first char of the goal + end-goal: the position of the last char of the goal + goal-name: the goal name (or number) + start-concl: the position of first char of the conclusion of the goal + hyps: the list of hypothesis with the shape: + +(start-hyp start-hyp-text end-hyp hyp-name ...) with 4 elements per hypothesis: + start-hyp: the position of the first char of the hyp (including its name) + start-hyp-text: the position of the first char of the hyp formula (no name) + end-hyp: the position of the last char of the hypothesis + hyp-name: then name of the hypothesis." (with-current-buffer proof-goals-buffer (save-excursion (goto-char 0) @@ -204,7 +204,9 @@ If stores, in the variable pg-pbrpm-goal-description, a list with shape (pg-pbrpm-eliminate-id (cons (car l) acc) (cdr l))))) (defun pg-pbrpm-build-menu (event start end) -"Build a Proof By Rules pop-up menu according to the state of the proof, the event and a selected region (between the start and end markers). + "Build a Proof By Rules pop-up menu. +Depends on the state of the proof, the event and a selected region +(between the start and end markers). The prover command is processed via pg-pbrpm-run-command." ;; first, run the prover specific (name, rule)'s list generator (let ((click-info (pg-pbrpm-process-click event start end))) ; retrieve click informations @@ -327,8 +329,9 @@ The prover command is processed via pg-pbrpm-run-command." (span-property sp1 'goalnum)))))))) (defun pg-pbrpm-run-command (args) -"Insert COMMAND into the proof queue and then run it. --- adapted from proof-insert-pbp-command --" +"Insert command into the proof queue and then run it. + +\(adapted from ‘proof-insert-pbp-command’)" (let* ((command (pop args)) (act (pop args)) (spans (pop args)) (allspan (pop spans))) (if act (setq command (apply act command spans nil))) (if allspan (setq command (concat "(* " (span-string allspan) " *)\n" command "."))) @@ -428,15 +431,15 @@ If no match found, return the empty string." (return-from 'loop ""))))) (defun pg-pbrpm-translate-position (buffer pos) - "return pos if buffer is goals-buffer otherwise, return the point position in -the goal buffer" + "If BUFFER is goals-buffer, return POS, otherwise the point in the goal buffer." (if (eq proof-goals-buffer buffer) pos (with-current-buffer proof-goals-buffer (point)))) (defun pg-pbrpm-process-click (event start end) -"Returns the list of informations about the click needed to call generate-menu. EVENT is an event." + "Return the list of infos about the click needed to call ‘generate-menu’. +EVENT is an event." (save-excursion (save-window-excursion (mouse-set-point event) @@ -521,8 +524,8 @@ the goal buffer" t) (defun pg-pbrpm-remember-region (event &optional delete) - "Allow multiple selection as a list of spam stored in ???. The current (standard) - selection in the same buffer is also stored" + "Allow multiple selection as a list of span stored in ???. +The current (standard) selection in the same buffer is also stored." (interactive "*e") (setq pg-pbrpm-remember-region-selected-region nil) (let ((mouse-track-drag-up-hook 'pg-pbrpm-remember-region-drag-up-hook) @@ -535,7 +538,8 @@ the goal buffer" (pg-pbrpm-do-remember-region (car pair) (cdr pair)))))) (defun pg-pbrpm-process-region (span) -"Returns the list of informations about the the selected region needed to call generate-menu. span is a span covering the selected region" +"Return the list of infos on the selected region needed to call ‘generate-menu’. +SPAN is a span covering the selected region." (let ((start (span-start span)) (end (span-end span)) (buffer (span-buffer span)) diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el index 997f8bb1..0f427ecb 100644 --- a/generic/pg-pgip.el +++ b/generic/pg-pgip.el @@ -38,7 +38,7 @@ (declare-function pg-response-warning "pg-response") (declare-function pg-response-message "pg-response") -(declare-function proof-segment-up-to "proof-script") +(declare-function proof-segment-up-to "proof-script") (declare-function proof-insert-pbp-command "proof-script") (defalias 'pg-pgip-debug 'proof-debug) @@ -111,7 +111,7 @@ 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 + (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 d89d3c0b..43e0e279 100644 --- a/generic/pg-response.el +++ b/generic/pg-response.el @@ -92,8 +92,7 @@ ;; (defvar pg-response-special-display-regexp nil - "Regexp for `special-display-regexps' (now display-buffer-alist) -for multiple frame use. + "Regexp for ‘display-buffer-alist’ for multiple frame use. Internal variable, setting this will have no effect!") (defconst proof-multiframe-parameters @@ -129,8 +128,10 @@ Internal variable, setting this will have no effect!") (defun proof-guess-3win-display-policy (&optional policy) "Return the 3 windows mode layout policy from user choice POLICY. -If POLIY is smart then guess the good policy from the current -frame geometry, otherwise follow POLICY." +If POLICY is ’smart then guess the good policy from the current +frame geometry, otherwise follow POLICY. + +See ‘proof-layout-windows’ for more details about POLICY." (if (eq policy 'smart) (cond ((>= (frame-width) (* 1.5 split-width-threshold)) 'horizontal) @@ -139,9 +140,10 @@ frame geometry, otherwise follow POLICY." policy)) (defun proof-select-three-b (b1 b2 b3 &optional policy) - "Put the given three buffers into three windows. -Following POLICY, which can be one of 'smart, 'horizontal, -'vertical or 'hybrid." + "Put the three buffers B1, B2, and B3 into three windows. +Following POLICY, which can be 'smart, 'horizontal, 'vertical, or 'hybrid. + +See ‘proof-layout-windows’ for more details about POLICY." (interactive "bBuffer1:\nbBuffer2:\nbBuffer3:") (delete-other-windows) (switch-to-buffer b1) @@ -181,7 +183,8 @@ Following POLICY, which can be one of 'smart, 'horizontal, (defun proof-display-three-b (&optional policy) - "Layout three buffers in a single frame. Only do this if buffers exist." + "Layout three buffers in a single frame. Only do this if buffers exist. +In this case, call ‘proof-select-three-b’ with argument POLICY." (interactive) (when (and (buffer-live-p proof-goals-buffer) (buffer-live-p proof-response-buffer)) @@ -220,9 +223,9 @@ For multiple frame mode, this function obeys the setting of For single frame mode: - In two panes mode, this uses a canonical layout made by splitting -Emacs windows in equal proportions. The splitting is vertical if -emacs width is smaller than `split-width-threshold' and -horizontal otherwise. You can then adjust the proportions by +Emacs windows in equal proportions. The splitting is vertical if +Emacs width is smaller than `split-width-threshold' and +horizontal otherwise. You can then adjust the proportions by dragging the separating bars. - In three pane mode, there are three display modes, depending @@ -238,7 +241,7 @@ dragging the separating bars. response). By default, the display mode is automatically chosen by - considering the current emacs frame width: if it is smaller + considering the current Emacs frame width: if it is smaller than `split-width-threshold' then vertical mode is chosen, otherwise if it is smaller than 1.5 * `split-width-threshold' then hybrid mode is chosen, finally if the frame is larger than @@ -249,7 +252,7 @@ dragging the separating bars. If you want to force one of the layouts, you can set variable `proof-three-window-mode-policy' to 'vertical, 'horizontal or - 'hybrid. The default value is 'smart which sets the automatic + 'hybrid. The default value is 'smart which sets the automatic behaviour described above." (interactive) (cond diff --git a/generic/pg-user.el b/generic/pg-user.el index 21d9479d..126901cb 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -31,8 +31,8 @@ (require 'completion)) ; Loaded dynamically at runtime. (defvar which-func-modes) ; Defined by which-func. -(declare-function proof-segment-up-to "proof-script") -(declare-function proof-interrupt-process "proof-shell") +(declare-function proof-segment-up-to "proof-script") +(declare-function proof-interrupt-process "proof-shell") ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; @@ -46,12 +46,12 @@ ;;;###autoload (defun proof-script-new-command-advance () "Move point to a nice position for a new command, possibly inserting spaces. -Assumes that point is at the end of a command. +Assumes that point is at the end of a command. No effect if `proof-next-command-insert-space' is nil." (interactive) (when proof-next-command-insert-space (let (sps) - (if (and (proof-next-command-new-line) + (if (and (proof-next-command-new-line) (setq sps (skip-chars-forward " \t")) ;; don't break existing lines (eolp)) @@ -93,7 +93,7 @@ Assumes script buffer is current." ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -;; Further movement commands +;; Further movement commands ;; (defun proof-goto-command-start () @@ -135,7 +135,8 @@ Assumes script buffer is current." (backward-char)))))))) (defun proof-forward-command (&optional num) - "Move forward to the start of the next proof region." + "Move forward to the start of the next proof region. +If called interactively, NUM is given by the prefix argument." (interactive "p") (skip-chars-forward " \t\n") (let* ((span (or (span-at (point) 'type) @@ -387,7 +388,7 @@ a proof command." ;;;###autoload (defmacro proof-define-assistant-command (fn doc cmdvar &optional body) - "Define FN (docstring DOC) to send BODY to prover, based on CMDVAR. + "Define FN (docstring DOC): check if CMDVAR is set, then send BODY to prover. BODY defaults to CMDVAR, a variable." `(defun ,fn () ,(concat doc @@ -400,7 +401,8 @@ BODY defaults to CMDVAR, a variable." ;;;###autoload (defmacro proof-define-assistant-command-witharg (fn doc cmdvar prompt &rest body) - "Define command FN to prompt for string CMDVAR to proof assistant. + "Define FN (arg) with DOC: check CMDVAR is set, PROMPT a string and eval BODY. +The BODY can contain occurrences of arg. CMDVAR is a variable holding a function or string. Automatically has history." `(progn (defvar ,(intern (concat (symbol-name fn) "-history")) nil @@ -482,14 +484,14 @@ This is intended as a value for `proof-activate-scripting-hook'" "Write a goal command in the script, prompting for the goal." proof-goal-command "Goal" ; Goals always start at a new line - (let ((proof-next-command-on-new-line t)) + (let ((proof-next-command-on-new-line t)) (proof-issue-new-command arg))) (proof-define-assistant-command-witharg proof-issue-save "Write a save/qed command in the script, prompting for the theorem name." proof-save-command "Save as" ; Saves always start at a new line - (let ((proof-next-command-on-new-line t)) + (let ((proof-next-command-on-new-line t)) (proof-issue-new-command arg))) @@ -524,13 +526,13 @@ It can also be used as a minor mode function: with ARG, turn on iff ARG>0" (defun proof-electric-terminator (&optional count) "Insert terminator char, maybe sending the command to the assistant. If we are inside a comment or string, insert the terminator. -Otherwise, if the variable `proof-electric-terminator-enable' +Otherwise, if the variable `proof-electric-terminator-enable' is non-nil, the command will be sent to the assistant. -To side-step the electric action and possibly insert multiple -characters, use a numeric prefix arg, like M-3 <terminator>." +To side-step the electric action and possibly insert multiple characters, +pass a non-nil COUNT arg, e.g. a numeric prefix such as M-3 <terminator>." (interactive "P") - (if (and + (if (and (not count) proof-electric-terminator-enable (not (proof-inside-comment (point))) @@ -749,7 +751,7 @@ If NUM is negative, move upwards. Return new span." ((idiom (and span (span-property span 'idiom))) (id (and span (span-property span 'id)))) (popup-menu (pg-create-in-span-context-menu - span idiom + span idiom (if id (symbol-name id)))))))) (defun pg-toggle-visibility () @@ -766,7 +768,7 @@ If NUM is negative, move upwards. Return new span." (append (list (pg-span-name span)) (list (vector - "Show/hide" + "Show/hide" (if idiom (list 'pg-toggle-element-visibility (quote idiom) name)) (not (not idiom)))) (list (vector @@ -812,7 +814,7 @@ If NUM is negative, move upwards. Return new span." (pg-hint (format "\\[proof-prf] for goals;%s \\[proof-layout-windows] refreshes" - (if (or proof-three-window-enable + (if (or proof-three-window-enable proof-multiple-frames-enable) "" (format " \\[proof-display-some-buffers] rotates output%s;" @@ -956,7 +958,7 @@ If CALLBACK is set, we invoke that when the command completes." (imenu-add-to-menubar "Index") (progn (when (listp which-func-modes) - (setq which-func-modes + (setq which-func-modes (remove proof-mode-for-script which-func-modes))) (let ((oldkeymap (keymap-parent (current-local-map)))) (if ;; sanity checks in case someone else set local keymap @@ -994,7 +996,8 @@ If CALLBACK is set, we invoke that when the command completes." "Stored incomplete input: string between point and locked.") (defun pg-previous-input (arg) - "Cycle backwards through input history, saving input." + "Cycle backwards through input history, saving input. +If called interactively, ARG is given by the prefix argument." (interactive "*p") (if (and pg-input-ring-index (or ; leaving the "end" of the ring @@ -1008,7 +1011,8 @@ If CALLBACK is set, we invoke that when the command completes." (pg-previous-matching-input "." arg))) (defun pg-next-input (arg) - "Cycle forwards through input history." + "Cycle forwards through input history. +If called interactively, ARG is given by the prefix argument." (interactive "*p") (pg-previous-input (- arg))) @@ -1198,7 +1202,7 @@ removed if it matches the last item in the ring." ;;;###autoload -(defun pg-clear-input-ring () +(defun pg-clear-input-ring () (setq pg-input-ring nil)) @@ -1221,6 +1225,10 @@ removed if it matches the last item in the ring." (defun pg-protected-undo (&optional arg) "As `undo' but avoids breaking the locked region. +A numeric ARG serves as a repeat count. +If called interactively, ARG is given by the prefix argument. +If ARG is omitted, nil, or not numeric, it takes the value 1. + It performs each of the desired undos checking that these operations will not affect the locked region, obeying `proof-strict-read-only' if required. If strict read only behaviour is enforced, the user is queried whether to @@ -1268,7 +1276,7 @@ behavior is expected." (> (proof-queue-or-locked-end) beg) proof-strict-read-only ; edit freely doesn't retract (not (and ; neither does edit in comments - (proof-inside-comment beg) + (proof-inside-comment beg) (proof-inside-comment end)))) (if (or (eq proof-strict-read-only 'retract) (y-or-n-p "Next undo will modify read-only region, retract? ")) @@ -1276,12 +1284,12 @@ behavior is expected." (when (eq last-command 'undo) (setq this-command 'undo)) ;; now we can stop the function without breaking possible undo chains (error - "Cannot undo without retracting to the appropriate position."))) + "Cannot undo without retracting to the appropriate position"))) (undo arg)))) (defun next-undo-elt (arg) - "Returns the undo element that will be processed on next undo/redo, -assuming the undo-in-region behavior will apply if ARG is non-nil." + "Return the undo element that will be processed on next undo/redo. +Assume the undo-in-region behavior will apply if ARG is non-nil." (let ((undo-list (if arg ; handle "undo in region" (undo-make-selective-list (region-beginning) (region-end)) ; can be '(nil) @@ -1318,11 +1326,11 @@ assuming the undo-in-region behavior will apply if ARG is non-nil." ;;;###autoload (defun proof-autosend-enable (&optional nomsg) "Enable or disable autosend behaviour." - (if proof-autosend-timer + (if proof-autosend-timer (cancel-timer proof-autosend-timer)) (when proof-autosend-enable (setq proof-autosend-timer - (run-with-idle-timer proof-autosend-delay + (run-with-idle-timer proof-autosend-delay t 'proof-autosend-loop)) (setq proof-autosend-modified-tick nil) (unless nomsg (message "Automatic sending turned on."))) @@ -1355,10 +1363,10 @@ assuming the undo-in-region behavior will apply if ARG is non-nil." (progn (save-excursion (goto-char (point-max)) - (proof-assert-until-point - (if proof-multiple-frames-enable + (proof-assert-until-point + (if proof-multiple-frames-enable 'no-minibuffer-messages ; nb: not API - '(no-response-display + '(no-response-display no-error-display no-goals-display)))) (proof-shell-wait t) ; interruptible @@ -1381,9 +1389,9 @@ assuming the undo-in-region behavior will apply if ARG is non-nil." ;(skip-chars-forward " \t\n") (message "Trying next commands in prover...") (proof-assert-until-point - (if proof-multiple-frames-enable + (if proof-multiple-frames-enable 'no-minibuffer-messages ; nb: not API - '(no-response-display + '(no-response-display no-error-display no-goals-display)))) (let ((proof-sticky-errors t)) @@ -1401,16 +1409,16 @@ assuming the undo-in-region behavior will apply if ARG is non-nil." (unless (eq qol (proof-queue-or-locked-end)) ; no progress (save-excursion (goto-char qol) - (proof-retract-until-point + (proof-retract-until-point (lambda (beg end) - (span-make-self-removing-span + (span-make-self-removing-span (save-excursion (goto-char beg) (skip-chars-forward " \t\n") - (point)) + (point)) end 'face 'highlight)) - '(no-response-display + '(no-response-display no-error-display no-goals-display))))))) diff --git a/generic/pg-vars.el b/generic/pg-vars.el index 546c955e..d1e5dfa9 100644 --- a/generic/pg-vars.el +++ b/generic/pg-vars.el @@ -27,16 +27,16 @@ ;;; (defvar proof-assistant-cusgrp nil - "Symbol for the customization group of the user options for the proof assistant. + "Symbol for the customization group of user options for the proof assistant. Do not change this variable! It is set automatically by the mode stub defined in proof-site, from the name given in -proof-assistant-table.") +‘proof-assistant-table’.") (defvar proof-assistant-internals-cusgrp nil - "Symbol for the customization group of the PG internal settings proof assistant. + "Symbol for the customization group of PG internal settings. Do not change this variable! It is set automatically by the mode stub defined in proof-site, from the name given in -proof-assistant-table.") +‘proof-assistant-table’.") (defvar proof-assistant "" "Name of the proof assistant Proof General is using. @@ -217,7 +217,7 @@ the form of the menu entry for the setting (this is an Emacs widget type) and the DESCR description string is used as a help tooltip in the settings menu. As TYPE's only the simple types boolean, integer, number and -string are supported (see `proof-menu-entry-for-setting'). Other +string are supported (see `proof-menu-entry-for-setting'). Other types will yield an error when constructing the proof assistant menu from this list. diff --git a/generic/pg-xml.el b/generic/pg-xml.el index 5de8095d..18285572 100644 --- a/generic/pg-xml.el +++ b/generic/pg-xml.el @@ -61,6 +61,7 @@ (defun pg-xml-parse-buffer (&optional buffer nomsg start end) "Parse an XML documment in BUFFER (defaulting to current buffer). +Display progress message unless NOMSG is non-nil. Parsing according to `xml-parse-file' of xml.el. Optional START and END bound the parse." (unless nomsg @@ -83,7 +84,7 @@ Optional START and END bound the parse." (or val (if optional defaultval - (pg-xml-error "pg-xml-get-attr: Didn't find required %s attribute in %s element" + (pg-xml-error "Function pg-xml-get-attr: Didn't find required %s attribute in %s element" attribute (xml-node-name node)))))) (defun pg-xml-child-elts (node) @@ -100,7 +101,7 @@ Optional START and END bound the parse." (xml-node-name node))))) (defun pg-xml-get-child (child node) - "Return single element CHILD of node, give error if more than one." + "Return single element CHILD of NODE, give error if more than one." (let ((children (xml-get-children node child))) (if (> (length children) 1) (progn @@ -141,8 +142,9 @@ Optional START and END bound the parse." ;; based on xml-debug-print from xml.el (defun pg-xml-output-internal (xml indent-string outputfn) - "Outputs the XML tree using OUTPUTFN, which should accept a list of args. -Output with indentation INDENT-STRING (or none if nil)." + "Output the XML tree. +Use indentation INDENT-STRING (or none if nil). +Cal OUTPUTFN, which should accept a list of args." (let ((tree xml) attlist) (funcall outputfn (or indent-string "") "<" (symbol-name (xml-node-name tree))) @@ -167,7 +169,7 @@ Output with indentation INDENT-STRING (or none if nil)." (pg-xml-output-internal node (if indent-string (concat indent-string " ")) outputfn)) ((stringp node) (funcall outputfn node)) (t - (error "pg-xml-output-internal: Invalid XML tree")))) + (error "Function pg-xml-output-internal: Invalid XML tree")))) (funcall outputfn (if indent-string (concat "\n" indent-string) "") "</" (symbol-name (xml-node-name xml)) ">")) diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el index 5cd83ddd..e93c4da2 100644 --- a/generic/proof-autoloads.el +++ b/generic/proof-autoloads.el @@ -292,7 +292,7 @@ Additional properties in the ARGS prop list may include: pgdynamic flag If flag is non-nil, this setting is a dynamic one that is particular to the running instance of the prover. - Automatically set by preferences configured from PGIP + Automatically set by preferences configured from PGIP askprefs message. This macro also extends the `proof-assistant-settings' list. @@ -654,7 +654,7 @@ also as the 'response property on the span. Optional argument MOUSEFACE means use the given face as a mouse highlight face, if it is a face, otherwise, if it is non-nil but not a face, -do not add a mouse highlight. +do not add a mouse highlight. In any case, a mouse highlight and tooltip are only set if `proof-output-tooltips' is non-nil. @@ -783,7 +783,7 @@ Busy wait for `proof-shell-busy' to become nil, reading from prover. Needed between sequences of commands to maintain synchronization, because Proof General does not allow for the action list to be extended -in some cases. Also is considerably faster than leaving the Emacs +in some cases. Also is considerably faster than leaving the Emacs top-level command loop to read from the prover. Called by `proof-shell-invisible-command' and `proof-process-buffer' diff --git a/generic/proof-config.el b/generic/proof-config.el index bd5ca611..ea7fda8f 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -259,7 +259,7 @@ or `proof-script-parse-function'." :group 'prover-config) (defcustom proof-script-sexp-commands nil - "Non-nil if script has LISP-like syntax: commands are top-level sexps. + "Non-nil if script has Lisp-like syntax: commands are top-level sexps. You should set this variable in script mode configuration. To configure command recognition properly, you must set at least one @@ -411,11 +411,11 @@ It's safe to leave this setting as nil." :group 'proof-script) (defcustom proof-save-with-hole-result 2 - "How to get theorem name after `proof-save-with-hole-regexp' match. + "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' -should match the entire command" +If an int N, use ‘match-string’ to get the value of the Nth parenthesis matched. +If a string, use ‘replace-match’. In this case, ‘proof-save-with-hole-regexp’ +should match the entire command." :type '(choice string integer) :group 'proof-script) @@ -441,11 +441,11 @@ It's safe to leave this setting as nil." :group 'proof-script) (defcustom proof-goal-with-hole-result 2 - "How to get theorem name after `proof-goal-with-hole-regexp' match. + "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 -should match the entire command" +If an int N, use ‘match-string’ to get the value of the Nth parenthesis matched. +If a string, use ‘replace-match’. In this case, ‘proof-goal-with-hole-regexp’ +should match the entire command." :type '(choice string integer) :group 'proof-script) @@ -683,10 +683,10 @@ assistant, for example, to compile a completed file." (defcustom proof-no-fully-processed-buffer nil "Set to t if buffers should always retract before scripting elsewhere. Leave at nil if fully processed buffers make sense for the current -proof assistant. If nil the user can choose to fully assert a -buffer when starting scripting in a different buffer. If t there +proof assistant. If nil the user can choose to fully assert a +buffer when starting scripting in a different buffer. If t there is only the choice to fully retract the active buffer before -starting scripting in a different buffer. This last behavior is +starting scripting in a different buffer. This last behavior is needed for Coq." :type 'boolean :group 'proof-script) @@ -760,12 +760,12 @@ Elisp errors will be trapped when evaluating; set :group 'proof-script) (defcustom proof-script-insert-newlines t - "if non-nil inserts a newline between each message in response buffer." + "If non-nil, insert a newline between each message in response buffer." :type 'boolean :group 'proof-script) (defcustom proof-script-color-error-messages t - "if non-nil error messages will be globally colored with corresponding face. + "If non-nil, error messages will be globally colored with corresponding face. If prover mode has a better coloring mechanism for errors, set this to nil." :type 'boolean :group 'proof-script) @@ -1195,18 +1195,18 @@ If nil, use the whole of the output from the match on :group 'proof-shell) (defcustom proof-shell-empty-action-list-command nil - "A function returning a list of commands (strings) to be sent -to the prover when the last command in the queue has been -performed. Typically to ask for some informational -display (goals, etc). + "A function returning a list of commands (strings). +These commands are sent to the prover when the last command in the queue +has been performed. +Typically to ask for some informational display (goals, etc.) The function takes as argument the last command in the queue. -NOTE 1: The commands will be tagged invisible, i.e. not related +NOTE 1: The commands will be tagged invisible, i.e., not related to a place in the buffer. NOTE 2: The commands should NOT have any effect on the state of -the prover. Otherwise running the script outside pg would be +the prover. Otherwise running the script outside pg would be inconsistent." :type 'function :group 'proof-shell) @@ -1563,7 +1563,7 @@ This setting is used inside the function `proof-format-filename'." "The value of `process-connection-type' for the proof shell. Set non-nil for ptys, nil for pipes. -NOTE: In emacs >= 24 (checked for 24 and 25.0.50.1), t is not a +NOTE: In Emacs >= 24 (checked for 24 and 25.0.50.1), t is not a good choice: input is cut after 4095 chars, which hangs pg." :type 'boolean :group 'proof-shell) @@ -1589,14 +1589,14 @@ if you don't need it (slight speed penalty)." :group 'proof-shell) (defcustom proof-shell-extend-queue-hook nil - "Hooks run by proof-extend-queue before extending `proof-action-list'. + "Hooks run by ‘proof-extend-queue’ before extending `proof-action-list'. Can be used to run additional actions before items are added to the queue \(such as compiling required modules for Coq) or to modify the items that are going to be added to -`proof-action-list'. The items that are about to be added are +`proof-action-list'. The items that are about to be added are bound to `queueitems'." :type '(repeat function) - :group 'proof-shell) + :group 'proof-shell) (defcustom proof-shell-insert-hook nil "Hooks run by `proof-shell-insert' before inserting a command. @@ -1644,12 +1644,12 @@ it is added to the queue of commands." (defcustom proof-assert-command-hook nil "Hooks run before asserting a command (or a set of commands). Can be used to insert commands before any (set of) input sent -by the user. It is run by `proof-assert-until-point'. +by the user. It is run by `proof-assert-until-point'. WARNING: don't call `proof-assert-until-point' in this hook, you would loop forever. -Example of use: Insert a command to adapt printing width. Note +Example of use: Insert a command to adapt printing width. Note that `proof-shell-insert-hook' may be use instead (see lego mode) if no more prompt will be displayed (see `proof-shell-insert-hook' for details)." @@ -1658,13 +1658,13 @@ if no more prompt will be displayed (see (defcustom proof-retract-command-hook nil "Hooks run before retracting a command (or a set of commands). -Can be used to insert commands. It is run by +Can be used to insert commands. It is run by `proof-retract-until-point'. WARNING: don't call `proof-retract-until-point' in this hook, you would loop forever. -Example of use: Insert a command to adapt printing width. Note +Example of use: Insert a command to adapt printing width. Note that `proof-shell-insert-hook' may be use instead (see lego mode) if no more prompt will be displayed (see `proof-shell-insert-hook' for details)." @@ -1704,14 +1704,14 @@ something in scripting buffer, `save-excursion' and/or `set-buffer'." (defcustom proof-shell-signal-interrupt-hook nil "Run when the user tries to interrupt the prover. This hook is run inside `proof-interrupt-process' when the user -tries to interrupt the proof process. It is therefore run earlier +tries to interrupt the proof process. It is therefore run earlier than `proof-shell-handle-error-or-interrupt-hook', which runs when the interrupt is acknowledged inside `proof-shell-exec-loop'. This hook also runs when the proof assistent is killed. Hook functions should set the dynamic variable `prover-was-busy' -to t if there might have been a reason to interrupt. Otherwise +to t if there might have been a reason to interrupt. Otherwise the generic interrupt handler might issue a prover-not-busy error." :type '(repeat function) diff --git a/generic/proof-depends.el b/generic/proof-depends.el index 74332c71..72beb1d2 100644 --- a/generic/proof-depends.el +++ b/generic/proof-depends.el @@ -181,7 +181,7 @@ Called from `proof-done-advancing' when a save is processed and (vector menuname nil nil)))) (defun proof-dep-split-deps (deps) - "Split dependencies into named nested lists according to dotted prefixes." + "Split dependencies DEPS into named nested lists according to dotted prefixes." ;; NB: could handle deeper nesting here, but just do one level for now. (let (nested toplevel) ;; Add each name into a nested list or toplevel list @@ -223,6 +223,7 @@ NAMEFN is applied to each element of LIST to make the names." (defun proof-goto-dependency (name span) "Go to the start of SPAN." + ;; FIXME(EMD): seems buggy as NAME is not used ;; FIXME: check buffer is right one. Later we'll allow switching buffer ;; here and jumping to different files. (goto-char (span-start span)) diff --git a/generic/proof-easy-config.el b/generic/proof-easy-config.el index 59fa03e5..4dc2e1d4 100644 --- a/generic/proof-easy-config.el +++ b/generic/proof-easy-config.el @@ -62,7 +62,8 @@ `(define-derived-mode ,mode ,parent ,modename nil ,@fullbody))))) (defun proof-easy-config-check-setup (sym name) - "A number of simple checks." + "Perform a number of simple checks. +The proof assistant is denoted by symbol SYM and string NAME." (let ((msg "")) ;; At the moment we just check that the symbol/name used ;; in the macro matches that in `proof-assistant-table' @@ -84,7 +85,7 @@ (not (eq proof-assistant-symbol sym)) (setq msg (format "\nproof-assistant symbol: '%s doesn't match expected '%s" proof-assistant-symbol sym)))) - (error "proof-easy-config: PG already in use or name/symbol mismatch %s" + (error "Macro proof-easy-config: PG already in use or name/symbol mismatch %s" msg)) (t ;; Setting these here is nice for testing: no need to get @@ -94,9 +95,10 @@ ;;;###autoload (defmacro proof-easy-config (sym name &rest body) - "Configure Proof General for proof-assistant using BODY as a setq body. + "Configure Proof General for a given proof assistant. The symbol SYM and string name NAME must match those given in -the `proof-assistant-table', which see." + the `proof-assistant-table', which see. +Additional arguments are taken into account as a setq BODY." `(progn (proof-easy-config-check-setup ,sym ,name) (setq @@ -105,3 +107,7 @@ the `proof-assistant-table', which see." ;; (provide 'proof-easy-config) + +(provide 'proof-easy-config) + +;;; proof-easy-config.el ends here diff --git a/generic/proof-menu.el b/generic/proof-menu.el index f893a9f6..fc18d504 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -318,7 +318,7 @@ without adjusting window layout." (proof-deftoggle proof-delete-empty-windows) (proof-deftoggle proof-shrink-windows-tofit) (proof-deftoggle proof-multiple-frames-enable proof-multiple-frames-toggle) -(proof-deftoggle proof-layout-windows-on-visit-file +(proof-deftoggle proof-layout-windows-on-visit-file proof-layout-windows-eagerly-toggle) (proof-deftoggle proof-three-window-enable proof-three-window-toggle) (proof-deftoggle proof-auto-raise-buffers proof-auto-raise-toggle) @@ -342,7 +342,7 @@ without adjusting window layout." (proof-ass-sym maths-menu-enable) 'proof-maths-menu-toggle)) (defun proof-keep-response-history () - "Enable associated buffer histories following `proof-keep-response-history'." + "Enable associated buffer histories following option `proof-keep-response-history'." (if proof-keep-response-history (proof-map-buffers (proof-associated-buffers) (bufhist-init)) (proof-map-buffers (proof-associated-buffers) (bufhist-exit)))) @@ -371,7 +371,7 @@ without adjusting window layout." ["Beep on Errors" proof-shell-quiet-errors-toggle :style toggle :selected (not proof-shell-quiet-errors) - :help "Beep on errors or interrupts"] + :help "Beep on errors or interrupts"] ["Fly Past Comments" proof-script-fly-past-comments-toggle :style toggle :selected proof-script-fly-past-comments @@ -613,7 +613,7 @@ without adjusting window layout." ;; (defun proof-set-document-centred () - "Select options for document-centred working" + "Select options for document-centred working." (interactive) (proof-full-annotation-toggle 1) (proof-auto-raise-toggle 0) @@ -626,9 +626,9 @@ without adjusting window layout." (defun proof-set-non-document-centred () - "Set options for classic Proof General interaction" + "Set options for classic Proof General interaction." (interactive) - ;; default: (proof-full-annotation-toggle 1) + ;; default: (proof-full-annotation-toggle 1) (proof-auto-raise-toggle 1) (proof-colour-locked-toggle 1) (proof-sticky-errors-toggle 0) @@ -744,7 +744,7 @@ without adjusting window layout." ;;; Define stuff from favourites (defun proof-def-favourite (command inscript menuname &optional key new) - "Define and a \"favourite\" proof assisant function. + "Define and a \"favourite\" proof assistant function. See doc of `proof-add-favourite' for first four arguments. Extra NEW flag means that this should be a new favourite, so check that function defined is not already bound. @@ -987,7 +987,7 @@ We first clear the dynamic settings from `proof-assistant-settings'." (let (cmds) (dolist (setting proof-assistant-settings) (let ((sym (car setting)) - (pacmd (cadr setting))) + (pacmd (cadr setting))) (if (and pacmd (or (not (get sym 'pgdynamic)) (proof-ass-differs-from-default sym))) @@ -1038,7 +1038,7 @@ value) and the second for false." ((consp string) ;; true/false options (if curvalue (car string) (cdr string))) (t ;; no idea what to do - (error "proof-assistant-format: called with invalid string arg %s" string))))) + (error "Function proof-assistant-format: called with invalid string arg %s" string))))) (if proof-assistant-setting-format (funcall proof-assistant-setting-format setting) setting))) diff --git a/generic/proof-script.el b/generic/proof-script.el index 0baf3d5f..3a663a3a 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -287,8 +287,8 @@ next time an error is processed." (defun proof-restart-buffers (buffers) "Remove all extents in BUFFERS and maybe reset `proof-script-buffer'. The high-level effect is that all members of BUFFERS are -completely unlocked, including all the necessary cleanup. No -effect on a buffer which is nil or killed. If one of the buffers +completely unlocked, including all the necessary cleanup. No +effect on a buffer which is nil or killed. If one of the buffers is the current scripting buffer, then `proof-script-buffer' will deactivated." (mapcar @@ -416,7 +416,7 @@ Works on any buffer." (eq (proof-unprocessed-begin) (point-min))) (defun proof-only-whitespace-to-locked-region-p () - "Non-nil if only whitespace from char-after point and end of locked region. + "Non-nil if only whitespace from char after point to end of locked region. Point must be after the locked region or this will signal an error." (save-excursion (or (eq (point) (point-max)) @@ -510,7 +510,7 @@ Intended as a hook function for `proof-shell-handle-error-or-interrupt-hook'." (clrhash (cdr idtbl)))) (defun pg-remove-element (idiom id) - "Remove the identifier ID from the script portion IDIOM." + "From the script portion IDIOM, remove the identifier ID." (let* ((elts (cdr-safe (assq idiom pg-script-portions))) (span (and elts (gethash idiom elts)))) (when span @@ -518,8 +518,8 @@ Intended as a hook function for `proof-shell-handle-error-or-interrupt-hook'." (remhash id elts)))) (defun pg-get-element (idiomsym id) - "Return proof script element of type IDIOM identifier ID. -IDIOM is a symbol, ID is a string." + "Return proof script element of type IDIOMSYM with identifier ID. +IDIOMSYM is a symbol, ID is a string." (assert (symbolp idiomsym)) (assert (stringp id)) (let ((idsym (intern id)) @@ -581,15 +581,15 @@ This is a value for the overlay 'invisible property." (intern (concat "pg-" (symbol-name (or idiom 'other))))) (defun pg-set-element-span-invisible (span invisiblep) - "Function to adjust visibility of span to INVISIBLEP. + "Function to adjust visibility of SPAN to INVISIBLEP. We use list values of the 'invisible property which contain private symbols, that should play well with other conforming modes and `buffer-invisibility-spec'." (let* ((invisible-prop (pg-invisible-prop (span-property span 'idiom))) (invisible-rest (remq invisible-prop (span-property span 'invisible)))) - (span-set-property span 'invisible - (if invisiblep + (span-set-property span 'invisible + (if invisiblep (cons invisible-prop invisible-rest) invisible-rest)))) @@ -604,12 +604,12 @@ and `buffer-invisibility-spec'." (pg-set-element-span-invisible span invisible)) (defun pg-make-element-invisible (idiomsym id) - "Make element ID of type IDIOMSYM invisible, with ellipsis." + "Make element of type IDIOMSYM and identifier ID invisible, with ellipsis." (let ((span (pg-get-element idiomsym id))) (if span (pg-set-element-span-invisible span t)))) (defun pg-make-element-visible (idiomsym id) - "Make element ID of type IDIOMSYM visible." + "Make element of type IDIOMSYM and identifier ID visible." (let ((span (pg-get-element idiomsym id))) (if span (pg-set-element-span-invisible span nil)))) @@ -625,8 +625,8 @@ IDIOMSYM is a symbol and ID is a strings." (list (intern (completing-read - (concat "Make " - (if current-prefix-arg "in" "") + (concat "Make " + (if current-prefix-arg "in" "") "visible all regions of: ") (apply 'vector pg-idioms) nil t)) current-prefix-arg)) @@ -641,7 +641,7 @@ IDIOMSYM is a symbol and ID is a strings." (maphash alterfn elts))))) (defun pg-add-proof-element (name span controlspan) - "Add a span proof element to SPAN with name NAME and parent CONTROLSPAN." + "Add a span proof element (named NAME) to SPAN with parent CONTROLSPAN." (let ((proofid (proof-next-element-id 'proof))) (pg-add-element 'proof proofid span name) ;; Set id in controlspan [NB: intern here means symbol-name elsewhere] @@ -665,8 +665,7 @@ Each span has a 'type property, one of: 'vanilla Initialised in proof-semis-to-vanillas, for 'comment A comment outside a command. 'proverproc A region closed by the prover, processed outwith PG - 'pbp A PBP command inserted automatically into the script -" + 'pbp A PBP command inserted automatically into the script." (let ((type (span-property span 'type)) (idiom (span-property span 'idiom)) (name (span-property span 'name)) @@ -995,7 +994,7 @@ Gives a message in the minibuffer and busy-waits for the retraction or processing to complete. If it fails for some reason, an error is signalled here." (unless (or (eq action 'process) (eq action 'retract)) - (error "proof-protected-process-or-retract: invalid argument")) + (error "Invalid argument (in proof-protected-process-or-retract)")) (let ((buf (or buffer (current-buffer)))) (with-current-buffer buf (unless (proof-action-completed action) @@ -1093,7 +1092,7 @@ retract or assert, or automatically take the action indicated in the user option `proof-auto-action-when-deactivating-scripting'. If `proof-no-fully-processed-buffer' is t there is only the choice -to fully retract the active scripting buffer. In this case the +to fully retract the active scripting buffer. In this case the active scripting buffer is retracted even if it was fully processed. Setting `proof-auto-action-when-deactivating-scripting' to 'process is ignored in this case. @@ -1117,7 +1116,7 @@ questioning the user. It is used to make a value for the `kill-buffer-hook' for scripting buffers, so that when a scripting buffer is killed it is always retracted." (interactive) - (proof-with-current-buffer-if-exists + (proof-with-current-buffer-if-exists proof-script-buffer ;; Examine buffer. @@ -1277,7 +1276,7 @@ activation is considered to have failed and an error is given." (eq 'interrupt proof-shell-last-output-kind)) (proof-deactivate-scripting) ;; turn off again! ;; Give an error to prevent further actions. - (error + (error "Scripting not activated because of error or interrupt"))))))) @@ -1405,7 +1404,7 @@ Argument SPAN has just been processed." (pg-add-element 'comment id bodyspan) (span-set-property span 'id (intern id)) (span-set-property span 'idiom 'comment) - (let ((proof-shell-last-output "")) ; comments not sent, no last output + (let ((proof-shell-last-output "")) ; comments not sent, no last output (pg-set-span-helphighlights bodyspan)) ;; possibly evaluate some arbitrary Elisp. SECURITY RISK! @@ -1512,8 +1511,9 @@ Argument SPAN has just been processed." (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;." + "Make new goal-save span, using GSPAN. +Subroutine of `proof-done-advancing-save'. +Argument GOALEND is the end of the goal." (unless proof-arbitrary-undo-positions (span-set-end gspan saveend) (span-set-property gspan 'type 'goalsave)) @@ -1646,7 +1646,7 @@ Subroutine of `proof-done-advancing-save'." This partitions the script buffer into contiguous regions, classifying them by type. Return a list of lists of the form - (TYPE TEXT ENDPOS) + \(TYPE TEXT ENDPOS) where: @@ -1860,8 +1860,8 @@ The optional QUEUEFLAGS are added to each queue item." (span-set-property span 'cmd cmd) (setq alist (cons qitem alist)))) ;; ignored text - (let ((qitem - (list span nil cb queueflags))) ; nil was `proof-no-command' + (let ((qitem + (list span nil cb queueflags))) ; nil was `proof-no-command' (span-set-property span 'type 'comment) (setq alist (cons qitem alist)))) (setq start end))) @@ -1923,7 +1923,7 @@ try to avoid duplicating them in the buffer. When used in the locked region (and so with strict read only off), it always defaults to inserting a semi (nicer might be to parse for a comment, and insert or skip to the next semi)." - (let ((mrk (point)) + (let ((mrk (point)) (termregexp (regexp-quote proof-terminal-string)) ins incomment nwsp) (if (< mrk (proof-unprocessed-begin)) @@ -2045,9 +2045,8 @@ We update display after proof process has reset its state. See also the documentation for `proof-retract-until-point'. Optionally delete the region corresponding to the proof sequence. After an undo, we clear the proof completed flag. The rationale -is that undoing never leaves prover in a \"proof just completed\" -state, which is true for some proof assistants (but probably not -others)." +is that undoing never leaves prover in a \"proof just completed\" state, +which is true for some proof assistants (but probably not others)." ;; TODO: need to fixup proof-nesting-depth (setq proof-shell-proof-completed nil) (if (span-live-p span) @@ -2074,7 +2073,7 @@ others)." ;; State of scripting may have changed now (run-hooks 'proof-state-change-hook)) -(defun proof-setup-retract-action (start end proof-commands remove-action &optional +(defun proof-setup-retract-action (start end proof-commands remove-action &optional displayflags) "Make span from START to END which corresponds to retraction. Returns retraction action destined for proof shell queue, and make span. @@ -2186,7 +2185,7 @@ DISPLAYFLAGS control output shown to user, see `proof-action-list'." undo-action displayflags)))) - (proof-start-queue (min start end) (proof-unprocessed-begin) + (proof-start-queue (min start end) (proof-unprocessed-begin) actions 'retracting))) (defun proof-retract-until-point-interactive (&optional delete-region) @@ -2195,7 +2194,7 @@ If invoked outside a locked region, undo the last successfully processed command. If called with a prefix argument (DELETE-REGION non-nil), also delete the retracted region from the proof-script." (interactive "P") - (proof-retract-until-point + (proof-retract-until-point (if delete-region 'kill-region))) (defun proof-retract-until-point (&optional undo-action displayflags) @@ -2205,8 +2204,8 @@ the locked region. If invoked outside the locked region, undo the last successfully processed command. See `proof-retract-target'. After retraction has succeeded in the prover, the filter will call -`proof-done-retracting'. If UNDO-ACTION is non-nil, it will -then be invoked on the region in the proof script corresponding to +`proof-done-retracting'. If UNDO-ACTION is non-nil, it will +then be invoked on the region in the proof script corresponding to the proof command sequence. DISPLAYFLAGS control output shown to user, see `proof-action-list'. @@ -2218,7 +2217,7 @@ of effects: for scripting again which may involve retracting other (dependent) files. -2. We may query the user whether to save some buffers. +2. We may query the user whether to save some buffers. Step 2 may seem odd -- we're undoing (in) the buffer, after all -- but what may happen is that when scripting starts going @@ -2371,9 +2370,9 @@ mode features, but are only ever processed atomically by the proof assistant." (setq proof-script-buffer-file-name buffer-file-name) - (setq font-lock-defaults + (setq font-lock-defaults (list '(proof-script-font-lock-keywords) - ;; see defadvice in proof-syntax + ;; see defadvice in proof-syntax (fboundp (proof-ass-sym font-lock-fontify-syntactically-region)))) ;; Has buffer already been processed? @@ -2593,7 +2592,7 @@ finish setup which depends on specific proof assistant configuration." ;; Invisibility management: show ellipsis (mapc (lambda (p) - (add-to-invisibility-spec + (add-to-invisibility-spec (cons (pg-invisible-prop p) t))) pg-all-idioms) @@ -2686,7 +2685,7 @@ Stores recent results of `proof-segment-up-to' in reverse order.") (if (and proof-use-parser-cache ;; safety off valve proof-segment-up-to-cache - (>= (proof-queue-or-locked-end) + (>= (proof-queue-or-locked-end) proof-segment-up-to-cache-start) (setq res (proof-segment-cache-contents-for pos)) ;; only use result if last edit point is >1 segment below @@ -2710,7 +2709,7 @@ Stores recent results of `proof-segment-up-to' in reverse order.") (defun proof-segment-cache-contents-for (pos) ;; only return result if we have cache for complete region - (when (<= pos proof-segment-up-to-cache-end) + (when (<= pos proof-segment-up-to-cache-end) (let ((semis proof-segment-up-to-cache) (start (proof-queue-or-locked-end)) usedsemis semiend) @@ -2719,7 +2718,7 @@ Stores recent results of `proof-segment-up-to' in reverse order.") (if (> semiend start) (setq usedsemis (cons (car semis) usedsemis))) (setq semis - (if (or (< semiend pos) + (if (or (< semiend pos) ;; matches parsing-until-find-something behaviour (and (= semiend pos) (not usedsemis))) (cdr semis)))) diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 00d8b1d7..b5bbcd9f 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -59,12 +59,12 @@ The value is a list of lists of the form which is the queue of things to do. -SPAN is a region in the sources, where COMMANDS come from. Often, +SPAN is a region in the sources, where COMMANDS come from. Often, additional properties are recorded as properties of SPAN. COMMANDS is a list of strings, holding the text to be send to the -prover. It might be the empty list if nothing needs to be sent to -the prover, such as, for comments. Usually COMMANDS +prover. It might be the empty list if nothing needs to be sent to +the prover, such as, for comments. Usually COMMANDS contains just 1 string, but it might also contains more elements. The text should be obtained with `(mapconcat 'identity COMMANDS \" \")', where the last argument @@ -105,14 +105,13 @@ See the functions `proof-start-queue' and `proof-shell-exec-loop'.") "Signals that some items are waiting outside of `proof-action-list'. If this is t it means that some items from the queue region are waiting for being processed in a place different from -`proof-action-list'. In this case Proof General must behave as if -`proof-action-list' would be non-empty, when it is, in fact, -empty. +`proof-action-list'. In this case Proof General must behave as if +`proof-action-list' would be non-empty, when it is, in fact, empty. This is used, for instance, for parallel background compilation for Coq: The Require command and the following items are not put into `proof-action-list' and are stored somewhere else until the -background compilation finishes. Then those items are put into +background compilation finishes. Then those items are put into `proof-action-list' for getting processed.") @@ -158,8 +157,8 @@ from calling `proof-shell-exit'.") ;; (defcustom proof-shell-active-scripting-indicator - '(:eval (propertize - " Scripting " 'face + '(:eval (propertize + " Scripting " 'face (cond (proof-shell-busy 'proof-queue-face) ((eq proof-shell-last-output-kind 'error) 'proof-script-sticky-error-face) @@ -224,7 +223,7 @@ No change to current buffer or point." ;;;###autoload (defsubst proof-shell-live-buffer () - "Return non-nil if proof-shell-buffer is live." + "Return non-nil if ‘proof-shell-buffer’ is live." (and proof-shell-buffer (buffer-live-p proof-shell-buffer) (scomint-check-proc proof-shell-buffer))) @@ -262,10 +261,10 @@ If QUEUEMODE is supplied, set the lock to that value." :group 'proof-shell) (defvar proof-shell-filter-active nil - "t when `proof-shell-filter' is running.") + "Variable equal to t if `proof-shell-filter' is running.") (defvar proof-shell-filter-was-blocked nil - "t when a recursive call of `proof-shell-filter' was blocked. + "Variable equal to t if a recursive call of `proof-shell-filter' was blocked. In this case `proof-shell-filter' must be called again after it finished.") (defun proof-shell-set-text-representation () @@ -358,7 +357,7 @@ process command." ;; The next few settings control the proof assistant encoding. - ;; See Elisp manual for recommendations for coding systems. + ;; See Elisp manual for recommendations for coding systems. ;; Modern versions of proof systems should be Unicode ;; clean, i.e., outputing only ASCII characters or using a @@ -376,7 +375,7 @@ process command." (cons (if (getenv "LANG") (format "LANG=%s" - (replace-regexp-in-string + (replace-regexp-in-string "\\.UTF-8" "" (getenv "LANG"))) "LANG=C") @@ -487,7 +486,7 @@ shell buffer, called by `proof-shell-bail-out' if process exits." (when (and alive proc) (catch 'exited (setq proof-shell-exit-in-progress t) - (set-process-sentinel + (set-process-sentinel proc (lambda (p m) (throw 'exited t))) @@ -520,7 +519,7 @@ shell buffer, called by `proof-shell-bail-out' if process exits." (proof-shell-clear-state) (run-hooks 'proof-shell-kill-function-hooks) - ;; Remove auxiliary windows, trying to stop proliferation of + ;; Remove auxiliary windows, trying to stop proliferation of ;; frames (NB: loses if user has switched buffer in special frame) (if (and proof-multiple-frames-enable proof-shell-fiddle-frames) @@ -558,7 +557,7 @@ shell buffer, called by `proof-shell-bail-out' if process exits." This simply kills the `proof-shell-buffer' relying on the hook function -`proof-shell-kill-function' to do the hard work. If optional +`proof-shell-kill-function' to do the hard work. If optional argument DONT-ASK is non-nil, the proof process is terminated without confirmation. @@ -680,7 +679,7 @@ In both cases we then sound a beep, clear the queue and spans and finally we call `proof-shell-handle-error-or-interrupt-hook'. Commands which are not part of regular script management (with -non-empty flags='no-error-display) will not cause any display action. +FLAGS containing 'no-error-display) will not cause any display action. This is called in two places: (1) from the output processing functions, in case we find an error or interrupt message output, @@ -697,7 +696,7 @@ didn't cause prover output." "Interrupt: script management may be in an inconsistent state (but it's probably okay)")) (t ; error - (if proof-shell-delayed-output-start + (if proof-shell-delayed-output-start (save-excursion (proof-shell-handle-delayed-output))) (proof-shell-handle-error-output @@ -724,11 +723,11 @@ unless the FLAGS for the command are non-nil (see `proof-action-list')." (proof-with-current-buffer-if-exists proof-script-buffer (save-excursion - (proof-script-clear-queue-spans-on-error badspan + (proof-script-clear-queue-spans-on-error badspan (eq err-or-int 'interrupt)))) ;; Note: coq-par-emergency-cleanup, which might be called via ;; proof-shell-handle-error-or-interrupt-hook below, assumes that - ;; proof-action-list is empty on error. + ;; proof-action-list is empty on error. (setq proof-action-list nil) (proof-release-lock) (unless flags @@ -739,7 +738,7 @@ unless the FLAGS for the command are non-nil (see `proof-action-list')." (run-hooks 'proof-shell-handle-error-or-interrupt-hook)))) (defun proof-goals-pos (span maparg) - "Given a span, return the start of it if corresponds to a goal, nil otherwise." + "Given a SPAN, return the start of it if corresponds to a goal, nil otherwise." (and (eq 'goal (car (span-property span 'proof-top-element))) (span-start span))) @@ -756,7 +755,7 @@ This is a hook function for proof-shell-handle-delayed-output-hook." (defsubst proof-shell-string-match-safe (regexp string) - "Like string-match except returns nil if REGEXP is nil." + "Like (string-match REGEXP STRING), but return nil if REGEXP is nil." (and regexp (string-match regexp string))) (defun proof-shell-handle-immediate-output (cmd start end flags) @@ -787,7 +786,7 @@ after a completed proof." (cond ;; TODO: Isabelle has changed (since 2009) and is now amalgamating ;; output between prompts, and does e.g., - ;; GOALS + ;; GOALS ;; ERROR ;; we need to override delayed output from the previous ;; command with delayed output from this command to handle that! @@ -878,9 +877,9 @@ single string. The ACTION argument is a symbol which is typically the name of a callback for when each string has been processed. -This calls `proof-shell-insert-hook'. The arguments `action' and -`scriptspan' may be examined by the hook to determine how to modify -the `string' variable (exploiting dynamic scoping) which will be +This calls `proof-shell-insert-hook'. The arguments ACTION and +SCRIPTSPAN may be examined by the hook to determine how to modify +the string variable (exploiting dynamic scoping) which will be the command actually sent to the shell. Note that the hook is not called for the empty (null) string @@ -959,7 +958,7 @@ track what happens in the proof queue." "Non-nil if we should switch to silent mode based on size of queue." (if (and proof-shell-start-silent-cmd ; configured (not proof-full-annotation) ; always noisy - (not proof-tree-external-display) ; no proof-tree display + (not proof-tree-external-display) ; no proof-tree display (not proof-shell-silent)) ; already silent ;; NB: to be more accurate we should only count number ;; of scripting items in the list (not e.g. invisibles). @@ -1044,7 +1043,7 @@ being processed." proof-action-list) (cons (car proof-action-list) ; after current (cons (proof-shell-stop-silent-item) - (cdr proof-action-list)))))) + (cdr proof-action-list)))))) (when nothingthere ; start sending commands (proof-grab-lock queuemode) (setq proof-shell-last-output-kind nil) @@ -1059,11 +1058,11 @@ being processed." ;;;###autoload (defun proof-start-queue (start end queueitems &optional queuemode) - "Begin processing a queue of commands in QUEUEITEMS. + "Begin processing a queue of commands. If START is non-nil, START and END are buffer positions in the active scripting buffer for the queue region. -This function calls `proof-add-to-queue'." +This function calls ‘proof-add-to-queue’ with args QUEUEITEMS and QUEUEMODE." (if start (proof-set-queue-endpoints start end)) (proof-add-to-queue queueitems queuemode)) @@ -1173,7 +1172,7 @@ contains only invisible elements for Prooftree synchronization." (proof-shell-insert-action-item (car proof-action-list))) ;; process the delayed callbacks now - (mapc 'proof-shell-invoke-callback cbitems) + (mapc 'proof-shell-invoke-callback cbitems) (unless (or proof-action-list proof-second-action-list-active) ; release lock, cleanup @@ -1218,8 +1217,8 @@ and indentation. Assumes `proof-script-buffer' is active." (defun proof-shell-process-urgent-message (start end) "Analyse urgent message between START and END for various cases. -Cases are: *trace* output, included/retracted files, cleared -goals/response buffer, variable setting, xml-encoded PGIP response, +Cases are: *trace* output, included/retracted files, cleared +goals/response buffer, variable setting, xml-encoded PGIP response, theorem dependency message or interactive output indicator. If none of these apply, display the text between START and END. @@ -1301,11 +1300,10 @@ A subroutine of `proof-shell-process-urgent-message'." (defun proof-shell-process-urgent-message-retract (start end) "A subroutine of `proof-shell-process-urgent-message'. -Takes files off `proof-included-files-list' and calls -`proof-restart-buffers' to do the necessary clean-up on those -buffers visting a file that disappears from -`proof-included-files-list'. So in some respect this function is -inverse to `proof-register-possibly-new-processed-file'." +Take files off `proof-included-files-list' and call `proof-restart-buffers' +to do the necessary clean-up on those buffers visiting a file that disappears +from `proof-included-files-list'. So in some respect, this function is inverse +to `proof-register-possibly-new-processed-file'." (let ((current-included proof-included-files-list)) (setq proof-included-files-list (funcall proof-shell-compute-new-files-list)) @@ -1363,7 +1361,7 @@ inverse to `proof-register-possibly-new-processed-file'." ;; (defun proof-shell-strip-eager-annotations (start end) - "Strip `proof-shell-eager-annotation-{start,end}' from region." + "Strip `proof-shell-eager-annotation-{START,END}' from region." (goto-char start) (if (re-search-forward proof-shell-eager-annotation-start end nil) (setq start (point))) @@ -1407,20 +1405,20 @@ calls." (setq proof-shell-filter-active nil proof-shell-filter-was-blocked nil) (signal (car err) (cdr err)))) - (setq call-proof-shell-filter proof-shell-filter-was-blocked))))) + (setq call-proof-shell-filter proof-shell-filter-was-blocked))))) (defun proof-shell-filter () "Master 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 an -important internal function. The output must be collected from -`proof-shell-buffer' for the following reason. This function +Deal with output and issue new input from the queue. This is an +important internal function. The output must be collected from +`proof-shell-buffer' for the following reason. This function might block inside `process-send-string' when sending input to -the proof assistant or to prooftree. In this case Emacs might +the proof assistant or to prooftree. In this case Emacs might call the process filter again while the previous instance is -still running. `proof-shell-filter-wrapper' detects and delays +still running. `proof-shell-filter-wrapper' detects and delays such calls but does not buffer the output. Handle urgent messages first. As many as possible are processed, @@ -1702,7 +1700,7 @@ i.e., 'goals or 'response." (setq both (> (- gmark rstart) 4)) (if both - (proof-shell-display-output-as-response + (proof-shell-display-output-as-response flags (buffer-substring-no-properties rstart gmark))) ;; display goals output second so it persists in 2-pane mode @@ -1763,10 +1761,10 @@ Only works when system timer has microsecond count available." (> (- tm pg-last-tracing-output-time) pg-slow-mode-duration) (setq dontprint nil)) (when ;; time since last tracing output less than threshold - (and - (< (- tm pg-last-tracing-output-time) + (and + (< (- tm pg-last-tracing-output-time) (/ pg-fast-tracing-mode-threshold 1000000.0)) - (>= (incf pg-last-trace-output-count) + (>= (incf pg-last-trace-output-count) pg-slow-mode-trigger-count)) ;; quickly consecutive tracing outputs: go into slow mode (setq dontprint t) @@ -1779,7 +1777,7 @@ Only works when system timer has microsecond count available." "Handle the end of possibly voluminous tracing-style output. If the output update was slowed down, show it now." (proof-trace-buffer-finish) - (when pg-tracing-slow-mode + (when pg-tracing-slow-mode (proof-display-and-keep-buffer proof-trace-buffer) (setq pg-tracing-slow-mode nil)) (setq pg-last-trace-output-count 0)) @@ -1800,7 +1798,7 @@ If the output update was slowed down, show it now." Needed between sequences of commands to maintain synchronization, because Proof General does not allow for the action list to be extended -in some cases. Also is considerably faster than leaving the Emacs +in some cases. Also is considerably faster than leaving the Emacs top-level command loop to read from the prover. Called by `proof-shell-invisible-command' and `proof-process-buffer' @@ -1815,7 +1813,7 @@ If TIMEOUTSECS is a number, time out after that many seconds." (/ timeoutsecs accepttime)))) (when proverproc (while (and proof-shell-busy (not quit-flag) - (if timecount + (if timecount (> (setq timecount (1- timecount)) 0) t) (not (and interrupt-on-input (input-pending-p)))) @@ -1826,8 +1824,8 @@ If TIMEOUTSECS is a number, time out after that many seconds." (error "Proof General: quit in proof-shell-wait"))))) (defun proof-done-invisible (span) - "Callback for proof-shell-invisible-command. -Calls proof-state-change-hook." + "Callback for ‘proof-shell-invisible-command’. +Call ‘proof-state-change-hook’." (run-hooks 'proof-state-change-hook)) ;;;###autoload @@ -2021,7 +2019,7 @@ processing." (if (listp proof-shell-init-cmd) (mapc 'proof-shell-invisible-command-invisible-result proof-shell-init-cmd) - (proof-shell-invisible-command-invisible-result + (proof-shell-invisible-command-invisible-result proof-shell-init-cmd))) (proof-shell-wait) (if proof-assistant-settings diff --git a/generic/proof-site.el b/generic/proof-site.el index 9900aa5c..e339d022 100644 --- a/generic/proof-site.el +++ b/generic/proof-site.el @@ -156,7 +156,7 @@ You can use customize to set this variable." ;; (defun proof-add-to-load-path (dir) - "Add DIR to `load-path' if not contained already" + "Add DIR to `load-path' if not contained already." (add-to-list 'load-path dir)) (proof-add-to-load-path (concat proof-home-directory "generic/")) @@ -206,10 +206,10 @@ Each entry is a list of the form The NAME is a string, naming the proof assistant. The SYMBOL is used to form the name of the mode for the assistant, `SYMBOL-mode', run when files with AUTOMODE-REGEXP -\(or with extension FILE-EXTENSION) are visited. If present, +\(or with extension FILE-EXTENSION) are visited. If present, IGNORED-EXTENSIONS-LIST is a list of file-name extensions to be ignored when doing file-name completion (IGNORED-EXTENSIONS-LIST -is added to completion-ignored-extensions). +is added to ‘completion-ignored-extensions’). SYMBOL is also used to form the name of the directory and elisp file for the mode, which will be @@ -309,7 +309,7 @@ If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'." (mapcar (lambda (astnt) (car astnt)) proof-assistant-table)) "A list of the configured proof assistants. Set on startup to contents of environment variable PROOFGENERAL_ASSISTANTS, -the lisp variable `proof-assistants', or the contents of `proof-assistant-table'.") +the Lisp variable `proof-assistants', or the contents of `proof-assistant-table'.") ;; Add auto-loads and load-path elements to support the ;; proof assistants selected, and define stub major mode functions diff --git a/generic/proof-splash.el b/generic/proof-splash.el index daa09eff..75164890 100644 --- a/generic/proof-splash.el +++ b/generic/proof-splash.el @@ -104,7 +104,7 @@ If it is nil, a new line is inserted." "Name of the Proof General splash buffer.") (define-derived-mode proof-splash-mode fundamental-mode - "Splash" "Mode for splash. + "Splash" "Mode for splash. \\{proof-splash-mode-map}" (set-buffer-modified-p nil) (setq buffer-read-only t)) @@ -138,12 +138,12 @@ Borrowed from startup-center-spaces." (glyph-pixwidth (cond ((stringp glyph) (* avg-pixwidth (length glyph))) ((proof-emacs-imagep glyph) - (car (with-no-warnings + (car (with-no-warnings ; image-size not available in tty emacs (image-size glyph 'inpixels)))) (t (error - "proof-splash-centre-spaces: bad arg"))))) + "Function proof-splash-centre-spaces: bad arg"))))) (+ left-margin (round (/ (/ (- fill-area-width glyph-pixwidth) 2) avg-pixwidth))))) @@ -151,7 +151,7 @@ Borrowed from startup-center-spaces." ;; underneath the splash screen. This is just to be polite. ;; NB: not as polite as it could be: if minibuffer is active, ;; this may deactivate it. -;; NB2: There is something worse here: pending input +;; NB2: There is something worse here: pending input ;; causes this function to spoil the mode startup, if the splash ;; buffer is killed before the input has been processed. ;; Symptom is ProofGeneral mode instead of the native script mode. @@ -161,7 +161,7 @@ Borrowed from startup-center-spaces." "Remove splash screen and restore window config." (let ((splashbuf (get-buffer proof-splash-welcome))) (proof-splash-unset-frame-titles) - (if (and + (if (and splashbuf proof-splash-timeout-conf) (progn @@ -178,10 +178,10 @@ Borrowed from startup-center-spaces." "Remove the splash buffer if it's still present." (let ((splashbuf (get-buffer proof-splash-welcome))) - (if splashbuf + (if splashbuf ;; Kill should be right, but it can cause core dump ;; on XEmacs (kill-buffer splashbuf) (TODO: check Emacs now) - (if (eq (selected-window) (window-buffer + (if (eq (selected-window) (window-buffer (selected-window))) (bury-buffer splashbuf))))) @@ -208,7 +208,7 @@ Borrowed from startup-center-spaces." (let ((spec (car splash-contents))) (if (functionp spec) (setq spec (funcall spec))) - (indent-to (proof-splash-centre-spaces + (indent-to (proof-splash-centre-spaces (concat (car spec) (cadr spec)))) (insert (car spec)) (insert-button (cadr spec) diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el index 7af4dd06..5871a993 100644 --- a/generic/proof-syntax.el +++ b/generic/proof-syntax.el @@ -64,56 +64,56 @@ nil if a region cannot be found." ;; applicable. (defsubst proof-search-forward (string &optional bound noerror count) - "Like search-forward, but set case-fold-search to proof-case-fold-search." + "Like ‘search-forward’, but set ‘case-fold-search’ to ‘proof-case-fold-search’." (let ((case-fold-search proof-case-fold-search)) (search-forward string bound noerror count))) ;;;###autoload (defsubst proof-replace-regexp-in-string (regexp rep string) - "Like replace-regexp-in-string, but set case-fold-search to proof-case-fold-search." + "Like ‘replace-regexp-in-string’, but set ‘case-fold-search’ to ‘proof-case-fold-search’." (let ((case-fold-search proof-case-fold-search)) (replace-regexp-in-string regexp rep string))) (defsubst proof-re-search-forward (regexp &optional bound noerror count) - "Like re-search-forward, but set case-fold-search to proof-case-fold-search." + "Like ‘re-search-forward’, but set ‘case-fold-search’ to ‘proof-case-fold-search’." (let ((case-fold-search proof-case-fold-search)) (re-search-forward regexp bound noerror count))) (defsubst proof-re-search-backward (regexp &optional bound noerror count) - "Like re-search-backward, but set case-fold-search to proof-case-fold-search." + "Like ‘re-search-backward’, but set ‘case-fold-search’ to ‘proof-case-fold-search’." (let ((case-fold-search proof-case-fold-search)) (re-search-backward regexp bound noerror count))) (defsubst proof-re-search-forward-safe (regexp &optional bound noerror count) - "Like re-search-forward, but set case-fold-search to proof-case-fold-search." + "Like ‘re-search-forward’, but set ‘case-fold-search’ to ‘proof-case-fold-search’." (and regexp (let ((case-fold-search proof-case-fold-search)) (re-search-forward regexp bound noerror count)))) (defsubst proof-string-match (regexp string &optional start) - "Like string-match, but set case-fold-search to proof-case-fold-search." + "Like ‘string-match’, but set ‘case-fold-search’ to ‘proof-case-fold-search’." (let ((case-fold-search proof-case-fold-search)) (string-match regexp string start))) (defsubst proof-string-match-safe (regexp string &optional start) - "Like `string-match', but return nil if REGEXP or STRING is nil." + "Like ‘string-match’, but return nil if REGEXP or STRING is nil." (if (and regexp string) (proof-string-match regexp string start))) (defsubst proof-stringfn-match (regexp-or-fn string) - "Like proof-string-match if first arg is regexp, otherwise call it." + "Like ‘proof-string-match’ if first arg is regexp, otherwise call it." (cond ((stringp regexp-or-fn) (proof-string-match regexp-or-fn string)) ((functionp regexp-or-fn) (funcall regexp-or-fn string)))) (defsubst proof-looking-at (regexp) - "Like looking-at, but set case-fold-search to proof-case-fold-search." + "Like ‘looking-at’, but set ‘case-fold-search’ to ‘proof-case-fold-search’." (let ((case-fold-search proof-case-fold-search)) (looking-at regexp))) (defsubst proof-looking-at-safe (regexp) - "Like `proof-looking-at', but return nil if REGEXP is nil." + "Like ‘proof-looking-at’, but return nil if REGEXP is nil." (if regexp (proof-looking-at regexp))) ;; diff --git a/generic/proof-tree.el b/generic/proof-tree.el index 996934b6..cb85952d 100644 --- a/generic/proof-tree.el +++ b/generic/proof-tree.el @@ -1,4 +1,4 @@ -;;; tree-tree.el --- Proof General prooftree communication. +;;; proof-tree.el --- Proof General prooftree communication. ;; This file is part of Proof General. @@ -15,7 +15,7 @@ ;;; Commentary: ;; -;; Generic code for the communication with prooftree. Prooftree +;; Generic code for the communication with prooftree. Prooftree ;; is an ocaml-gtk program that displays proof trees. ;; ;; The main problem with proof tree visualization is that Coq (and @@ -26,20 +26,20 @@ ;; ;; To solve this problem prooftree relies on unique identification ;; strings of goals, which are called goal or sequent ID's in the -;; code. With these ID's it is easy to keep track which goals are new. +;; code. With these ID's it is easy to keep track which goals are new. ;; ;; A second problem is that, for an undo command, Coq (and probably ;; other proof assistants as well) does not tell which subgoals and -;; which finished branches must be deleted. Therefore prooftree needs +;; which finished branches must be deleted. Therefore prooftree needs ;; a continuously increasing proof state number and keeps a complete ;; undo history for every proof. ;; ;; A third problem is that Coq (and probably other proof assistants as ;; well) is not able to generate the information for a proof tree in -;; the middle of a proof. Therefore, if the user wants to start the +;; the middle of a proof. Therefore, if the user wants to start the ;; proof-tree display in the middle of the proof, it is necessary to ;; retract to the start of the proof and then to reassert to the -;; previous end of the locked region. To achieve this, one has to call +;; previous end of the locked region. To achieve this, one has to call ;; `accept-process-output' at suitable points to let Proof General ;; process the `proof-action-list'. ;; @@ -56,36 +56,36 @@ ;; ;; * To avoid synchronization trouble the communication between ;; Proof General and prooftree is almost one way only: Only Proof -;; General sends display or undo commands to Prooftree. Prooftree +;; General sends display or undo commands to Prooftree. Prooftree ;; never requests any proof-state information from Proof General. ;; Prooftree only sends a quit message to Proof General when the -;; user closes the proof-tree display of the current proof. This +;; user closes the proof-tree display of the current proof. This ;; goal requires that some of the heuristics, which decide which ;; subgoals are new and which have to be refreshed, have to be ;; implemented here. ;; -;; In general the glue code here works on the delayed output. That is, +;; In general the glue code here works on the delayed output. That is, ;; the glue code here runs when the next proof command has already -;; been sent to the proof assistant. The glue code makes a light +;; been sent to the proof assistant. The glue code makes a light ;; analysis on the output of the proof assistant, extracts the ;; necessary parts with regular expressions and sends appropriate -;; commands to prooftree. This is achieved by calling the main entry +;; commands to prooftree. This is achieved by calling the main entry ;; here, the function `proof-tree-handle-delayed-output' from the ;; proof shell filter function after `proof-shell-exec-loop' has ;; finished. ;; -;; However, some aspects can not be delayed. Those are treated by -;; `proof-tree-urgent-action'. Its primary use is for inserting +;; However, some aspects can not be delayed. Those are treated by +;; `proof-tree-urgent-action'. Its primary use is for inserting ;; special goal-displaying commands into `proof-action-list' before -;; the next real proof command runs. For Coq this needs to be done for +;; the next real proof command runs. For Coq this needs to be done for ;; newly generated subgoals and for goals that contain an existential ;; variable that got instantiated in the last proof step. ;; ;; Actually, for every proof, Prooftree can display a set of disjunct -;; proof trees, which are organized into layers. More than one proof +;; proof trees, which are organized into layers. More than one proof ;; tree in more than one layer is needed to support the Grap -;; Existential Variables command in Coq. There is one proof tree in -;; the first layer for the original goal. The second layer contains +;; Existential Variables command in Coq. There is one proof tree in +;; the first layer for the original goal. The second layer contains ;; all the goals that the first Grab Existential Variables command ;; created from uninstantiated existential variabes in the main proof. ;; The third layer contains the goals that the second Grap Existential @@ -134,8 +134,8 @@ (defcustom proof-tree-ignored-commands-regexp nil "Commands that should be ignored for the prooftree display. The output of commands matching this regular expression is not -sent to prooftree. It should match commands that display -additional information but do not make any proof progress. Leave +sent to prooftree. It should match commands that display +additional information but do not make any proof progress. Leave at nil to act on all commands. For Coq this regular expression should contain all commands such @@ -146,7 +146,7 @@ as Lemma, that can start a proof." (defcustom proof-tree-navigation-command-regexp nil "Regexp to match a navigation command. A navigation command typically focusses on a different open goal -without changing any of the open goals. Leave at nil if there are +without changing any of the open goals. Leave at nil if there are no navigation commands." :type '(choice regexp (const nil)) :group 'proof-tree-internals) @@ -155,15 +155,15 @@ no navigation commands." "Regexp to match cheating proofer commands. A cheating command finishes the current goal without proving it to permit the user to first focus on other parts of the -development. Examples are \"sorry\" in Isabelle and \"admit\" in -Coq. Leave at nil if there are no cheating commands." +development. Examples are \"sorry\" in Isabelle and \"admit\" in +Coq. Leave at nil if there are no cheating commands." :type '(choice regexp (const nil)) :group 'proof-tree-internals) (defcustom proof-tree-new-layer-command-regexp nil "Regexp to match proof commands that add new goals to a proof. This regexp must match the command that turns the proof assistant -into prover mode, which adds the initial goal to the proof. It +into prover mode, which adds the initial goal to the proof. It must further match commands that add additional goals after all previous goals have been proved." :type 'regexp @@ -172,7 +172,7 @@ previous goals have been proved." (defcustom proof-tree-current-goal-regexp nil "Regexp to match the current goal and its ID. The regexp is matched against the output of the proof assistant -to extract the current goal with its ID. The regexp must have 2 +to extract the current goal with its ID. The regexp must have 2 grouping constructs, the first one matches just the ID, the second one the complete sequent text that is to be sent to prooftree." @@ -183,9 +183,9 @@ prooftree." "Regexp to match a goal and its ID. The regexp is matched against the output of additional show-goal commands inserted by Proof General with a command returned by -`proof-tree-show-sequent-command'. Proof General inserts such -commands to update the goal text in prooftree. This is necessary, -for instance, when existential variables get instantiated. This +`proof-tree-show-sequent-command'. Proof General inserts such +commands to update the goal text in prooftree. This is necessary, +for instance, when existential variables get instantiated. This regexp must have 2 grouping constructs, the first matching the ID of the goal, the second the complete sequent text." :type 'regexp @@ -194,7 +194,7 @@ of the goal, the second the complete sequent text." (defcustom proof-tree-additional-subgoal-ID-regexp nil "Regular expression to match ID's of additional subgoals. This regexp is used to extract the ID's of all additionally open -goals. The regexp is used in a while loop and must match one +goals. The regexp is used in a while loop and must match one subgoal ID with subgroup 1." :type 'regexp :group 'proof-tree-internals) @@ -202,8 +202,8 @@ subgoal ID with subgroup 1." (defcustom proof-tree-existential-regexp nil "Regexp to match existential variables. Existential variables exist for instance in Isabelle/Hol and in -Coq. They are placeholders for terms that might (for Coq they -must) get instantiated in a later stage of the proof. This regexp +Coq. They are placeholders for terms that might (for Coq they +must) get instantiated in a later stage of the proof. This regexp should match one existential variable in subgroup 1. It is used inside a while loop to extract all existential variables from the goal text or from a list of existential variables. @@ -219,7 +219,7 @@ Together with `proof-tree-existentials-state-end-regexp', this regular expression is used to determine the state display of existential variables, which contains information about which existentials are still uninstantiated and about dependencies of -instantiated existential variables. Leave this variable nil, if +instantiated existential variables. Leave this variable nil, if there is no such state display." :type '(choice regexp (const nil)) :group 'proof-tree-internals) @@ -230,7 +230,7 @@ Together with `proof-tree-existentials-state-start-regexp', this regular expression is used to determine the state display of existential variables, which contains information about which existentials are still uninstantiated and about dependencies of -instantiated existential variables. If this variable is nil (and +instantiated existential variables. If this variable is nil (and if `proof-tree-existentials-state-start-regexp' is non-nil), then the state display expands to the end of the prover output." :type '(choice regexp (const nil)) @@ -242,29 +242,29 @@ This must match in precisely the following cases: - The current branch has been finished but there is no current open subgoal because the prover has not switched to the next subgoal. -- The last open goal has been proved. " +- The last open goal has been proved." :type 'regexp :group 'proof-tree-internals) (defcustom proof-tree-get-proof-info nil "Proof assistant specific function for information about the current proof. -This function takes no arguments. It must return a list, which +This function takes no arguments. It must return a list, which contains, in the following order: * the current state number (as positive integer) * the name of the current proof (as string) or nil -The state number is used to implement undo in prooftree. The +The state number is used to implement undo in prooftree. The proof name is used to distinguish different proofs inside prooftree. The state number is interpreted as the state that has been -reached after the last command has been processed. It must be -consistent in the following sense. Firstly, it must be strictly +reached after the last command has been processed. It must be +consistent in the following sense. Firstly, it must be strictly increasing for successive commands that can be individually -retracted. Secondly, the state number reported after some command +retracted. Secondly, the state number reported after some command X has been processed must be strictly greater than the state -reported when X is retracted. Finally, state numbers of commands +reported when X is retracted. Finally, state numbers of commands preceding X must be less than or equal the state reported when X is retracted (but no stuff before X)." :type 'function @@ -277,7 +277,7 @@ variables, that is, if `proof-tree-existential-regexp' is non-nil. If defined, this function should return the list of currently -instantiated existential variables as a list of strings. The +instantiated existential variables as a list of strings. The function is called with `proof-shell-buffer' as current buffer and with two arguments start and stop, which designate the region containing the last output from the proof assistant. @@ -291,7 +291,7 @@ function." "Proof assistant specific function for a show-goal command. This function is applied to an ID of a goal and should return a command (as string) that will display the complete sequent with -that ID. The regexp `proof-tree-update-goal-regexp' should match +that ID. The regexp `proof-tree-update-goal-regexp' should match the output of the proof assistant for the returned command, such that `proof-tree-update-sequent' will update the sequent ID inside prooftree. @@ -304,11 +304,11 @@ function should return nil and prooftree will not get updated." (defcustom proof-tree-find-begin-of-unfinished-proof nil "Proof assistant specific function for the start of the current proof. This function is called with no argument when the user switches -the external proof-tree display on. Then, this function must +the external proof-tree display on. Then, this function must determine if there is a currently unfinished proof for which the -proof-tree display should be started. If yes this function must +proof-tree display should be started. If yes this function must return the starting position of the command that started this -proof. If there is no such proof, this function must return nil." +proof. If there is no such proof, this function must return nil." :type 'function :group 'proof-tree-internals) @@ -316,8 +316,8 @@ proof. If there is no such proof, this function must return nil." "Proof assistant specific function for finding the point to undo to. This function is used to convert the state number, which comes with an undo command from Prooftree, into a point position for -`proof-retract-until-point'. This function is called in the -current scripting buffer with the state number as argument. It +`proof-retract-until-point'. This function is called in the +current scripting buffer with the state number as argument. It must return a buffer position." :type 'function :group 'proof-tree-internals) @@ -327,7 +327,7 @@ must return a buffer position." This hook is called (indirectly) from inside `proof-shell-exec-loop' after the preceeding command and any comments that follow have been choped off `proof-action-list' and -before the next command is sent to the proof assistant. This hook +before the next command is sent to the proof assistant. This hook can therefore be used to insert additional commands into `proof-action-list' that must be executed before the next real proof command. @@ -336,7 +336,7 @@ Functions in this hook can rely on `proof-info' being bound to the result of `proof-tree-get-proof-info'. This hook is used, for instance, for Coq to insert Show commands -for newly generated subgoals. (The normal Coq output does not +for newly generated subgoals. (The normal Coq output does not contain the complete sequent text of newly generated subgoals.)" :type 'hook :group 'proof-tree-internals) @@ -349,19 +349,19 @@ contain the complete sequent text of newly generated subgoals.)" (defvar proof-tree-external-display nil "Display proof trees in external prooftree windows if t. Actually, if this variable is t then the user requested an -external proof-tree display. If there was no unfinished proof +external proof-tree display. If there was no unfinished proof when proof-tree display was requested and if no proof has been started since then, then there is obviously no proof-tree -display. In this case, this variable stays t and the proof-tree +display. In this case, this variable stays t and the proof-tree display will be started for the next proof. Controlled by `proof-tree-external-display-toggle'.") (defvar proof-tree-process nil - "Emacs lisp process object of the prooftree process.") + "Emacs Lisp process object of the prooftree process.") (defconst proof-tree-process-name "proof-tree" - "Name of the prooftree process for Emacs lisp.") + "Name of the prooftree process for Emacs Lisp.") (defconst proof-tree-process-buffer-name (concat "*" proof-tree-process-name "*") @@ -387,13 +387,13 @@ This variable is only maintained and meaningful if "Hash table to remember sequent ID's. Needed because some proof assistants do not distinguish between new subgoals, which have been created by the last proof command, -and older, currently unfocussed subgoals. If Proof General meets +and older, currently unfocussed subgoals. If Proof General meets a goal, it is treated as new subgoal if it is not in this hash yet. -The hash is mostly used as a set of sequent ID's. However, for +The hash is mostly used as a set of sequent ID's. However, for undo operations it is necessary to delete all those sequents from the hash that have been created in a state later than the undo -state. For this purpose this hash maps sequent ID's to the state +state. For this purpose this hash maps sequent ID's to the state number in which the sequent has been created. The hash table is initialized in `proof-tree-start-process'.") @@ -401,9 +401,9 @@ The hash table is initialized in `proof-tree-start-process'.") (defvar proof-tree-existentials-alist nil "Alist mapping existential variables to sequent ID's. Used to remember which goals need a refresh when an existential -variable gets instantiated. To support undo commands the old +variable gets instantiated. To support undo commands the old contents of this list must be stored in -`proof-tree-existentials-alist-history'. To ensure undo is +`proof-tree-existentials-alist-history'. To ensure undo is properly working, this variable should only be changed by using `proof-tree-delete-existential-assoc', `proof-tree-add-existential-assoc' or @@ -425,7 +425,7 @@ This marker points to the next piece of output that needs to get processed.") (defvar proof-tree-filter-continuation nil "Continuation when `proof-tree-process-filter' stops early. A function that handles a command from Prooftee might fail -because not all data from Prooftee has yet arrived. In this case +because not all data from Prooftee has yet arrived. In this case the continuation is stored in this variable and will be called from `proof-tree-process-filter' when more output arrives.") @@ -450,7 +450,7 @@ from `proof-tree-process-filter' when more output arrives.") (defun proof-tree-insert-script (data) "Handle an insert-command command from Prooftree." - (let ((command-length (string-to-number data))) + (let ((command-length (string-to-number data))) (if (and (integerp command-length) (> command-length 0)) (condition-case nil (progn @@ -768,13 +768,13 @@ state PROOF-STATE." 'proof-tree-existentials-alist-history)) (defun proof-tree-delete-existential-assoc (state ex-assoc) - "Delete mapping EX-ASSOC from 'proof-tree-existentials-alist'." + "Delete mapping EX-ASSOC from ‘proof-tree-existentials-alist’." (proof-tree-record-existentials-state state) (setq proof-tree-existentials-alist (delq ex-assoc proof-tree-existentials-alist))) (defun proof-tree-add-existential-assoc (state ex-var sequent-id) - "Add the mapping EX-VAR -> SEQUENT-ID to 'proof-tree-existentials-alist'. + "Add the mapping EX-VAR -> SEQUENT-ID to ‘proof-tree-existentials-alist’. Do nothing if this mapping does already exist." (let ((ex-var-assoc (assoc ex-var proof-tree-existentials-alist))) (if ex-var-assoc @@ -830,7 +830,7 @@ the current output does not come from a command (with the Urgent actions are only needed if the external proof display is currently running. Therefore this function should not be called -when `proof-tree-external-display' is nil. +when `proof-tree-external-display' is nil. This function assumes that the prover output is not suppressed. Therefore, `proof-tree-external-display' being t is actually a @@ -1073,8 +1073,8 @@ Send the undo command to prooftree and undo changes to the internal state of this package. The latter involves currently two points: * delete those goals from `proof-tree-sequent-hash' that have - been generated after the state to which we undo now -* change proof-tree-existentials-alist back to its previous content" + been generated after the state to which we undo now; +* change proof-tree-existentials-alist back to its previous content." ;; (message "PTHU info %s" proof-info) (let ((proof-state (car proof-info))) ;; delete sequents from the hash @@ -1103,11 +1103,11 @@ points: "Prepare an update-sequent command for prooftree. This function processes delayed output that the proof assistant generated in response to commands that Proof General inserted in -order to keep prooftree up-to-date. Such commands are tagged with +order to keep prooftree up-to-date. Such commands are tagged with a 'proof-tree-show-subgoal flag. This function uses `proof-tree-update-goal-regexp' to find a -sequent and its ID in the delayed output. If something is found +sequent and its ID in the delayed output. If something is found an appropriate update-sequent command is sent to prooftree. The update-sequent command is associated with state PROOF-STATE @@ -1143,7 +1143,7 @@ The delayed output is in the region (defun proof-tree-handle-delayed-output (old-proof-marker cmd flags span) "Process delayed output for prooftree. This function is the main entry point of the Proof General -prooftree support. It examines the delayed output in order to +prooftree support. It examines the delayed output in order to take appropriate actions and maintains the internal state. The delayed output to handle is in the region @@ -1153,7 +1153,7 @@ which contains the position of `proof-marker', before the next command was sent to the proof assistant. All other arguments are (former) fields of the `proof-action-list' -entry that is now finally retired. CMD is the command, FLAGS are +entry that is now finally retired. CMD is the command, FLAGS are the flags and SPAN is the span." ;; (message "PTHDO cmd %s flags %s span %s-%s" cmd flags ;; (if span (span-start span)) (if span (span-end span))) @@ -1215,10 +1215,10 @@ the flags and SPAN is the span." (defun proof-tree-display-current-proof (proof-start) "Start an external proof-tree display for the current proof. Coq (and probably other proof assistants as well) does not -support outputing the current proof tree. Therefore this function +support outputing the current proof tree. Therefore this function retracts to the start of the current proof, switches the proof-tree display on, and reasserts then until the former end of -the locked region. Argument PROOF-START must contain the start +the locked region. Argument PROOF-START must contain the start position of the current proof." ;;(message "PTDCP %s" proof-tree-external-display) (unless (and proof-script-buffer @@ -1247,10 +1247,10 @@ position of the current proof." (defun proof-tree-external-display-toggle () "Toggle the external proof-tree display. When called outside a proof the external proof-tree display will -be enabled for the next proof. When called inside a proof the -proof display will be created for the current proof. If the +be enabled for the next proof. When called inside a proof the +proof display will be created for the current proof. If the external proof-tree display is currently on, then this toggle -will switch it off. At the end of the proof the proof-tree +will switch it off. At the end of the proof the proof-tree display is switched off." (interactive) (unless proof-tree-configured @@ -1287,4 +1287,4 @@ display is switched off." (provide 'proof-tree) -;;; tree-tree.el ends here +;;; proof-tree.el ends here diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el index b1d8e2e4..9a60e0ac 100644 --- a/generic/proof-useropts.el +++ b/generic/proof-useropts.el @@ -192,7 +192,7 @@ and displayed lazily. See `proof-layout-windows'." and goal and response buffers on the left (one above the other). - If 'smart or anything else: 'horizontal when the window - is wide enough and 'vertical otherwise. The width threshold + is wide enough and 'vertical otherwise. The width threshold is given by `split-width-threshold'. See `proof-layout-windows'." @@ -362,8 +362,8 @@ locked (coloured blue); a buffer is completely unprocessed when there is no locked region. For some proof assistants (such as Coq) fully processed buffers make -no sense. Setting this option to 'process has then the same effect -as leaving it unset (nil). (This behaviour is controlled by +no sense. Setting this option to 'process has then the same effect +as leaving it unset (nil). (This behaviour is controlled by `proof-no-fully-processed-buffer'.)" :type '(choice (const :tag "No automatic action; query user" nil) @@ -408,7 +408,7 @@ Hovers will be added when this option is non-nil. Prover outputs can be displayed when the mouse hovers over the region that produced it and output is available (see `proof-full-annotation'). If output is not available, the type of the output region is displayed. -Changes of this option will not be reflected in already-processed +Changes of this option will not be reflected in already-processed regions of the script." :type 'boolean :group 'proof-user-options) @@ -438,7 +438,7 @@ are distracting or too frequent." :type 'boolean :group 'proof-user-options) -(defcustom proof-fast-process-buffer +(defcustom proof-fast-process-buffer (or (featurep 'ns) ; Mac OS X ; or Windows (speed up TBC, see Trac #308) (memq system-type '(windows-nt ms-dos cygwin))) diff --git a/generic/proof-utils.el b/generic/proof-utils.el index 575a76ee..4a0ca857 100644 --- a/generic/proof-utils.el +++ b/generic/proof-utils.el @@ -66,7 +66,7 @@ ;; (defmacro proof-with-current-buffer-if-exists (buf &rest body) - "As with-current-buffer if BUF exists and is live, otherwise nothing." + "Like ‘with-current-buffer’ if BUF exists and is live, otherwise nothing." `(if (buffer-live-p ,buf) (with-current-buffer ,buf ,@body))) @@ -75,7 +75,7 @@ ;; which work from different PG buffers (goals, response), typically ;; bound to toolbar commands. (defmacro proof-with-script-buffer (&rest body) - "Execute BODY in some script buffer: current buf or otherwise proof-script-buffer. + "Execute BODY in some script buffer: current buf, else ‘proof-script-buffer’. Return nil if not a script buffer or if no active scripting buffer." `(cond ((eq proof-buffer-type 'script) @@ -86,7 +86,7 @@ Return nil if not a script buffer or if no active scripting buffer." ,@body)))) (defmacro proof-map-buffers (buflist &rest body) - "Do BODY on each buffer in BUFLIST, if it exists." + "Eval BODY on each buffer in BUFLIST, if it exists." `(dolist (buf ,buflist) (proof-with-current-buffer-if-exists buf ,@body))) @@ -187,9 +187,9 @@ user accidently killing an associated buffer." ;; Key functions (defun proof-define-keys (map kbl) - "Adds keybindings KBL in MAP. -The argument KBL is a list of tuples (k . f) where `k' is a keybinding -\(vector) and `f' the designated function." + "Add in MAP the keybindings KBL. +The argument KBL is a list of tuples (K . F) where K is a keybinding +\(vector) and F the designated function." (mapcar (lambda (kbl) (let ((k (car kbl)) (f (cdr kbl))) @@ -230,21 +230,21 @@ Leave point at END." (defvar proof-advertise-layout-freq 30 "Frequency for PG messages to be displayed from time to time.") (defvar proof-advertise-layout-count proof-advertise-layout-freq - "counter used to display PG messages from time to time.") + "Counter used to display PG messages from time to time.") (defun proof-get-window-for-buffer (buffer) "Find a window for BUFFER, display it there, return the window. -NB: may change the selected window. This function is a wrapper on -display-buffer. The idea is that if the user has opened and +NB: may change the selected window. This function is a wrapper on +‘display-buffer’. The idea is that if the user has opened and closed some windows we want to preserve the layout by only -switching buffer in already pg-associate windows. So if the +switching buffer in already pg-associate windows. So if the buffer is not already displayed, we try to reuse an existing -associated window, even if in 3-win mode. If no such window -exists, we fall back to display-buffer while protecting script +associated window, even if in 3-win mode. If no such window +exists, we fall back to ‘display-buffer’ while protecting script buffer to be hidden or split. Experimentally we display a message from time to time advertising -C-c C-l." +\\[proof-layout-windows]." ;; IF there *isn't* a visible window showing buffer... (unless (get-buffer-window buffer 0) (if proof-three-window-enable @@ -323,7 +323,7 @@ Ensure that point is visible in window." (kill-local-variable 'mode-line-format)))))))))))) (defun proof-clean-buffer (buffer) - "Erase buffer and hide from display if proof-delete-empty-windows set. + "Erase BUFFER and hide from display if ‘proof-delete-empty-windows’ set. Auto deletion only affects selected frame. (We assume that the selected frame is the one showing the script buffer.) No effect if buffer is dead." @@ -699,9 +699,10 @@ KEY is added onto proof assistant map." ;; (defun proof-locate-executable (progname &optional returnnopath extrapath) - "Search for PROGNAME on environment PATH. Return the full path to PROGNAME, or nil. + "Search for PROGNAME on environment PATH. +Return the full path to PROGNAME, or nil. If RETURNNOPATH is non-nil, return PROGNAME even if we can't find a full path. -EXTRAPATH is a list of extra path components" +EXTRAPATH is a list of extra path components." (or (let ((exec-path (append exec-path extrapath))) (executable-find progname)) diff --git a/lib/bufhist.el b/lib/bufhist.el index 4c24ca42..65d33cc5 100644 --- a/lib/bufhist.el +++ b/lib/bufhist.el @@ -186,7 +186,8 @@ This is as a pair (POINT . CONTENTS)." (bufhist-insert-buttons)) (defun bufhist-checkpoint-and-erase () - "Add buffer contents to history then erase. Only erase if not in bufhist mode" + "Add buffer contents to history then erase. +Only erase if not in bufhist mode." (interactive) (bufhist-checkpoint) (bufhist-erase-buffer)) @@ -241,7 +242,8 @@ If optional NOSAVE is non-nil, do not try to save current contents." (bufhist-switch-to-index 0 nil 'browsing)) (defun bufhist-prev (&optional n) - "Browse backward in the history of buffer contents." + "Browse backward in the history of buffer contents. +If N is omitted or nil, move backward by one item." (interactive "p") (bufhist-switch-to-index (mod (+ bufhist-ring-pos (or n 1)) @@ -249,7 +251,8 @@ If optional NOSAVE is non-nil, do not try to save current contents." nil 'browsing)) (defun bufhist-next (&optional n) - "Browse forward in the history of buffer contents." + "Browse forward in the history of buffer contents. +If N is omitted or nil, move forward by one item." (interactive "p") (bufhist-prev (- (or n 1)))) @@ -284,7 +287,7 @@ If optional NOSAVE is non-nil, do not try to save current contents." "Initialise a ring history for the current buffer. The history will be read-only unless READWRITE is non-nil. For read-only histories, edits to the buffer switch to the latest version. -The size defaults to `bufhist-ring-size'." +If RINGSIZE is omitted or nil, the size defaults to ‘bufhist-ring-size’." (interactive) (setq bufhist-ring (make-ring (or ringsize bufhist-ring-size))) (setq bufhist-normal-read-only buffer-read-only) @@ -370,3 +373,4 @@ The size defaults to `bufhist-ring-size'." (setq bufhist-top-point (point)))))) (provide 'bufhist) +;;; bufhist.el ends here diff --git a/lib/holes.el b/lib/holes.el index 2b154723..9a45037c 100644 --- a/lib/holes.el +++ b/lib/holes.el @@ -42,7 +42,7 @@ ;;; initialization ;;; -(defvar holes-default-hole +(defvar holes-default-hole (let ((ol (make-overlay 0 0))) (delete-overlay ol) ol) "An empty detached hole used as the default hole. @@ -78,7 +78,7 @@ which should be removed when making the text into a hole." ;(defcustom holes-search-limit 1000 -; "Number of chars to look forward when looking for the next hole, unused for now.") +; "Number of chars to look forward when looking for the next hole, unused for now.") ;unused for the moment ;; The following is customizable by a command of the form: @@ -121,18 +121,18 @@ which should be removed when making the text into a hole." (define-key map [(mouse-2)] 'holes-mouse-forget-hole) map) "Keymap to use on the holes's overlays. -This keymap is used only when point is on a hole. +This keymap is used only when point is on a hole. See `holes-mode-map' for the keymap of `holes-mode'.") (defvar holes-mode-map (let ((map (make-sparse-keymap))) (define-key map [(control c) (h)] 'holes-set-make-active-hole) (define-key map [(control c) (control y)] 'holes-replace-update-active-hole) - (define-key map [(control meta down-mouse-1)] + (define-key map [(control meta down-mouse-1)] 'holes-mouse-set-make-active-hole) - (define-key map [(control meta shift down-mouse-1)] + (define-key map [(control meta shift down-mouse-1)] 'holes-mouse-replace-active-hole) - (define-key map [(control c) (control j)] + (define-key map [(control c) (control j)] 'holes-set-point-next-hole-destroy) map) "Keymap of `holes-mode'. @@ -190,7 +190,7 @@ This is not the keymap used on holes's overlay (see `hole-map' instead).") (defun holes-hole-start-position (hole) "Return start position of HOLE." - (assert (holes-is-hole-p hole) t + (assert (holes-is-hole-p hole) t "holes-hole-start-position: %s is not a hole") (span-start hole)) @@ -285,7 +285,7 @@ the active hole is already disable." Error if HOLE is not a hole." (assert (holes-is-hole-p hole) t "holes-set-active-hole: %s is not a hole") - (if (holes-active-hole-exist-p) + (if (holes-active-hole-exist-p) (holes-highlight-hole holes-active-hole)) (setq holes-active-hole hole) (holes-highlight-hole-as-active holes-active-hole)) @@ -330,7 +330,7 @@ the span." "Clear the HOLE." (assert (holes-is-hole-p hole) t "holes-clear-hole: %s is not a hole") - (if (and (holes-active-hole-exist-p) + (if (and (holes-active-hole-exist-p) (eq holes-active-hole hole)) (holes-disable-active-hole)) (span-delete hole)) @@ -343,9 +343,10 @@ the span." (holes-clear-hole (holes-hole-at (or pos (point))))) -(defun holes-map-holes (function &optional object from to) - "Map function FUNCTION across holes." - (fold-spans function object from to nil nil 'hole)) +(defun holes-map-holes (function &optional buffer from to) + "Map function FUNCTION across holes in buffer BUFFER. +Operate between character positions FROM and TO." + (fold-spans function buffer from to nil nil 'hole)) (defun holes-clear-all-buffer-holes (&optional start end) "Clear all holes leaving their contents. @@ -353,7 +354,7 @@ Operate betwenn START and END if non nil." (interactive) (holes-disable-active-hole) (span-mapcar-spans - 'holes-clear-hole (or start (point-min)) (or end (point-max)) + 'holes-clear-hole (or start (point-min)) (or end (point-max)) 'hole)) ;; limit ? @@ -361,7 +362,7 @@ Operate betwenn START and END if non nil." "Return the first hole after POS in BUFFER. Or after the hole at pos if there is one (default pos=point). If no hole found, return nil." - (holes-map-holes + (holes-map-holes (lambda (h x) (and (holes-is-hole-p h) h)) buffer pos)) (defun holes-next-after-active-hole () @@ -391,7 +392,8 @@ Default pos = point and buffer = current." (defun holes-replace-segment (start end str &optional buffer) - "Erase chars between START and END, and replace them with STR." + "Erase chars between START and END, and replace them with STR. +Operate in buffer BUFFER." (with-current-buffer (or buffer (current-buffer)) (goto-char end) ;; Insert before deleting, so the markers at `start' and `end' @@ -445,9 +447,9 @@ following hole if it exists." (let ((nxthole (holes-next-after-active-hole))) (holes-replace-active-hole (or str - (and mark-active + (and mark-active (holes-copy-active-region)) - (current-kill 0) + (current-kill 0) (error "Nothing to put in hole"))) (if nxthole (holes-set-active-hole nxthole) (setq holes-active-hole holes-default-hole))))) @@ -477,7 +479,7 @@ Sets `holes-active-hole' to the next hole if it exists." (defalias 'holes-track-mouse-selection 'mouse-drag-track) (defsubst holes-track-mouse-clicks () - "See `mouse-track-click-count'" + "See `mouse-track-click-count'." (+ mouse-selection-click-count 1)) (defun holes-mouse-replace-active-hole (event) @@ -497,7 +499,7 @@ Sets `holes-active-hole' to the next hole if it exists." (defun holes-destroy-hole (&optional span) "Destroy the hole SPAN." (interactive) - (let* ((sp (or span (holes-hole-at (point)) + (let* ((sp (or span (holes-hole-at (point)) (error "No hole to destroy")))) (save-excursion (if (and (holes-active-hole-exist-p) @@ -555,7 +557,7 @@ Sets `holes-active-hole' to the next hole if it exists." (defun holes-set-point-next-hole-destroy () - "Moves the point to current active hole (if any and if in current buffer). + "Move the point to current active hole (if any and if in current buffer). Destroy it and makes the next hole active if any." (interactive) (assert (holes-active-hole-exist-p) nil "no active hole") @@ -583,7 +585,10 @@ Destroy it and makes the next hole active if any." (defun holes-replace-string-by-holes-backward (limit) "Change each occurrence of REGEXP into a hole. Sets the active hole to the last created hole and unsets it if no hole is -created. Return the number of holes created." +created. Return the number of holes created. +The LIMIT argument bounds the search; it is a buffer position. + The match found must not begin before that position. A value of nil + means search to the beginning of the accessible portion of the buffer." (holes-disable-active-hole) (let ((n 0)) (save-excursion @@ -615,9 +620,9 @@ created. Return the number of holes created." (defun holes-replace-string-by-holes-backward-jump (pos &optional noindent alwaysjump) "Put holes between POS and point, backward, indenting. -\"#\" and \"@{..}\" between this positions will become holes. If -ALWAYSJUMP is non nil, jump to the first hole even if more than -one." +\"#\" and \"@{..}\" between this positions will become holes. +If NOINDENT is non-nil, skip the indenting step. +If ALWAYSJUMP is non-nil, jump to the first hole even if more than one." (unless noindent (save-excursion (indent-region pos (point) nil))) (let ((n (holes-replace-string-by-holes-backward pos))) (case n @@ -634,7 +639,7 @@ one." ;;;###autoload -(define-minor-mode holes-mode +(define-minor-mode holes-mode "Toggle Holes minor mode. With arg, turn Outline minor mode on if arg is positive, off otherwise. diff --git a/lib/local-vars-list.el b/lib/local-vars-list.el index bcea270f..4d737d73 100644 --- a/lib/local-vars-list.el +++ b/lib/local-vars-list.el @@ -34,9 +34,9 @@ (defconst local-vars-list-doc nil "From Emacs Info: -A file can contain a \"local variables list\", which specifies the values to use for -certain Emacs variables when that file is edited. See info node \"(emacs)File -Variables\". +A file can contain a \"local variables list\", which specifies the values to use +for certain Emacs variables when that file is edited. +See info node \"(emacs)File Variables\". local-vars-list provides two useful functions: @@ -111,7 +111,7 @@ variable definition (or at the \"End:\" line)." (read (buffer-substring boexp (point))))))) ; TODO: catch errors here? -;; Only looks for file local vars. Not dir local vars. +;; Only looks for file local vars. Not dir local vars. (defun local-vars-list-get (symb) "Return the value written in the local variable list for variable symb. Raises an error if symb is not in the list. @@ -122,14 +122,14 @@ alist. Proceed by looking in the file instead." (save-excursion (let* ((lrpat (local-vars-list-find)) - (dummy (if lrpat t (error "local variables zone not found. "))) + (dummy (if lrpat t (error "Local variables zone not found"))) (lpat (car lrpat)) (rpat (car (cdr lrpat))) ) (beginning-of-line) (if (local-vars-list-goto-var symb lpat rpat) t - (error "variable %s not found" symb)) + (error "Variable %s not found" symb)) (beginning-of-line) (local-vars-list-get-current lpat rpat)))) @@ -154,3 +154,6 @@ of the buffer first." ;;; fill-column: 85 *** ;;; indent-tabs-mode: nil *** ;;; End: *** + +(provide 'local-vars-list) +;;; local-vars-list.el ends here diff --git a/lib/maths-menu.el b/lib/maths-menu.el index a6b64201..32911a35 100644 --- a/lib/maths-menu.el +++ b/lib/maths-menu.el @@ -56,7 +56,7 @@ ;;; Code: (defvar maths-menu-filter-predicate (lambda (char) t) - "Predicate function used to filter menu elements") + "Predicate function used to filter menu elements.") (defvar maths-menu-tokenise-insert #'insert "Function used to insert possibly formatted or escaped character.") diff --git a/lib/pg-dev.el b/lib/pg-dev.el index 79afca23..8e82a753 100644 --- a/lib/pg-dev.el +++ b/lib/pg-dev.el @@ -114,7 +114,7 @@ pg-thymodes pg-autotest ;; isar-syntax isar-find-theorems isar-unicode-tokens - isar-autotest interface-setup isabelle-system isar + isar-autotest interface-setup isabelle-system isar isar-keywords ;; coq-abbrev coq-db coq-unicode-tokens coq-local-vars coq coq-syntax @@ -130,7 +130,7 @@ ;;;###autoload (defun profile-pg () - "Configure Proof General for profiling. Use M-x elp-results to see results." + "Configure Proof General for profiling. Use \\[elp-results] to see results." (interactive) (elp-instrument-package "proof-") (elp-instrument-package "pg-") @@ -142,10 +142,10 @@ (elp-instrument-package "replace-") ; for replace-regexp etc (elp-instrument-package "re-search-") ; for re-search-forwad etc (elp-instrument-package "skip-chars-") ; for skip chars etc - (elp-instrument-list + (elp-instrument-list '(string-match match-string re-search-forward re-search-backward skip-chars-forward skip-chars-backward - goto-char insert + goto-char insert set-marker marker-position nreverse nconc mapc member @@ -153,7 +153,7 @@ sit-for overlay-put overlay-start overlay-end make-overlay buffer-live-p kill-buffer - process-status get-buffer-process + process-status get-buffer-process delete-overlay move-overlay accept-process-output)) (elp-instrument-package "font-lock")) diff --git a/lib/proof-compat.el b/lib/proof-compat.el index 4c1fa5b2..abbdb465 100644 --- a/lib/proof-compat.el +++ b/lib/proof-compat.el @@ -141,6 +141,5 @@ The value returned is the value of the last form in BODY." (if (and (symbolp this-command) (get this-command 'completion-function)) (funcall (get this-command 'completion-function))))) - -;; End of proof-compat.el (provide 'proof-compat) +;;; proof-compat.el ends here diff --git a/lib/scomint.el b/lib/scomint.el index 3644add2..8f7104e8 100644 --- a/lib/scomint.el +++ b/lib/scomint.el @@ -88,7 +88,7 @@ a TCP connection to be opened via `open-network-stream'. If there is already a running process in that buffer, it is not restarted. Optional fourth arg STARTFILE is the name of a file to send the contents of to the process. -If PROGRAM is a string, any more args are arguments to PROGRAM." +If PROGRAM is a string, the remaining SWITCHES are arguments to PROGRAM." (unless (or (fboundp 'start-process) (fboundp 'start-file-process)) (error "Multi-processing is not supported for this system")) @@ -112,13 +112,14 @@ a TCP connection to be opened via `open-network-stream'. If there is already a running process in that buffer, it is not restarted. Optional third arg STARTFILE is the name of a file to send the contents of the process to. -If PROGRAM is a string, any more args are arguments to PROGRAM." +If PROGRAM is a string, the remaining SWITCHES are arguments to PROGRAM." (apply #'scomint-make-in-buffer name nil program startfile switches)) (defun scomint-exec (buffer name command startfile switches) - "Start up a process named NAME in buffer BUFFER for Comint modes. -Runs the given COMMAND with SWITCHES with output to STARTFILE. + "In buffer BUFFER, start up a process named NAME for Comint modes. +Runs the given COMMAND with output to STARTFILE. +SWITCHES contains the arguments passed to the COMMAND. Blasts any old process running in the buffer. Doesn't set the buffer mode. You can use this to cheaply run a series of processes in the same Comint buffer. The hook `scomint-exec-hook' is run after each exec." diff --git a/lib/span.el b/lib/span.el index 2252d605..e7e3d68b 100644 --- a/lib/span.el +++ b/lib/span.el @@ -39,7 +39,7 @@ (defalias 'span-buffer 'overlay-buffer) (defun span-p (ol) - "Check if an overlay belongs to PG." + "Check if an overlay OL belongs to PG." (overlay-get ol 'pg-span)) (defun span-read-only-hook (overlay after start end &optional len) @@ -119,7 +119,7 @@ (defun span-mapcar-spans-inorder (fn start end prop) "Map function FN over spans between START and END with property PROP." - (mapcar fn + (mapcar fn (sort (spans-at-region-prop start end prop) 'span-lt))) @@ -165,7 +165,7 @@ A span is before PT if it begins before the character before PT." (defun span-string (span) (with-current-buffer (overlay-buffer span) - (buffer-substring-no-properties + (buffer-substring-no-properties (overlay-start span) (overlay-end span)))) (defun set-span-properties (span plist) @@ -212,7 +212,8 @@ A span is before PT if it begins before the character before PT." (span-mapc-spans 'span-delete start end prop)) (defun span-property-safe (span name) - "Like span-property, but return nil if SPAN is nil." + "Get the property of span SPAN with property name NAME. +Like ‘span-property’, but return nil if SPAN is nil." (and span (span-property span name))) (defun span-set-start (span value) diff --git a/lib/texi-docstring-magic.el b/lib/texi-docstring-magic.el index 93896209..e39ee51a 100644 --- a/lib/texi-docstring-magic.el +++ b/lib/texi-docstring-magic.el @@ -96,7 +96,10 @@ (require 'cl)) (defun texi-docstring-magic-find-face (face) - ;; Compatibility between FSF Emacs and XEmacs + "Return non-nil if FACE is a face name; nil otherwise. +A face name can be a string or a symbol. + +Compatibility between FSF Emacs and XEmacs." (or (facep face) (and (fboundp 'find-face) (find-face face)))) @@ -202,13 +205,14 @@ including any whitespace included to delimit matches.") (defun texi-docstring-magic-untabify (string) "Convert tabs in STRING into multiple spaces." - (with-temp-buffer + (with-temp-buffer (insert string) (untabify (point-min) (point-max)) (buffer-string))) (defun texi-docstring-magic-munge-docstring (docstring args) "Markup DOCSTRING for texi according to regexp matches." + ;; FIXME(EMD): seems buggy as ARGS is not used (let ((case-fold-search nil)) (setq docstring (texi-docstring-magic-untabify docstring)) (dolist (test texi-docstring-magic-munge-table) @@ -261,7 +265,7 @@ including any whitespace included to delimit matches.") (defun texi-docstring-magic-format-default (default) "Make a default value string for the value DEFAULT. -Markup as @code{stuff} or @lisp stuff @end lisp." +Markup as @code{stuff} or @lisp stuff @end Lisp." ;; NB: might be nice to use a 'default-value-description ;; property here, in case the default value is computed. (let ((text (format "%S" default))) @@ -409,3 +413,7 @@ With prefix arg, no errors on unknown symbols. (This results in (provide 'texi-docstring-magic) + +(provide 'texi-docstring-magic) + +;;; texi-docstring-magic.el ends here diff --git a/lib/unicode-chars.el b/lib/unicode-chars.el index 880371ce..2b854739 100644 --- a/lib/unicode-chars.el +++ b/lib/unicode-chars.el @@ -5063,7 +5063,7 @@ (defun unicode-chars-list-chars () "Insert each Unicode character into a buffer. Lets you see which characters are available for literal display -in your emacs font." +in your Emacs font." (interactive) (pop-to-buffer "*unicode-chars*") (let ((chars unicode-chars-alist) @@ -5081,3 +5081,4 @@ in your emacs font." (insert (format " %s\n" name))))))) (provide 'unicode-chars) +;;; unicode-chars.el ends here diff --git a/lib/unicode-tokens.el b/lib/unicode-tokens.el index e98ca0a2..4d1d0d35 100644 --- a/lib/unicode-tokens.el +++ b/lib/unicode-tokens.el @@ -67,6 +67,7 @@ :group 'unicode-tokens-options) (defun unicode-tokens-toggle-add-help-echo () + "Toggle option ‘unicode-tokens-add-help-echo’." (interactive) (customize-set-variable 'unicode-tokens-add-help-echo (not unicode-tokens-add-help-echo)) @@ -264,7 +265,7 @@ This is used for an approximate reverse mapping, see `unicode-tokens-paste'.") ;; (defconst unicode-tokens-font-family-alternatives '(("STIXGeneral" - "DejaVu Sans Mono" "DejaVuLGC Sans Mono" + "DejaVu Sans Mono" "DejaVuLGC Sans Mono" "Lucida Grande" "Lucida Sans Unicode" "Apple Symbols") ("Script" "Lucida Calligraphy" "URW Chancery L" "Zapf Chancery") @@ -869,7 +870,7 @@ Starts from point." (regexp-opt (mapcar 'car unicode-tokens-shortcut-replacement-alist)))) ;; override the display of the regexp because it's huge! ;; (doesn't help with C-h: need way to programmatically show string) - (cl-flet ((query-replace-descr (str) + (cl-flet ((query-replace-descr (str) (if (eq str shortcut-regexp) "shortcut" str))) (perform-replace shortcut-regexp (cons 'unicode-tokens-replace-shortcut-match nil) @@ -883,7 +884,7 @@ Starts from point." (format unicode-tokens-token-format token))))) (defun unicode-tokens-replace-unicode () - "Query-replace unicode sequences in the buffer with tokens having same appearance. + "Query-replace unicode seq. in the buffer with tokens having same appearance. Starts from point." (interactive) (let ((uchar-regexp unicode-tokens-uchar-regexp)) @@ -972,7 +973,7 @@ Starts from point." (defalias 'unicode-tokens-list-unicode-chars 'unicode-chars-list-chars) (defun unicode-tokens-encode-in-temp-buffer (str fn) - "Call FN on encoded version of STR." + "Compute an encoded version of STR and call FN onto." (with-temp-buffer (insert str) (goto-char (point-min)) diff --git a/pghaskell/pghaskell.el b/pghaskell/pghaskell.el index 7784cf0f..88dd44bc 100644 --- a/pghaskell/pghaskell.el +++ b/pghaskell/pghaskell.el @@ -71,3 +71,4 @@ ) (provide 'pghaskell) +;;; pghaskell.el ends here diff --git a/pgocaml/pgocaml.el b/pgocaml/pgocaml.el index dcf179d0..ce899c45 100644 --- a/pgocaml/pgocaml.el +++ b/pgocaml/pgocaml.el @@ -68,3 +68,4 @@ ) (provide 'pgocaml) +;;; pgocaml.el ends here diff --git a/pgshell/pgshell.el b/pgshell/pgshell.el index 39c780dc..0521b3f9 100644 --- a/pgshell/pgshell.el +++ b/pgshell/pgshell.el @@ -47,3 +47,4 @@ ) (provide 'pgshell) +;;; pgshell.el ends here diff --git a/phox/phox.el b/phox/phox.el index 53a82a55..4b57650a 100644 --- a/phox/phox.el +++ b/phox/phox.el @@ -1,6 +1,16 @@ -;; phox.el +;;; phox.el --- Major mode for the PhoX proof assistant + +;; This file is part of Proof General. + +;; Copyright © 2017 Christophe Raffalli + +;;; Commentary: +;; (require 'proof-site) + +;;; Code: + (proof-ready-for-assistant 'phox) (require 'proof) @@ -70,7 +80,6 @@ "unfold_hyp") ) - ;; code for sisplaying unicode borrowed from ;; Erik Parmann, Pål Drange latex-pretty-symbol @@ -137,5 +146,6 @@ their unicode counterpart" (add-hook 'phox-goals-mode-hook 'phox-unicode-simplified) (add-hook 'phox-response-mode-hook 'phox-unicode-simplified) - (provide 'phox) + +;;; phox.el ends here |