aboutsummaryrefslogtreecommitdiff
path: root/generic
diff options
context:
space:
mode:
Diffstat (limited to 'generic')
-rw-r--r--generic/proof-script.el5
-rw-r--r--generic/proof-shell.el3
2 files changed, 6 insertions, 2 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el
index e9b05d2a..7f248dba 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -729,8 +729,9 @@ the next command end."
alist)))
(defun proof-semis-to-vanillas (semis &optional callback-fn)
- "Convert a sequence of semicolon positions (returned by the above
-function) to a set of vanilla extents."
+ "Convert a sequence of terminator positions to a set of vanilla extents.
+Proof terminator positions SEMIS has the form returned by
+the function proof-segment-up-to."
(let ((ct (proof-unprocessed-begin)) span alist semi)
(while (not (null semis))
(setq semi (car semis)
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 1216e337..996ffa65 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -795,6 +795,9 @@ assistant."
;; FIXME: note: removed optional 'relaxed' arg
(defun proof-start-queue (start end alist)
+ "Begin processing a queue of commands in ALIST.
+If START is non-nil, START and END are buffer positions in the
+active scripting buffer for the queue region."
(if start
(proof-set-queue-endpoints start end))
(let (item)