branch: elpa/idris-mode
commit 060d9603808e5b33000d6fb9e714f3dce3c764bf
Author: Marek L <nospam.ke...@gmail.com>
Commit: Marek L <nospam.ke...@gmail.com>
Update documentation strings to follow
best practices reported by checkdoc and flycheck
Why:
To improve maintainability and user experience.
https://www.gnu.org/software/emacs/manual/html_node/elisp/Documentation-Tips.html
---
docs/documentation.tex | 2 +-
idris-commands.el | 83 +++++++++++++++++++++++++-------------------------
idris-common-utils.el | 15 +++++----
idris-events.el | 2 +-
idris-hole-list.el | 8 ++---
idris-ipkg-mode.el | 32 +++++++++----------
idris-log.el | 20 ++++++------
idris-mode.el | 4 +--
idris-prover.el | 44 ++++++++++++--------------
idris-repl.el | 26 ++++++++--------
idris-settings.el | 73 +++++++++++++++++++++-----------------------
idris-simple-indent.el | 6 ++--
idris-syntax.el | 4 +--
idris-tree-info.el | 9 +++---
idris-warnings-tree.el | 17 +++++------
idris-warnings.el | 8 ++---
inferior-idris.el | 51 +++++++++++++++----------------
readme.markdown | 6 ++--
18 files changed, 198 insertions(+), 212 deletions(-)
diff --git a/docs/documentation.tex b/docs/documentation.tex
index 805f00d76c..b4b78c6242 100644
--- a/docs/documentation.tex
+++ b/docs/documentation.tex
@@ -227,7 +227,7 @@ A dependency diagram of the various emacs lisp files is
shown in Figure~\ref{fig
Minor notes on some of the implementation files: \texttt{compat.el} includes
emacs 24.1 compatibility; \texttt{completion.el} implements a completion popup;
\texttt{warnings.el} does the highlighting of warnings using overlays.
-The current design uses exactly one idris process for the interaction (a
handle is stored in \emph{idris-process} (in \texttt{inferior-idris.el})).
+The current design uses exactly one Idris process for the interaction (a
handle is stored in \emph{idris-process} (in \texttt{inferior-idris.el})).
Since it can consume an arbitrary amount of time to handle a request,
\emph{idris-eval-async} (in \texttt{inferior-idris.el}) can be used to evaluate
any sexp, where the given continuation is called with the asynchronous result.
Some features, like tab completion, return a result immediately.
diff --git a/idris-commands.el b/idris-commands.el
index 5f4faf2015..befa67b5f3 100644
--- a/idris-commands.el
+++ b/idris-commands.el
@@ -1,4 +1,4 @@
-;;; idris-commands.el --- Commands for Emacs passed to idris -*-
lexical-binding: t -*-
+;;; idris-commands.el --- Commands for Emacs passed to Idris -*-
lexical-binding: t -*-
;; Copyright (C) 2013 Hannes Mehnert
@@ -46,7 +46,7 @@
(require 'thingatpt)
(defvar-local idris-load-to-here nil
- "The maximum position to load")
+ "The maximum position to load.")
(defun idris-get-line-num (position)
"Get the absolute line number at POSITION."
@@ -113,6 +113,7 @@
"Use the user's settings from customize to determine whether to list the
holes.")
(defun idris-possibly-make-dirty (_beginning _end _length)
+ "Make the buffer dirty."
(idris-make-dirty))
;; If there is a load-to-here marker and a currently loaded region, only
;; make the buffer dirty when the change overlaps the loaded region.
@@ -123,7 +124,6 @@
;; ;; Otherwise just make it dirty.
;; (idris-make-dirty)))
-
(defun idris-update-loaded-region (fc)
(if fc
(let* ((end (assoc :end fc))
@@ -189,7 +189,7 @@ Returning these as a cons."
(defun idris-load-file (&optional set-line)
"Pass the current buffer's file to the inferior Idris process.
-A prefix argument forces loading but only up to the current line."
+A prefix argument SET-LINE forces loading but only up to the current line."
(interactive "p")
(save-buffer)
(idris-ensure-process-and-repl-buffer)
@@ -264,8 +264,8 @@ A prefix argument forces loading but only up to the current
line."
(error "No warnings or errors until beginning of buffer"))))
(defun idris-load-file-sync ()
- "Pass the current buffer's file synchronously to the inferior
-Idris process. This sets the load position to point, if there is one."
+ "Pass the current buffer's file synchronously to the inferior Idris process.
+This sets the load position to point, if there is one."
(save-buffer)
(idris-ensure-process-and-repl-buffer)
(if (buffer-file-name)
@@ -313,9 +313,9 @@ Use this in Idris source buffers."
line)))
(defun idris-name-at-point ()
- "Return the name at point, taking into account semantic
-annotations. Use this in Idris source buffers or in
-compiler-annotated output. Does not return a line number."
+ "Return the name at point, taking into account semantic annotations.
+Use this in Idris source buffers or in compiler-annotated output.
+Does not return a line number."
(let ((ref (cl-remove-if
#'null
(cons (get-text-property (point) 'idris-ref)
@@ -326,7 +326,7 @@ compiler-annotated output. Does not return a line number."
(car ref))))
(defun idris-info-for-name (what name)
- "Display the type for a name"
+ "Display the type for a NAME."
(let* ((ty (idris-eval (list what name)))
(result (car ty))
(formatting (cdr ty)))
@@ -334,7 +334,7 @@ compiler-annotated output. Does not return a line number."
(defun idris-type-at-point (thing)
- "Display the type of the name at point, considered as a global variable"
+ "Display the type of the THING at point, considered as a global variable."
(interactive "P")
(let ((name (if thing (read-string "Check: ")
(idris-name-at-point))))
@@ -342,7 +342,7 @@ compiler-annotated output. Does not return a line number."
(idris-info-for-name :type-of name))))
(defun idris-print-definition-of-name (thing)
- "Display the definition of the function or type at point"
+ "Display the definition of the function or type of the THING at point."
(interactive "P")
(let ((name (if thing (read-string "Print definition: ")
(idris-name-at-point))))
@@ -397,7 +397,8 @@ compiler-annotated output. Does not return a line number."
"Browse Namespace"))
(defun idris-caller-tree (caller cmd)
- "Display a tree from an IDE caller list, lazily retrieving a few levels at a
time"
+ "Display a tree from an IDE CALLER list.
+Using CMD lazily retrieve a few levels at a time from Idris compiler."
(pcase caller
(`((,name ,highlight) ,children)
(make-idris-tree
@@ -412,7 +413,7 @@ compiler-annotated output. Does not return a line number."
nil)))
children))
:preserve-properties '(idris-tt-tree)))
- (_ (error "failed to make tree from %s" caller))))
+ (_ (error "Failed to make tree from %s" caller))))
(defun idris-namespace-tree (namespace &optional recursive)
"Create a tree of the contents of NAMESPACE.
@@ -459,7 +460,7 @@ Lazily retrieve children when RECURSIVE is non-nil."
(_ (error "Invalid namespace %s" namespace)))))))
(defun idris-newline-and-indent ()
- "Indent a new line like the current one by default"
+ "Indent a new line like the current one by default."
(interactive)
(let ((indent ""))
(save-excursion
@@ -474,8 +475,8 @@ If the current buffer is in `idris-mode' and the file being
edited is a literate Idris file, deleting the end of a line will
take into account bird tracks. If Transient Mark mode is
enabled, the mark is active, and N is 1, delete the text in the
-region and deactivate the mark instead. To disable this, set
-`delete-active-region' to nil.
+region and deactivate the mark instead.
+To disable this, set variable `delete-active-region' to nil.
Optional second arg KILLFLAG non-nil means to kill (save in kill
ring) instead of delete. Interactively, N is the prefix arg, and
@@ -527,7 +528,7 @@ Considered as a global variable"
(idris-info-for-name :docs-for name))))
(defun idris-eldoc-lookup ()
- "Support for showing type signatures in the modeline when there's a running
Idris"
+ "Return Eldoc string associated with the thing at point."
(get-char-property (point) 'idris-eldoc))
(defun idris-pretty-print ()
@@ -603,7 +604,7 @@ Otherwise, case split as a pattern variable."
(t (idris-case-split))))
(defun idris-add-clause (proof)
- "Add clauses to the declaration at point"
+ "Add clauses to the declaration at point."
(interactive "P")
(let ((what (idris-thing-at-point))
(command (if proof :add-proof-clause :add-clause)))
@@ -638,7 +639,7 @@ Otherwise, case split as a pattern variable."
(goto-char final-point))))) ;; Put the cursor on the start of the
inserted clause
(defun idris-add-missing ()
- "Add missing cases"
+ "Add missing cases."
(interactive)
(let ((what (idris-thing-at-point)))
(when (car what)
@@ -648,7 +649,7 @@ Otherwise, case split as a pattern variable."
(insert result)))))
(defun idris-make-with-block ()
- "Add with block"
+ "Add with block."
(interactive)
(let ((what (idris-thing-at-point)))
(when (car what)
@@ -659,7 +660,7 @@ Otherwise, case split as a pattern variable."
(insert result)))))
(defun idris-make-lemma ()
- "Extract lemma from hole"
+ "Extract lemma from hole."
(interactive)
(let ((what (idris-thing-at-point)))
(when (car what)
@@ -742,9 +743,9 @@ Otherwise, case split as a pattern variable."
"The end position of the last proof region.")
(defun idris-proof-search (&optional arg)
- "Invoke the proof search. A plain prefix argument causes the
-command to prompt for hints and recursion depth, while a numeric
-prefix argument sets the recursion depth directly."
+ "Invoke the proof search.
+A plain prefix ARG causes the command to prompt for hints and recursion
+ depth, while a numeric prefix argument sets the recursion depth directly."
(interactive "P")
(let ((hints (if (consp arg)
(split-string (read-string "Hints: ") "[^a-zA-Z0-9']")
@@ -774,7 +775,7 @@ prefix argument sets the recursion depth directly."
Idris 2 only."
(interactive)
(if (not proof-region-start)
- (error "You must proof search first before looking for subsequent proof
results.")
+ (error "You must proof search first before looking for subsequent proof
results")
(let ((result (car (idris-eval `:proof-search-next))))
(if (string= result "No more results")
(message "No more results")
@@ -789,7 +790,7 @@ Idris 2 only."
(defvar-local def-region-end nil)
(defun idris-generate-def ()
- "Generate defintion."
+ "Generate definition."
(interactive)
(let ((what (idris-thing-at-point)))
(when (car what)
@@ -832,7 +833,7 @@ Idris 2 only."
Idris 2 only."
(interactive)
(if (not def-region-start)
- (error "You must program search first before looking for subsequent
program results.")
+ (error "You must program search first before looking for subsequent
program results")
(let ((result (car (idris-eval `:generate-def-next))))
(if (string= result "No more results")
(message "No more results")
@@ -942,7 +943,7 @@ type-correct, so loading will fail."
(let ((buf (get-buffer idris-repl-buffer-name)))
(if buf
(pop-to-buffer buf)
- (error "No Idris REPL buffer is open."))))
+ (error "No Idris REPL buffer is open"))))
(defun idris-switch-to-last-idris-buffer ()
"Switch to the last Idris buffer.
@@ -990,8 +991,9 @@ https://github.com/clojure-emacs/cider";
idris-protocol-version-minor 0)))
(defun idris-delete-ibc (no-confirmation)
- "Delete the IBC file for the current buffer. A prefix argument
-means to not ask for confirmation."
+ "Delete the IBC file for the current buffer.
+When NO-CONFIRMATION argument is set to t the deletion will be
+performed silently without confirmation from the user."
(interactive "P")
(unless (> idris-protocol-version 1)
(let* ((fname (buffer-file-name))
@@ -1038,8 +1040,7 @@ be Idris's own serialization of the term in question."
menu))
(defun idris-insert-term-widget (term)
- "Make a widget for interacting with the term represented by TERM
-beginning at START-POS in the current buffer."
+ "Make a widget for interacting with the TERM."
(let ((inhibit-read-only t)
(start-pos (copy-marker (point)))
(end-pos (copy-marker (idris-find-term-end (point) 1)))
@@ -1088,7 +1089,7 @@ beginning at START-POS in the current buffer."
(idris-insert-term-widget term)))))
(defun idris-remove-term-widgets (&optional buffer)
- "Remove interaction widgets from annotated terms."
+ "Remove interaction widgets from annotated terms in BUFFER."
(interactive)
(with-current-buffer (or buffer (current-buffer))
(save-excursion
@@ -1102,27 +1103,27 @@ beginning at START-POS in the current buffer."
(delete-char 1))))))
(defun idris-show-term-implicits (position &optional buffer)
- "Replace the term at POSITION with a fully-explicit version."
+ "Replace the term at POSITION in BUFFER with a fully-explicit version."
(interactive "d")
(idris-active-term-command position :show-term-implicits buffer))
(defun idris-hide-term-implicits (position &optional buffer)
- "Replace the term at POSITION with a fully-implicit version."
+ "Replace the term at POSITION in BUFFER with a fully-implicit version."
(interactive "d")
(idris-active-term-command position :hide-term-implicits buffer))
(defun idris-normalize-term (position &optional buffer)
- "Replace the term at POSITION with a normalized version."
+ "Replace the term at POSITION in BUFFER with a normalized version."
(interactive "d")
(idris-active-term-command position :normalise-term buffer))
(defun idris-show-core-term (position &optional buffer)
- "Replace the term at POSITION with the corresponding core term."
+ "Replace the term at POSITION in BUFFER with the corresponding core term."
(interactive "d")
(idris-active-term-command position :elaborate-term buffer))
(defun idris-active-term-command (position cmd &optional buffer)
- "For the term at POSITION, Run the live term command CMD."
+ "For the term at POSITION in BUFFER, run the live term command (CMD)."
(unless (member cmd '(:show-term-implicits
:hide-term-implicits
:normalise-term
@@ -1201,7 +1202,7 @@ of the term to replace."
(select-window window))))))))
(defun idris-fill-paragraph (justify)
- ;; In literate Idris files, allow filling non-code paragraphs
+ "In literate Idris files, allow filling non-code paragraphs."
(if (and (idris-lidr-p) (not (save-excursion (move-beginning-of-line nil)
(looking-at-p ">\\s-"))))
(fill-paragraph justify)
@@ -1219,7 +1220,7 @@ of the term to replace."
(defun idris-set-idris-load-packages ()
- "Interactively set the `idris-load-packages' variable"
+ "Interactively set the `idris-load-packages' variable."
(interactive)
(let* ((idris-libdir (replace-regexp-in-string
"[\r\n]*\\'" "" ; remove trailing newline junk
diff --git a/idris-common-utils.el b/idris-common-utils.el
index 8b3cbf12a9..0af862df57 100644
--- a/idris-common-utils.el
+++ b/idris-common-utils.el
@@ -35,8 +35,7 @@
;;; These variables are here because many things depend on them
(defvar-local idris-buffer-dirty-p t
- "An Idris buffer is dirty if there have been modifications since
-it was last loaded")
+ "An Idris buffer is dirty if it have been modified since it was last
loaded.")
(defvar idris-currently-loaded-buffer nil
"The buffer currently loaded by the running Idris.")
@@ -141,7 +140,7 @@ inserted text (that is, relative to point prior to
insertion)."
"The decors that should light up as responsive to mouse clicks.")
(defun idris-semantic-properties-face (props)
- "Compute the text property `face' from the Idris properties for a region."
+ "Compute the text property `face' from the Idris properties (PROPS) for a
region."
(let* ((decor (assoc :decor props))
(implicit (assoc :implicit props))
(text-format (assoc :text-formatting props))
@@ -197,7 +196,7 @@ inserted text (that is, relative to point prior to
insertion)."
(defun idris-semantic-properties-eldoc (props)
- "Compute an Eldoc string from Idris semantic properties PROPS"
+ "Compute an Eldoc string from Idris semantic properties (PROPS)."
(let* ((name (assoc :name props))
(namespace (assoc :namespace props))
(source-file (assoc :source-file props))
@@ -255,7 +254,7 @@ inserted text (that is, relative to point prior to
insertion)."
(t nil))))
(defun idris-semantic-properties (props)
- "Compute how to highlight with Idris compiler properties PROPS."
+ "Compute how to highlight with Idris compiler properties (PROPS)."
(let* ((name (assoc :name props))
(decor (assoc :decor props))
(term (assoc :tt-term props))
@@ -384,7 +383,7 @@ Use the current buffer if BUFFER is not supplied or is nil."
(overlay-put overlay 'help-echo help-echo)))
(defun idris-clear-file-link-overlays (&optional mode)
- "Remove all file link overlays from the current buffer"
+ "Remove all file link overlays from the current buffer."
(when (or (not mode) (eq major-mode mode))
(remove-overlays (point-min) (point-max) 'idris-file-link t)))
@@ -409,8 +408,8 @@ relative to SRC-DIR"
(when (file-exists-p lidr)
(make-link lidr))))))
-(defvar idris-protocol-version 0 "The protocol version")
-(defvar idris-protocol-version-minor 0 "The protocol minor version")
+(defvar idris-protocol-version 0 "The protocol version.")
+(defvar idris-protocol-version-minor 0 "The protocol minor version.")
(defun >=-protocol-version (major minor)
(or (> idris-protocol-version major)
diff --git a/idris-events.el b/idris-events.el
index e2642d4d6a..cd4e319ec1 100644
--- a/idris-events.el
+++ b/idris-events.el
@@ -68,7 +68,7 @@ The event is only logged if `idris-log-events' is non-nil."
(pp event buffer)))
(defun idris-dump-events-to-file (file)
- "Dump event log to file"
+ "Dump event log to FILE."
(when idris-log-events
(with-current-buffer (idris-events-buffer)
(write-file file))))
diff --git a/idris-hole-list.el b/idris-hole-list.el
index 643dbd51fa..3d45bbcd2d 100644
--- a/idris-hole-list.el
+++ b/idris-hole-list.el
@@ -32,10 +32,10 @@
(require 'idris-settings)
(defvar idris-hole-list-buffer-name (idris-buffer-name :holes)
- "The name of the buffer containing Idris holes")
+ "The name of the buffer containing Idris holes.")
(defun idris-hole-list-quit ()
- "Quit the Idris hole list"
+ "Quit the Idris hole list."
(interactive)
(idris-kill-buffer idris-hole-list-buffer-name))
@@ -54,7 +54,7 @@
map))
(easy-menu-define idris-hole-list-mode-menu idris-hole-list-mode-map
- "Menu for the Idris hole list buffer"
+ "Menu for the Idris hole list buffer."
`("Idris Holes"
["Show term interaction widgets" idris-add-term-widgets t]
["Close hole list buffer" idris-hole-list-quit t]
@@ -73,7 +73,7 @@ Invokes `idris-hole-list-mode-hook'."
;; (push '("#\\*idris-holes\\*$" . idris-hole-list-mode) auto-mode-alist)
(defun idris-hole-list-buffer ()
- "Return the Idris hole buffer, creating one if there is not one"
+ "Return the Idris hole buffer, creating one if there is not one."
(get-buffer-create idris-hole-list-buffer-name))
(defun idris-hole-list-show (hole-info)
diff --git a/idris-ipkg-mode.el b/idris-ipkg-mode.el
index 6a2208bc4c..3fe70b9d4d 100644
--- a/idris-ipkg-mode.el
+++ b/idris-ipkg-mode.el
@@ -27,12 +27,12 @@
(defface idris-ipkg-keyword-face
'((t (:inherit font-lock-keyword-face)))
- "The face to highlight Idris package keywords"
+ "The face to highlight Idris package keywords."
:group 'idris-faces)
(defface idris-ipkg-package-name-face
'((t (:inherit font-lock-function-name-face)))
- "The face to highlight the name of the package"
+ "The face to highlight the name of the package."
:group 'idris-faces)
@@ -107,7 +107,7 @@
failure)))
(defun idris-ipkg-complete-keyword ()
- "Complete the current .ipkg keyword, if possible"
+ "Complete the current .ipkg keyword, if possible."
(interactive)
(cl-destructuring-bind (identifier start end) (idris-ipkg-find-keyword)
(when identifier
@@ -115,7 +115,7 @@
;;; Inserting fields
(defun idris-ipkg-insert-field ()
- "Insert one of the ipkg fields"
+ "Insert one of the ipkg fields."
(interactive)
(let ((field (completing-read "Field: " (remove "package"
idris-ipkg-keywords) nil t)))
(beginning-of-line)
@@ -133,7 +133,7 @@
;;; Clickable modules
(defun idris-ipkg-make-files-clickable ()
- "Make all modules with existing files clickable, where clicking opens them"
+ "Make all modules with existing files clickable, where clicking opens them."
(interactive)
(idris-clear-file-link-overlays 'idris-ipkg-mode)
(let ((src-dir (idris-ipkg-buffer-src-dir (file-name-directory
(buffer-file-name)))))
@@ -180,7 +180,7 @@
(defun idris-ipkg-enable-clickable-files ()
- "Enable setting up clickable modules and makefiles on idle Emacs"
+ "Enable setting up clickable modules and makefiles on idle Emacs."
(interactive)
(add-hook 'after-save-hook 'idris-ipkg-make-files-clickable)
(idris-ipkg-make-files-clickable))
@@ -217,9 +217,8 @@ or nil if not found."
(find-file-r dir))))))
(defun idris-try-directory-files (directory &optional full match nosort)
- "Call `directory-files' with arguments DIRECTORY, FULL, MATCH,
-and NOSORT, but return the empty list on failure instead of
-throwing an error.
+ "Call `directory-files' with arguments DIRECTORY, FULL, MATCH and NOSORT.
+Return the empty list on failure instead of throwing an error.
See the docstring for `directory-files' for the meaning of the
arguments."
@@ -233,7 +232,7 @@ arguments."
(defvar idris-ipkg-build-buffer-name "*idris-build*")
(defun idris-ipkg--compilation-buffer-name-function (_mode)
- "Compute a buffer name for the idris-mode compilation buffer."
+ "Compute a buffer name for the `idris-mode' compilation buffer."
idris-ipkg-build-buffer-name)
(defun idris-ipkg--ansi-compile-filter (start)
@@ -243,7 +242,7 @@ arguments."
(ansi-color-apply-on-region start (point)))))
(defun idris-ipkg-command (ipkg-file command)
- "Run a command on ipkg-file. The command can be build, install, or clean."
+ "Run a command on IPKG-FILE. The COMMAND can be build, install, or clean."
;; Idris must have its working directory in the same place as the ipkg file
(let ((dir (file-name-directory ipkg-file))
(file (file-name-nondirectory ipkg-file))
@@ -375,8 +374,7 @@ arguments."
pkgs)))))
(defun idris-ipkg-pkgs-flags-for-current-buffer ()
- "Compute a list of Idris command line options
-based on the pkgs field of the .ipkg file."
+ "List of Idris command line options based on the pkgs field of the .ipkg
file."
(let ((pkgs (idris-ipkg-pkgs-for-current-buffer)))
(cl-loop for pkg in pkgs appending (list "-p" pkg))))
@@ -401,10 +399,10 @@ based on the pkgs field of the .ipkg file."
idris-define-ipkg-editing-keys)
do (funcall keyer map))
map)
- "Keymap used for Idris package mode")
+ "Keymap used for Idris package mode.")
(easy-menu-define idris-ipkg-mode-menu idris-ipkg-mode-map
- "Menu for Idris package mode"
+ "Menu for Idris package mode."
`("IPkg"
["Build package" idris-ipkg-build t]
["Install package" idris-ipkg-install t]
@@ -414,8 +412,8 @@ based on the pkgs field of the .ipkg file."
;;;###autoload
(define-derived-mode idris-ipkg-mode prog-mode "Idris Pkg"
- "Major mode for Idris package files
- \\{idris-ipkg-mode-map}
+ "Major mode for Idris package files.
+\\{idris-ipkg-mode-map}
Invokes `idris-ipkg-mode-hook'."
:group 'idris
:syntax-table idris-ipkg-syntax-table
diff --git a/idris-log.el b/idris-log.el
index 73b8fd565d..667d80c481 100644
--- a/idris-log.el
+++ b/idris-log.el
@@ -33,42 +33,42 @@
(defface idris-log-timestamp-face
'((t :foreground "#211ab0"
:weight bold))
- "The face used for timestamps in the Idris log"
+ "The face used for timestamps in the Idris log."
:group 'idris-faces)
(defface idris-log-level-face
'((t :weight bold))
- "General properties for displaying Idris log levels"
+ "General properties for displaying Idris log levels."
:group 'idris-faces)
(defface idris-log-level-1-face
'((t :foreground "#ff0011"))
- "The face used for log level 1 in the Idris log"
+ "The face used for log level 1 in the Idris log."
:group 'idris-faces)
(defface idris-log-level-2-face
'((t :foreground "#dd0033"))
- "The face used for log level 2 in the Idris log"
+ "The face used for log level 2 in the Idris log."
:group 'idris-faces)
(defface idris-log-level-3-face
'((t :foreground "#bb0055"))
- "The face used for log level 3 in the Idris log"
+ "The face used for log level 3 in the Idris log."
:group 'idris-faces)
(defface idris-log-level-4-face
'((t :foreground "#990077"))
- "The face used for log level 4 in the Idris log"
+ "The face used for log level 4 in the Idris log."
:group 'idris-faces)
(defface idris-log-level-5-face
'((t :foreground "#770099"))
- "The face used for log level 5 in the Idris log"
+ "The face used for log level 5 in the Idris log."
:group 'idris-faces)
(defface idris-log-level-higher-face
'((t :foreground "#550099"))
- "The face used for log levels over 5 in the Idris log"
+ "The face used for log levels over 5 in the Idris log."
:group 'idris-faces)
(defun idris-get-log-level-face (level)
@@ -85,8 +85,8 @@
map))
(define-derived-mode idris-log-mode fundamental-mode "Idris Log"
- "Major mode used to show Idris compiler internals logs
- \\{idris-log-mode-map}
+ "Major mode used to show Idris compiler internals logs.
+\\{idris-log-mode-map}
Invokes `idris-log-mode-hook'."
(buffer-disable-undo)
(set (make-local-variable 'outline-regexp) "^(")
diff --git a/idris-mode.el b/idris-mode.el
index f6d7b798e6..7d95895f94 100644
--- a/idris-mode.el
+++ b/idris-mode.el
@@ -66,7 +66,7 @@
(easy-menu-define idris-mode-menu idris-mode-map
- "Menu for the Idris major mode"
+ "Menu for the Idris major mode."
`("Idris"
["New Project" idris-start-project t]
"-----------------"
@@ -75,7 +75,7 @@
["Compile and execute" idris-compile-and-execute]
["Delete IBC file" idris-delete-ibc t]
["View compiler log" idris-view-compiler-log (get-buffer
idris-log-buffer-name)]
- ["Quit inferior idris process" idris-quit t]
+ ["Quit inferior Idris process" idris-quit t]
"-----------------"
["Add initial match clause to type declaration" idris-add-clause t]
["Add missing cases" idris-add-missing t]
diff --git a/idris-prover.el b/idris-prover.el
index 9a4ea45c2b..57004a2619 100644
--- a/idris-prover.el
+++ b/idris-prover.el
@@ -37,7 +37,7 @@
; | proof shell | proof script |
; ------------------------------
-(defgroup idris-prover nil "Idris Prover" :prefix 'idris :group 'idris)
+(defgroup idris-prover nil "Idris Prover." :prefix 'idris :group 'idris)
(defface idris-prover-processed-face
'((t (:background "PaleGreen1")))
@@ -50,8 +50,7 @@
:group 'idris-faces)
(defcustom idris-prover-restore-window-configuration t
- "When non-nil, restore the window configuration after exiting
-the prover."
+ "When non-nil, restore the window configuration after exiting the prover."
:type 'boolean
:group 'idris-prover)
@@ -65,12 +64,11 @@ the prover."
"The name of the Idris proof script buffer.")
(defvar idris-prover-currently-proving nil
- "The hole that Idris has open in the interactive prover, or nil
-if Idris is not proving anything.")
+ "The hole that Idris has open in the interactive prover.
+Nil if Idris is not proving anything.")
(defconst idris-prover-error-message-prefix "Prover error: "
- "A prefix to show on minibuffer error messages that originate
- in the prover.")
+ "A prefix to show on minibuffer error messages that originate in the
prover.")
(defun idris-prover-obligations-buffer ()
(or (get-buffer idris-prover-obligations-buffer-name)
@@ -104,24 +102,24 @@ string and whose cadr is highlighting information."
"The saved window configuration from before running the prover.")
(defvar-local idris-prover-script-processed nil
- "Marker for the processed part of proof script")
+ "Marker for the processed part of proof script.")
(defvar-local idris-prover-script-processed-overlay nil
- "Overlay for processed proof script")
+ "Overlay for processed proof script.")
(defvar-local idris-prover-script-processing nil
- "Marker for the processing part of proof script")
+ "Marker for the processing part of proof script.")
(defvar-local idris-prover-script-processing-overlay nil
- "Overlay for processing proof script")
+ "Overlay for processing proof script.")
(defvar-local idris-prover-script-warning-overlay nil
- "Overlay for warning in proof script")
+ "Overlay for warning in proof script.")
; invariant: point-min <= idris-prover-script-processed <=
idris-prover-script-processing <= point-max
(defvar-local idris-prover-prove-step 0
- "Step counter of the proof")
+ "Step counter of the proof.")
(defvar idris-prover-script-mode-map
(let ((map (make-sparse-keymap)))
@@ -150,10 +148,9 @@ string and whose cadr is highlighting information."
(list start (point) completions)))))
(defun idris-prover-find-tactic (start-pos)
- "Use some layout heuristics to find the tactic beginning at
-START-POS, returning a pair consisting of the start and end
-positions of the tactic. Tactics are required to begin at the
-left margin."
+ "Use layout heuristics to find the tactic beginning at START-POS.
+Return a pair consisting of the start and end positions of the tactic.
+Tactics are required to begin at the left margin."
(let (tactic-start tactic-end)
(save-excursion
(goto-char start-pos)
@@ -188,7 +185,7 @@ left margin."
(defun idris-prover-script-backward ()
- "Backward one piece of proof script"
+ "Backward one piece of proof script."
(interactive)
(idris-eval-async (list :interpret (if idris-enable-elab-prover ":undo"
"undo"))
#'(lambda (_result) t)
@@ -273,7 +270,7 @@ left margin."
(error "No proof in progress")))
(easy-menu-define idris-prover-script-mode-menu idris-prover-script-mode-map
- "Menu for Idris prover scripts"
+ "Menu for Idris prover scripts."
`("Idris Proof"
["Advance" idris-prover-script-forward t]
["Retract" idris-prover-script-backward t]
@@ -283,7 +280,7 @@ left margin."
(define-derived-mode idris-prover-script-mode prog-mode "Idris-Proof-Script"
"Major mode for interacting with Idris proof script.
- \\{idris-prover-script-mode-map}
+\\{idris-prover-script-mode-map}
Invokes `idris-prover-script-mode-hook'."
:group 'idris-prover
(set (make-local-variable 'completion-at-point-functions)
@@ -302,8 +299,7 @@ Invokes `idris-prover-script-mode-hook'."
buffer)))
(defun idris-prover-reset-prover-script-buffer ()
- "Erase or initialize a proof script buffer, resetting all the
-special prover state."
+ "Erase or initialize a proof script buffer, resetting all the prover state."
(with-current-buffer (idris-prover-script-buffer)
(when idris-prover-script-processed-overlay
(delete-overlay idris-prover-script-processed-overlay)
@@ -453,8 +449,8 @@ the length reported by Idris."
(kill-buffer proof-buffer)))))
(defconst idris-proof-script-insertion-marker "---------- Proofs ----------"
- "Look for this marker to insert proofs. Should agree with the
- one in the Idris compiler source.")
+ "Look for this marker to insert proofs.
+Should agree with the one in the Idris compiler source.")
(defun idris-insert-proof-script (buffer proof)
"Insert PROOF into BUFFER."
diff --git a/idris-repl.el b/idris-repl.el
index e307d36fc1..2baba65ccd 100644
--- a/idris-repl.el
+++ b/idris-repl.el
@@ -55,7 +55,7 @@
"Welcome to the Idris REPL!")
(defun idris-repl-get-logo ()
- "Return the path to the Idris logo if it exists, or `nil' if not."
+ "Return the path to the Idris logo if it exists, or nil if not."
(let ((logo-path (concat idris-mode-path "logo-small.png")))
(if (file-readable-p logo-path)
logo-path
@@ -63,7 +63,7 @@
(defun idris-repl-insert-logo ()
"Attempt to insert a graphical logo.
-Returns non-`nil' on success, `nil' on failure."
+Returns non-nil on success, nil on failure."
(let ((logo (idris-repl-get-logo)))
(if (and (display-graphic-p)
(image-type-available-p 'png)
@@ -75,13 +75,13 @@ Returns non-`nil' on success, `nil' on failure."
(defun idris-repl-animate-banner ()
"Insert a text banner using animation.
-Returns non-`nil' on success, `nil' on failure."
+Returns non-nil on success, nil on failure."
(animate-string (idris-repl-welcome-message) 0 0)
t)
(defun idris-repl-text-banner ()
"Insert a text banner with no animation.
-Returns non-`nil' on success, `nil' on failure."
+Returns non-nil on success, nil on failure."
(insert (idris-repl-welcome-message))
t)
@@ -196,7 +196,7 @@ If ALWAYS-INSERT is non-nil, always insert a prompt at the
end of the buffer."
"Keymap used in Idris REPL mode.")
(easy-menu-define idris-repl-mode-menu idris-repl-mode-map
- "Menu for the Idris REPL mode"
+ "Menu for the Idris REPL mode."
`("Idris REPL"
("Interpreter options" :active idris-process
["Show implicits" (idris-set-option :show-implicits t)
@@ -209,12 +209,12 @@ If ALWAYS-INSERT is non-nil, always insert a prompt at
the end of the buffer."
:visible (idris-get-option :error-context)])
["Show term interaction widgets" idris-add-term-widgets t]
["Customize idris-mode" (customize-group 'idris) t]
- ["Quit inferior idris process" idris-quit t]
+ ["Quit inferior Idris process" idris-quit t]
))
(define-derived-mode idris-repl-mode fundamental-mode "Idris-REPL"
"Major mode for interacting with Idris.
- \\{idris-repl-mode-map}
+\\{idris-repl-mode-map}
Invokes `idris-repl-mode-hook'."
;syntax-table?
:group 'idris-repl
@@ -286,7 +286,7 @@ Invokes `idris-repl-mode-hook'."
(idris-repl-eval-string input input-start))))
(defun idris-repl-complete ()
- "Completion of the current input"
+ "Completion of the current input."
(when idris-completion-via-compiler
(let* ((input (idris-repl-current-input))
(result (idris-eval `(:repl-completions ,input))))
@@ -296,7 +296,7 @@ Invokes `idris-repl-mode-hook'."
(list (+ idris-input-start (length partial)) (point-max)
completions))))))
(defun find-common-prefix (input slist)
- "Finds longest common prefix of all strings in list."
+ "Finds longest common prefix of all strings in SLIST."
(let ((first (car slist))
(ilen (length input)))
(if (> (length first) ilen)
@@ -308,7 +308,7 @@ Invokes `idris-repl-mode-hook'."
input)))
(defun idris-repl-begin-of-prompt ()
- "Got to the beginning of linke or the prompt."
+ "Go to the beginning of line or the prompt."
(interactive)
(cond ((and (>= (point) idris-input-start)
(idris-same-line-p (point) idris-input-start))
@@ -431,7 +431,7 @@ highlighting information from Idris."
"History list of strings entered into the REPL buffer.")
(defun idris-repl-add-to-input-history (string)
- "Adds input to history."
+ "Add input STRING to history."
(unless (equal string "")
(setq idris-repl-input-history
(remove string idris-repl-input-history)))
@@ -570,9 +570,9 @@ The default value for FILENAME is
`idris-repl-history-file'."
(read (current-buffer)))))))
(defun idris-repl-save-history (&optional filename history)
- "Simply save the current Idris REPL history to a file.
+ "Save the current Idris REPL HISTORY to a FILENAME.
When Idris is setup to always load the old history and one uses only
-one instance of idris all the time, there is no need to merge the
+one instance of Idris all the time, there is no need to merge the
files and this function is sufficient."
(interactive (list (idris-repl-read-history-filename)))
(let ((file (or filename (idris-repl-history-file-f)))
diff --git a/idris-settings.el b/idris-settings.el
index a1d70bd694..bf9a3f38f2 100644
--- a/idris-settings.el
+++ b/idris-settings.el
@@ -31,17 +31,17 @@
(defgroup idris nil "Idris mode" :prefix 'idris :group 'languages)
(defcustom idris-interpreter-path "idris"
- "The path to the Idris interpreter"
+ "The path to the Idris interpreter."
:type 'file
:group 'idris)
(defcustom idris-interpreter-flags '()
- "The command line arguments passed to the Idris interpreter"
+ "The command line arguments passed to the Idris interpreter."
:type '(repeat string)
:group 'idris)
(defcustom idris-warnings-printing (list 'warnings-tree)
- "How to print warnings: tree view ('warnings-tree) in REPL ('warnings-repl)"
+ "How to print warnings: tree view ('warnings-tree) in REPL ('warnings-repl)."
:group 'idris
:type '(repeat symbol)
:options '(warnings-tree warnings-repl))
@@ -54,8 +54,8 @@
(defcustom idris-show-help-text t
- "Show explanatory text in idris-mode's auxiliary buffers if
- non-nil. Advanced users may wish to disable this."
+ "Show explanatory text in idris-mode's auxiliary buffers if non-nil.
+Advanced users may wish to disable this."
:group 'idris
:type 'boolean)
@@ -65,8 +65,7 @@
:type 'boolean)
(defcustom idris-semantic-source-highlighting t
- "If non-nil, use the Idris compiler's semantic source
-information to highlight Idris code.
+ "Use the Idris compiler's semantic source information to highlight Idris
code.
If `debug', log failed highlighting to buffer `*Messages*'."
:group 'idris
:type '(choice (boolean :tag "Enable")
@@ -95,7 +94,7 @@ The log is placed in `idris-event-buffer-name'."
:background "lightgray")
(((background dark))
:background "darkgray"))
- "The face to highlight active terms"
+ "The face to highlight active terms."
:group 'idris-faces)
(defface idris-semantic-type-face
@@ -103,7 +102,7 @@ The log is placed in `idris-event-buffer-name'."
:foreground "blue")
(((background dark))
:foreground "cornflower blue"))
- "The face to be used to highlight types"
+ "The face to be used to highlight types."
:group 'idris-faces)
(defface idris-semantic-data-face
@@ -111,7 +110,7 @@ The log is placed in `idris-event-buffer-name'."
:foreground "red")
(((background dark))
:foreground "firebrick1"))
- "The face to be used to highlight data and constructors"
+ "The face to be used to highlight data and constructors."
:group 'idris-faces)
(defface idris-semantic-function-face
@@ -119,12 +118,12 @@ The log is placed in `idris-event-buffer-name'."
:foreground "darkgreen")
(((background dark))
:foreground "#A6E22E"))
- "The face to be used to highlight defined functions"
+ "The face to be used to highlight defined functions."
:group 'idris-faces)
(defface idris-semantic-postulate-face
'((t (:inherit idris-unsafe-face :weight semi-bold)))
- "The face to be used to highlight postulated values"
+ "The face to be used to highlight postulated values."
:group 'idris-faces)
(defface idris-semantic-bound-face
@@ -132,37 +131,36 @@ The log is placed in `idris-event-buffer-name'."
:foreground "purple")
(((background dark))
:foreground "MediumPurple1"))
- "The face to be used to highlight bound variables"
+ "The face to be used to highlight bound variables."
:group 'idris-faces)
(defface idris-semantic-implicit-face
'((t (:underline t)))
- "The face to be used to highlight implicit arguments"
+ "The face to be used to highlight implicit arguments."
:group 'idris-faces)
(defface idris-semantic-namespace-face
'((t (:italic t)))
- "The face to be used to highlight namespace declarations"
+ "The face to be used to highlight namespace declarations."
:group 'idris-faces)
(defface idris-semantic-module-face
'((t :inherit idris-semantic-namespace-face))
- "The face to be used to highlight namespace declarations"
+ "The face to be used to highlight namespace declarations."
:group 'idris-faces)
(defface idris-quasiquotation-face nil
- "The face to be used to highlight quasiquotations in Idris source code"
+ "The face to be used to highlight quasiquotations in Idris source code."
:group 'idris-faces)
(defface idris-antiquotation-face nil
- "The face to be used to highlight antiquotations in Idris source code"
+ "The face to be used to highlight antiquotations in Idris source code."
:group 'idris-faces)
(defface idris-loaded-region-face nil
- "The face to use for the currently-loaded region of a
-buffer. Since semantic highlighting has been added, this face
-defaults to nothing, but is provided for users who prefer the old
-behavior."
+ "The face to use for the currently-loaded region of a buffer.
+Since semantic highlighting has been added, this face defaults to nothing,
+but is provided for users who prefer the old behavior."
:group 'idris-faces)
(defface idris-inline-doc-face
@@ -183,16 +181,16 @@ behavior."
;;; Mode hooks
(defcustom idris-mode-hook '(turn-on-idris-simple-indent
turn-on-eldoc-mode)
- "Hook to run upon entering Idris mode. You should choose at most
-one indentation style."
+ "Hook to run upon entering Idris mode.
+You should choose at most one indentation style."
:type 'hook
:options '(turn-on-idris-simple-indent
turn-on-eldoc-mode)
:group 'idris)
(defcustom idris-mode-lidr-hook '()
- "Hook to run after opening a literate Idris file. Use this to
-customize the display of non-code text."
+ "Hook to run after opening a literate Idris file.
+Use this to customize the display of non-code text."
:type 'hook
:group 'idris)
@@ -276,12 +274,11 @@ will be removed from the list automatically and will not
be executed."
(defcustom idris-repl-banner-functions '(idris-repl-insert-logo
idris-repl-animate-banner
idris-repl-text-banner)
- "A list of functions that can attempt to insert a banner into
-the REPL. If a function cannot insert a banner (for instance, if
-it is supposed to insert a graphical banner but the current Emacs
-has no image support), it returns `nil'. The functions in this
-list are run in order, until one returns non-`nil'.
-Set to `nil' for no banner."
+ "A list of functions that can attempt to insert a banner into the REPL.
+If a function cannot insert a banner (for instance, if it is supposed
+to insert a graphical banner but the current Emacs has no image support),
+it returns nil. The functions in this list are run in order,
+until one returns non-nil. Set to nil for no banner."
:type 'hook
:group 'idris-repl
:options '(idris-repl-insert-logo
@@ -327,26 +324,26 @@ using Idris2, then you may wish to customise this
variable."
:group 'idris-repl)
(defcustom idris-repl-history-size 200
- "*Maximum number of lines for persistent REPL history."
+ "Maximum number of lines for persistent REPL history."
:type 'integer
:group 'idris-repl)
(defcustom idris-repl-history-file-coding-system
'utf-8-unix
- "*The coding system for the history file."
+ "The coding system for the history file."
:type 'symbol
:group 'idris-repl)
(defcustom idris-repl-prompt-style 'short
- "What sort of prompt to show. 'long shows the Idris REPL prompt,
-while 'short shows a shorter one."
+ "What sort of prompt to show.
+'long shows the Idris REPL prompt, while 'short shows a shorter one."
:options '(short long)
:type 'symbol
:group 'idris-repl)
(defcustom idris-repl-show-repl-on-startup t
- "If non-`nil', show the REPL window when Idris starts. If `nil',
-only do this when `idris-repl' was called interactively."
+ "If non-nil, show the REPL window when Idris starts.
+If nil, only do this when `idris-repl' was called interactively."
:type 'boolean
:group 'idris-repl)
diff --git a/idris-simple-indent.el b/idris-simple-indent.el
index 173e131a2c..22c15b978c 100644
--- a/idris-simple-indent.el
+++ b/idris-simple-indent.el
@@ -84,7 +84,7 @@ Takes into account literate Idris syntax."
(length (match-string 0))))
(defun idris-simple-indent-indent-line-to (column)
- "Just like `indent-line-to`, but ignoring the leading > for literate Idris"
+ "Just like `indent-line-to`, but ignoring the leading > for literate Idris."
(if (idris-lidr-p)
(if (save-excursion (move-to-column 0) (looking-at ">")) ;; lidr code
line - look out for >
(progn
@@ -99,7 +99,7 @@ Takes into account literate Idris syntax."
(indent-line-to column))) ;; not lidr, do normal indent
(defun idris-simple-indent-tab-to-tab-stop ()
- "A version of `tab-to-tab-stop' that takes literate Idris into account"
+ "A version of `tab-to-tab-stop' that takes literate Idris into account."
(let ((indent (idris-simple-indent-current-indentation))
(stops tab-stop-list)
indent-to)
@@ -125,7 +125,7 @@ column, `tab-to-tab-stop' is done instead."
(skip-chars-forward " "))
;; otherwise we're in code - do code indenting
(let* ((start-column (current-column))
- (invisible-from nil) ; `nil' means infinity here
+ (invisible-from nil) ; nil means infinity here
(indent
(catch 'idris-simple-indent-break
(save-excursion
diff --git a/idris-syntax.el b/idris-syntax.el
index 2d0d940e30..547070422f 100644
--- a/idris-syntax.el
+++ b/idris-syntax.el
@@ -95,7 +95,7 @@ contributing the settings upstream to the theme maintainer."
(defface idris-unsafe-face
'((t (:inherit font-lock-warning-face)))
- "The face used to highlight unsafe Idris features, such as %assert_total"
+ "The face used to highlight unsafe Idris features, such as %assert_total."
:group 'idris-faces)
@@ -198,7 +198,7 @@ syntax table won't support, such as characters."
(regexp-opt (append idris-definition-keywords
idris-keywords)
'words)
- "A regexp for matching Idris keywords")
+ "A regexp for matching Idris keywords.")
(defun idris-font-lock-literate-search (regexp lidr limit)
"Find REGEXP in Idris source between point and LIMIT.
diff --git a/idris-tree-info.el b/idris-tree-info.el
index 8121658358..89ac134891 100644
--- a/idris-tree-info.el
+++ b/idris-tree-info.el
@@ -35,8 +35,7 @@
(require 'idris-warnings-tree)
(defvar idris-tree-info-buffer-name (idris-buffer-name :tree-viewer)
- "The name of the buffer that `idris-mode' uses to show general
-tree-structured command output.")
+ "The buffer used to show general, tree-structured command output.")
(defun idris-tree-info-quit ()
"Quit the Idris tree info viewer."
@@ -57,14 +56,14 @@ tree-structured command output.")
map))
(easy-menu-define idris-tree-info-mode-menu idris-tree-info-mode-map
- "Menu for the Idris tree viewer buffer"
+ "Menu for the Idris tree viewer buffer."
`("Idris Tree Viewer"
["Show term interaction widgets" idris-add-term-widgets t]
["Close Idris tree viewer buffer" idris-tree-info-quit t]))
(define-derived-mode idris-tree-info-mode fundamental-mode "Idris Tree"
- "Major mode used for transient Idris tree viewers
- \\{idris-tree-info-mode-map}
+ "Major mode used for transient Idris tree viewers.
+\\{idris-tree-info-mode-map}
Invokes `idris-tree-info-mode-hook'.
This mode should be used to display tree-structured output,
diff --git a/idris-warnings-tree.el b/idris-warnings-tree.el
index 2236e8b417..999fb49aac 100644
--- a/idris-warnings-tree.el
+++ b/idris-warnings-tree.el
@@ -1,4 +1,4 @@
-;;; idris-warnings-tree.el --- Tree view of warnings reported by idris in
buffers -*- lexical-binding: t -*-
+;;; idris-warnings-tree.el --- Tree view of warnings reported by Idris in
buffers -*- lexical-binding: t -*-
;; Copyright (C) 2014 Hannes Mehnert
@@ -94,7 +94,6 @@
(interactive)
(idris-kill-buffer idris-notes-buffer-name))
-
(define-derived-mode idris-compiler-notes-mode special-mode "Compiler-Notes"
"Major mode for displaying Idris compiler notes.
\\{idris-compiler-notes-mode-map}
@@ -112,7 +111,7 @@ Invokes `idris-compiler-notes-mode-hook'."
(idris-goto-source-location (nth 0 note) (nth 1 note) (nth 2
note))))))
(defun idris-goto-location (filename)
- "Opens buffer for filename"
+ "Opens buffer for FILENAME."
(let ((fullpath (concat (file-name-as-directory
idris-process-current-working-directory)
filename)))
(or (get-buffer filename)
@@ -120,9 +119,10 @@ Invokes `idris-compiler-notes-mode-hook'."
(find-file-noselect fullpath))))
(defun idris-goto-source-location (filename lineno col)
- "Move to the source location FILENAME LINENO COL. If the buffer
-containing the file is narrowed and the location is hidden, show
-a preview and offer to widen."
+ "Move to the source location FILENAME LINENO COL.
+
+If the buffer containing the file is narrowed and the location is hidden,
+show a preview and offer to widen."
(let ((buf (idris-goto-location filename)))
(set-buffer buf)
(pop-to-buffer buf t)
@@ -145,11 +145,10 @@ a preview and offer to widen."
(when widen-p (widen))
(goto-char new-location)))))
-
;;;;;; Tree Widget
(cl-defmacro with-struct ((conc-name &rest slots) struct &body body)
- "Like with-slots but works only for structs.
+ "Like `with-slots' but works only for structs.
\(fn (CONC-NAME &rest SLOTS) STRUCT &body BODY)"
(declare (indent 2))
(let ((struct-var (gensym "struct")))
@@ -179,7 +178,7 @@ a preview and offer to widen."
(preserve-properties '() :type list))
(defun idris-tree-leaf-p (tree)
- ;; Evaluate the kids to see if we are at a leaf
+ "Evaluate the kids of TREE to see if we are at a leaf."
(when (functionp (idris-tree.kids tree))
(setf (idris-tree.kids tree) (funcall (idris-tree.kids tree))))
(cl-assert (listp (idris-tree.kids tree)))
diff --git a/idris-warnings.el b/idris-warnings.el
index db989384d9..1d98971e92 100644
--- a/idris-warnings.el
+++ b/idris-warnings.el
@@ -1,4 +1,4 @@
-;;; idris-warnings.el --- Mark warnings reported by idris in buffers -*-
lexical-binding: t -*-
+;;; idris-warnings.el --- Mark warnings reported by Idris in buffers -*-
lexical-binding: t -*-
;; Copyright (C) 2013 Hannes Mehnert
@@ -35,9 +35,9 @@
"Face for warnings from the compiler."
:group 'idris-faces)
-(defvar idris-warnings-buffers '() "All buffers which have warnings")
-(defvar-local idris-warnings '() "All warnings in the current buffer")
-(defvar idris-raw-warnings '() "All warnings from Idris")
+(defvar idris-warnings-buffers '() "All buffers which have warnings.")
+(defvar-local idris-warnings '() "All warnings in the current buffer.")
+(defvar idris-raw-warnings '() "All warnings from Idris.")
(defun idris-warning-event-hook-function (event)
(pcase event
diff --git a/inferior-idris.el b/inferior-idris.el
index 4ee0cb9421..17fd79574c 100644
--- a/inferior-idris.el
+++ b/inferior-idris.el
@@ -81,8 +81,8 @@
t)))
(defvar-local idris-load-packages nil
- "The list of packages to be loaded by Idris. Set using file or
-directory variables.")
+ "The list of packages to be loaded by Idris.
+Set using file or directory variables.")
(defun idris-compute-flags ()
"Calculate the command line options to use when running Idris."
@@ -94,8 +94,8 @@ directory variables.")
idris-command-line-option-functions)))
(defvar idris-current-flags nil
- "The list of command-line-args actually passed to Idris. This
- is maintained to restart Idris when the arguments change.")
+ "The list of `command-line-args' actually passed to Idris.
+This is maintained to restart Idris when the arguments change.")
(autoload 'idris-prover-event-hook-function "idris-prover.el")
(autoload 'idris-quit "idris-commands.el")
@@ -134,7 +134,7 @@ directory variables.")
(accept-process-output idris-process 3))))
(defun idris-connect (port)
- "Establish a connection with a Idris REPL."
+ "Establish a connection with a Idris REPL at PORT."
(when (not idris-connection)
(setq idris-connection
(open-network-stream "Idris IDE support"
idris-connection-buffer-name "127.0.0.1" port))
@@ -170,9 +170,9 @@ directory variables.")
(defvar idris-process-port-output-regexp (rx (? (group (+ any (not num))))
(group (+ (any num))))
"Regexp used to match the port of an Idris process.")
(defvar idris-process-exact-port-output-regexp (rx bol (group (+ (any num)))
eol)
- "Regexp to match port number")
+ "Regexp to match port number.")
(defvar idris-exact-port-matcher 1
- "port number matcher")
+ "Port number matcher.")
(defvar idris-process-port-with-warning-output-regexp
(rx (? (group (+ any (not num)))) (group (** 3 4 (any num)))))
@@ -182,14 +182,14 @@ directory variables.")
;; | +---- port number
;; +------------------------------- warning message
(defvar idris-warning-matcher 1
- "Warning from idris")
-(defvar idris-warning-port-matcher 2
- "port number matcher with warning")
+ "Warning from Idris.")
+(defvar idris-warning-port-matcher 2
+ "Port number matcher with warning.")
;; idris-process-filter is broken in theoreticaly.
(defun idris-process-filter (string)
- "Accept output from the process"
+ "Accept STRING output from the process."
(if idris-connection
string
;; Idris sometimes prints a warning prior to the port number, which causes
@@ -211,14 +211,14 @@ directory variables.")
(pop-to-buffer (get-buffer idris-process-buffer-name))))
(defun idris-output-filter (process string)
- "Accept output from the socket and process all complete messages"
+ "Accept STRING output from the socket and PROCESS all complete messages."
(with-current-buffer (process-buffer process)
(goto-char (point-max))
(insert string))
(idris-connection-available-input process))
(defun idris-connection-available-input (process)
- "Process all complete messages which arrived from Idris."
+ "Process all complete messages which arrived from Idris PROCESS."
(with-current-buffer (process-buffer process)
(while (idris-have-input-p)
(let ((event (idris-receive)))
@@ -234,7 +234,7 @@ directory variables.")
(>= (- (buffer-size) 6) (idris-decode-length))))
(defun idris-receive ()
- "Read a message from the idris process"
+ "Read a message from the Idris process."
(goto-char (point-min))
(let* ((length (idris-decode-length))
(start (+ 6 (point)))
@@ -257,7 +257,7 @@ directory variables.")
(process-send-string proc string)))
(defun idris-encode-length (n)
- "Encode an integer into a 24-bit hex string."
+ "Encode an N (integer) into a 24-bit hex string."
(format "%06x" n))
(defun idris-prin1-to-string (sexp)
@@ -271,10 +271,9 @@ directory variables.")
(buffer-string))))
(defvar idris-rex-continuations '()
- "List of (ID FUNCTION [FUNCTION]) continuations waiting for RPC
- results. The first function will be called with a final result,
- and the second (if present) will be called with intermediate
- output results.")
+ "List of (ID FUNCTION [FUNCTION]) continuations waiting for RPC results.
+The first function will be called with a final result, and the second
+ (if present) will be called with intermediate output results.")
(defvar idris-continuation-counter 1
"Continuation serial number counter.")
@@ -306,7 +305,7 @@ directory variables.")
(cl-defmacro idris-rex ((&rest saved-vars) sexp intermediate &rest
continuations)
"(idris-rex (VAR ...) (SEXP) INTERMEDIATE CLAUSES ...)
-Remote EXecute SEXP.
+Remote Execute SEXP.
VARs are a list of saved variables visible in the other forms. Each
VAR is either a symbol or a list (VAR INIT-VALUE).
@@ -341,8 +340,7 @@ versions cannot deal with that."
idris-connection))))
(defun idris-eval-async (sexp cont &optional failure-cont)
- "Evaluate EXPR on the superior Idris and call CONT with the result,
-or FAILURE-CONT in failure case."
+ "Evaluate SEXP on the superior Idris and call CONT or FAILURE-CONT."
(idris-rex (cont (buffer (current-buffer)) failure-cont)
sexp t
((:ok result)
@@ -365,12 +363,11 @@ or FAILURE-CONT in failure case."
(autoload 'idris-list-compiler-notes "idris-commands.el")
(defun idris-eval (sexp &optional no-errors)
- "Evaluate EXPR on the inferior Idris and return the result,
-ignoring intermediate output. If `NO-ERRORS' is non-nil, don't
-trigger warning buffers and don't call `ERROR' if there was an
-Idris error."
+ "Evaluate SEXP on the inferior Idris and return the result.
+If `NO-ERRORS' is non-nil, don't trigger warning buffers and
+ don't call `ERROR' if there was an Idris error."
(let* ((tag (gensym (format "idris-result-%d-"
- (1+ idris-continuation-counter))))
+ (1+ idris-continuation-counter))))
(idris-stack-eval-tags (cons tag idris-stack-eval-tags)))
(apply
#'funcall
diff --git a/readme.markdown b/readme.markdown
index fdbd19182f..691877f79d 100644
--- a/readme.markdown
+++ b/readme.markdown
@@ -55,12 +55,12 @@ Certain areas of `idris-mode` show explanatory help text.
When you've learned ho
There is now support for running an Idris interpreter in a buffer. Use
`C-c C-l` to load the current Idris buffer into the interpreter. This will
-spawn an inferior idris process and load the buffer. It will report warnings
+spawn an inferior Idris process and load the buffer. It will report warnings
if idris reports any. Pressing `C-c C-l` again will reload that buffer - if you
switch to a different buffer and press `C-c C-l`, that buffer will be loaded
instead.
-Customize `idris-interpreter-path` if idris is not on your default path.
+Customize `idris-interpreter-path` if Idris is not on your default path.
[Idris]: http://www.idris-lang.org
@@ -253,7 +253,7 @@ Throughout a session with `idris-mode`, many frames will
accumulate, such as `*i
;; This makes it so that especially errors reuse their frames
;;
https://emacs.stackexchange.com/questions/327/how-can-i-block-a-frame-from-being-split/338
;; alternatively, add this to certain frames: (set-frame-parameter nil
'unsplittable t)
- ;; (without this, idris throws out tons of new frames)
+ ;; (without this, Idris throws out tons of new frames)
(add-to-list 'display-buffer-alist
'(".*". (display-buffer-reuse-window . ((reusable-frames .
t)))))
(setq idris-stay-in-current-window-on-compiler-error t)
