diff options
| -rw-r--r-- | generic/proof-script.el | 5 | ||||
| -rw-r--r-- | generic/proof-shell.el | 3 | ||||
| -rw-r--r-- | isa/thy-mode.el | 13 |
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) |