Docstring fixes

3 files changed, 15 insertions, 6 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)
diff --git a/isa/thy-mode.el b/isa/thy-mode.el
index 9e47231f..864a31cf 100644
--- a/isa/thy-mode.el
+++ b/isa/thy-mode.el
@@ -21,7 +21,7 @@
   :group 'thy)
 
 (defcustom thy-indent-level 2
-  "Indentation level for Isabelle theory files."
+  "Indentation level for Isabelle theory files.  An integer."
   :type  'integer
   :group 'thy)
 
@@ -33,7 +33,10 @@ any of the usual bracket characters in unusual ways."
   :group 'thy)
 
 (defcustom thy-use-sml-mode nil
-  "*If non-nil, invoke sml-mode inside \"ML\" section of theory files."
+  "*If non-nil, invoke sml-mode inside \"ML\" section of theory files.
+This option is left-over from Isamode.  Really, it would be more
+useful if the script editing mode of Proof General itself could be based 
+on sml-mode, but at the moment there is no way to do this."
   :type 'boolean
   :group 'thy)
 
@@ -430,8 +433,10 @@ Here is the full list of theory mode key bindings:
 
 (defun thy-find-other-file (&optional samewindow)
   "Find associated .ML or .thy file.
-If SAMEWINDOW is non-nil (prefix argument when called interactively),
-use find-file instead of find-file-other-window."
+Finds and switch to the associated ML file (when editing a theory file)
+or theory file (when editing an ML file).  
+If SAMEWINDOW is non-nil (interactively, with an optional argument)
+the other file replaces the one in the current window."
   (interactive "p")
   (and 
    (buffer-file-name)