diff options
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-abbrev.el | 6 | ||||
| -rw-r--r-- | coq/coq-autotest.el | 4 | ||||
| -rw-r--r-- | coq/coq-compile-common.el | 108 | ||||
| -rw-r--r-- | coq/coq-db.el | 21 | ||||
| -rw-r--r-- | coq/coq-indent.el | 105 | ||||
| -rw-r--r-- | coq/coq-local-vars.el | 40 | ||||
| -rw-r--r-- | coq/coq-par-compile.el | 148 | ||||
| -rw-r--r-- | coq/coq-par-test.el | 32 | ||||
| -rw-r--r-- | coq/coq-seq-compile.el | 53 | ||||
| -rw-r--r-- | coq/coq-smie.el | 72 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 84 | ||||
| -rw-r--r-- | coq/coq-system.el | 65 | ||||
| -rw-r--r-- | coq/coq-unicode-tokens.el | 14 | ||||
| -rw-r--r-- | coq/coq.el | 161 |
14 files changed, 463 insertions, 450 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)) |