diff options
| -rw-r--r-- | generic/proof-script.el | 6 | ||||
| -rw-r--r-- | generic/proof-shell.el | 50 | ||||
| -rw-r--r-- | generic/proof-utils.el | 2 | ||||
| -rw-r--r-- | generic/span-overlay.el | 2 |
4 files changed, 31 insertions, 29 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 184f0bfd..97528be8 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1357,7 +1357,7 @@ With ARG, turn on scripting iff ARG is positive." (savestart (span-start span)) (saveend (span-end span)) (cmd (span-property span 'cmd)) - lev nestedundos nam next ncmd) + lev nestedundos nam next) ;; Try to set the name of the theorem from the save ;; (message "%s" cmd) 3.4: remove this message. @@ -1745,7 +1745,7 @@ to the function which parses the script segment by segment." (defun proof-cmdstart-add-segment-for-cmd (comstart prev) (let ((tmp (point)) (commentre (concat "[ \t\n]*" proof-script-comment-start-regexp)) - (commentend (concat proof-script-comment-end-regexp "[ \t\n]*" ))) + (commentend (concat proof-script-comment-end-regexp "[ \t\n]*" ))) ;; FIXME: used? ;; Find end of previous command... (goto-char comstart) ;; Special hack: terminal char is included in a command, if set. @@ -1806,7 +1806,7 @@ which continues past POS, if any. (NOT IMPLEMENTED IN THIS VERSION). This version is used when `proof-script-command-start-regexp' is set." (save-excursion - (let* (alist prev cmdfnd startpos comstart first) + (let* (alist prev cmdfnd startpos comstart) (goto-char (proof-queue-or-locked-end)) (setq prev (point)) (skip-chars-forward " \t\n") diff --git a/generic/proof-shell.el b/generic/proof-shell.el index f6bd446c..8dc26f9a 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -113,6 +113,32 @@ to examine proof-shell-last-output.") ;; +;; Indicator and fake minor mode for active scripting buffer +;; + +(defcustom proof-shell-active-scripting-indicator + (if proof-running-on-XEmacs + (cons (make-extent nil nil) " Scripting ") + " Scripting") + "Modeline indicator for active scripting buffer. +If first component is extent it will automatically follow the colour +of the queue region." + :type 'sexp + :group 'proof-general-internals) + +(unless + (assq 'proof-active-buffer-fake-minor-mode minor-mode-alist) + (setq minor-mode-alist + (append minor-mode-alist + (list + (list + 'proof-active-buffer-fake-minor-mode + proof-shell-active-scripting-indicator))))) + + + + +;; ;; Implementing the process lock ;; ;; da: In fact, there is little need for a lock. Since Emacs Lisp @@ -357,30 +383,6 @@ Does nothing if proof assistant is already running." ;; -;; Indicator and fake minor mode for active scripting buffer -;; - -(defcustom proof-shell-active-scripting-indicator - (if proof-running-on-XEmacs - (cons (make-extent nil nil) " Scripting ") - " Scripting") - "Modeline indicator for active scripting buffer. -If first component is extent it will automatically follow the colour -of the queue region." - :type 'sexp - :group 'proof-general-internals) - -(unless - (assq 'proof-active-buffer-fake-minor-mode minor-mode-alist) - (setq minor-mode-alist - (append minor-mode-alist - (list - (list - 'proof-active-buffer-fake-minor-mode - proof-shell-active-scripting-indicator))))) - - -;; ;; Shutting down proof shell and associated buffers ;; diff --git a/generic/proof-utils.el b/generic/proof-utils.el index 39416c27..dab732e2 100644 --- a/generic/proof-utils.el +++ b/generic/proof-utils.el @@ -580,7 +580,7 @@ No action if BUF is nil or killed." ;; that gives much nicer behaviour than XEmacs here. (display-buffer buf 'not-this-window) (let ((pop-up-windows t)) - (pg-pop-to-buffer buffer 'not-this-window 'norecord)))))) + (pg-pop-to-buffer buf 'not-this-window 'norecord)))))) ;; Originally based on `shrink-window-if-larger-than-buffer', which diff --git a/generic/span-overlay.el b/generic/span-overlay.el index 1e910baa..08da16b3 100644 --- a/generic/span-overlay.el +++ b/generic/span-overlay.el @@ -285,7 +285,7 @@ A span is before PT if it covers the character before PT." (1+ start) (point-max))) (resstart (1+ (point-max))) - spanres newres) + spanres) ;; overlays are returned in an unspecified order; we ;; must search whole list for a closest-next one. (dolist (newres nextos spanres) |