Replace proof-locked-end -> proof-unprocessed-begin

9 files changed, 25 insertions, 35 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 0101ce04..c7b8bebf 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -291,7 +291,7 @@ used see coq-set-state-number. Initially 1 because Coq initial state has number
 (defun proof-last-locked-span ()
   (save-excursion ;; didn't found a way to avoid buffer switching
     (set-buffer proof-script-buffer)
-    (span-at (- (proof-locked-end) 1) 'type)
+    (span-at (- (proof-unprocessed-begin) 1) 'type)
     )
   )
 
@@ -1298,7 +1298,7 @@ buffer."
       (let ((pos (car mtch))
             (lgth (cadr mtch)))
         (set-buffer proof-script-buffer)
-        (goto-char (+ (proof-locked-end) 1))
+        (goto-char (+ (proof-unprocessed-begin) 1))
         (coq-find-real-start)
 
         ; utf8 adaptation is made in coq-get-last-error-location above
diff --git a/generic/pg-autotest.el b/generic/pg-autotest.el
index 994247cf..2aef7df8 100644
--- a/generic/pg-autotest.el
+++ b/generic/pg-autotest.el
@@ -1,6 +1,6 @@
 ;;; pg-autotest.el --- Simple testing framework for Proof General
 ;;
-;; Copyright (C) 2005 LFCS Edinburgh, David Aspinall.
+;; Copyright (C) 2005, 2009 LFCS Edinburgh, David Aspinall.
 ;; Authors:   David Aspinall
 ;;
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
@@ -67,7 +67,7 @@ An error is signalled if scripting doesn't complete."
   (save-excursion
     (let ((making-progress t) last-locked-end)
       (while making-progress
-	(setq last-locked-end (proof-locked-end))
+	(setq last-locked-end (proof-unprocessed-begin))
 	(goto-char last-locked-end)
 	(save-current-buffer
 	  (proof-assert-next-command-interactive)
diff --git a/generic/pg-pbrpm.el b/generic/pg-pbrpm.el
index 094b18b6..bee0ea05 100644
--- a/generic/pg-pbrpm.el
+++ b/generic/pg-pbrpm.el
@@ -344,7 +344,7 @@ The prover command is processed via pg-pbrpm-run-command."
      ;;   (proof-goto-end-of-locked)
      ;;   (proof-activate-scripting nil 'advancing)
      ;;   (insert (concat "\n" command))
-     ;;   (setq span (span-make (proof-locked-end) (point)))
+     ;;   (setq span (span-make (proof-unprocessed-begin) (point)))
      ;;  ; TODO : define the following properties for PBRPM, I don't understand their use ...
      ;;   (span-set-property span 'type 'pbp)
      ;;   (span-set-property span 'cmd command)
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 0a6a2522..198f7fe9 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -43,13 +43,13 @@
 Assumes that point is at the end of a command."
   (interactive)
 ; FIXME: pending improvement.2, needs a fix here.
-;  (if (eq (proof-locked-end) (point))
+;  (if (eq (proof-unprocessed-begin) (point))
 ;      ;; A hack to fix problem that the locked span
 ;      ;; is [ ) so sometimes inserting at the end
 ;      ;; tries to extend it, giving "read only" error.
-;      (if (> (point-max) (proof-locked-end))
+;      (if (> (point-max) (proof-unprocessed-begin))
 ;	  (progn
-;	    (goto-char (1+ (proof-locked-end)))
+;	    (goto-char (1+ (proof-unprocessed-begin)))
 ;	    (backward-char))))
   (if proof-one-command-per-line
       ;; One command per line: move to next new line, creating one if
@@ -123,7 +123,7 @@ Assumes script buffer is current."
 	(if (nth 2 semis) ; fetch end point of previous command
 	      (goto-char (nth 2 semis))
 	  ;; no previous command: just next to end of locked
-	  (goto-char (proof-locked-end)))))
+	  (goto-char (proof-unprocessed-begin)))))
     ;; Oddities of this function: if we're beyond the last proof
     ;; command, it jumps back to the last command.  Could alter this
     ;; by spotting that command end of last of semis is before
@@ -228,7 +228,7 @@ the proof script."
    (let (lastspan)
      (save-excursion
        (unless (proof-locked-region-empty-p)
-	 (if (setq lastspan (span-at-before (proof-locked-end) 'type))
+	 (if (setq lastspan (span-at-before (proof-unprocessed-begin) 'type))
 	     (progn
 	       (goto-char (span-start lastspan))
 	       (proof-retract-until-point delete))
@@ -344,11 +344,11 @@ a proof command."
     (error "Must be in the active scripting buffer"))
    ;; Sometimes may need to move point forwards, when locked region
    ;; is editable.
-   ;; ((> (point) (proof-locked-end))
+   ;; ((> (point) (proof-unprocessed-begin))
    ;; (error "You can only move point backwards"))
    ;; FIXME da: should move to a command boundary, really!
    (t (proof-set-locked-end (point))
-      (span-delete-spans (proof-locked-end) (point-max) 'type))))
+      (span-delete-spans (proof-unprocessed-begin) (point-max) 'type))))
 
 
 
diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el
index 449755ec..1bbcc702 100644
--- a/generic/proof-autoloads.el
+++ b/generic/proof-autoloads.el
@@ -536,7 +536,7 @@ in future if we have just activated it for this buffer.
 ;;;### (autoloads (proof-config-done proof-mode proof-insert-sendback-command
 ;;;;;;  proof-insert-pbp-command proof-register-possibly-new-processed-file
 ;;;;;;  pg-set-span-helphighlights proof-locked-region-empty-p proof-locked-region-full-p
-;;;;;;  proof-locked-end proof-unprocessed-begin proof-colour-locked)
+;;;;;;  proof-unprocessed-begin proof-unprocessed-begin proof-colour-locked)
 ;;;;;;  "proof-script" "proof-script.el" (19127 27615))
 ;;; Generated autoloads from proof-script.el
 
@@ -551,7 +551,7 @@ The position is actually one beyond the last locked character.
 
 \(fn)" nil nil)
 
-(autoload (quote proof-locked-end) "proof-script" "\
+(autoload (quote proof-unprocessed-begin) "proof-script" "\
 Return end of the locked region of the current buffer.
 Only call this from a scripting buffer.
 
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 405b700e..1f46212e 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -537,7 +537,7 @@ settings `proof-non-undoables-regexp' and
 This setting is used to for retraction (undoing) in proof scripts.
 
 It should undo the effect of all settings between its target span
-up to (proof-locked-end).  This may involve forgetting a number
+up to (proof-unprocessed-begin).  This may involve forgetting a number
 of definitions, declarations, or whatever.
 
 If return value is nil, it means there is nothing to do.
diff --git a/generic/proof-indent.el b/generic/proof-indent.el
index 1d00cf81..fc035aea 100644
--- a/generic/proof-indent.el
+++ b/generic/proof-indent.el
@@ -77,7 +77,7 @@
   "Indent current line of proof script, if indentation enabled."
   (interactive)
   (unless (not (proof-ass script-indent))
-	  (if (< (point) (proof-locked-end))
+	  (if (< (point) (proof-unprocessed-begin))
 	      (if (< (current-column) (current-indentation))
 		  (skip-chars-forward "\t "))
 	    (save-excursion
diff --git a/generic/proof-script.el b/generic/proof-script.el
index cc53f3bb..66d101fc 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -313,7 +313,7 @@ caused the error.  Go to the start of it if `proof-follow-mode' is
 'locked.
 
 This is a subroutine used in proof-shell-handle-{error,interrupt}."
-    (let ((start (proof-locked-end))
+    (let ((start (proof-unprocessed-begin))
 	  (end   (proof-queue-or-locked-end))
 	  (infop (span-live-p badspan)))
       (proof-detach-queue)
@@ -356,7 +356,7 @@ The position is actually one beyond the last locked character."
 
 (defun proof-script-end ()
   "Return the character beyond the last non-whitespace character.
-This is the same position `proof-locked-end' ends up at when asserting
+This is the same position `proof-unprocessed-begin' ends up at when asserting
 the script.  Works for any kind of buffer."
   (save-excursion
     (goto-char (point-max))
@@ -374,16 +374,6 @@ when a queue of commands is being processed."
    (and proof-locked-span (span-end proof-locked-span))
    (point-min)))
 
-;; FIXME: get rid of/rework this function.  Some places expect this to
-;; return nil if locked region is empty. Moreover, it confusingly
-;; returns the point past the end of the locked region.
-;;;###autoload
-(defun proof-locked-end ()
-  "Return end of the locked region of the current buffer.
-Only call this from a scripting buffer."
-  (proof-unprocessed-begin))
-
-
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -472,7 +462,7 @@ Intended as a hook function for `proof-shell-handle-error-or-interrupt-hook'."
 (defun proof-end-of-locked-visible-p ()
   "Return non-nil if end of locked region is visible."
   (let* ((pos (proof-with-current-buffer-if-exists proof-script-buffer
-		(proof-locked-end)))
+		(proof-unprocessed-begin)))
 	 (win (and pos (get-buffer-window proof-script-buffer t))))
     (and win (pos-visible-in-window-p pos))))
 
@@ -1864,7 +1854,7 @@ When used in the locked region (and so with strict read only off), it
 always defaults to inserting a semi (nicer might be to parse for a
 comment, and insert or skip to the next semi)."
   (let ((mrk (point)) ins incomment)
-    (if (< mrk (proof-locked-end))
+    (if (< mrk (proof-unprocessed-begin))
 	(insert proof-terminal-char) ; insert immediately in locked region
       (if (proof-only-whitespace-to-locked-region-p)
 	  (error "There's nothing to do!"))
@@ -1945,7 +1935,7 @@ No effect if prover is busy."
     (proof-goto-end-of-locked)
     (if proof-one-command-per-line (insert "\n"))
     (insert cmd)
-    (setq span (span-make (proof-locked-end) (point)))
+    (setq span (span-make (proof-unprocessed-begin) (point)))
     (span-set-property span 'type 'pbp)
     (span-set-property span 'cmd cmd)
     (proof-start-queue (proof-unprocessed-begin) (point)
@@ -2027,7 +2017,7 @@ Span deletion property set to flag DELETE-REGION."
 (defun proof-last-goal-or-goalsave ()
   "Return the span which is the last goal or save before point."
   (save-excursion
-    (let ((span (span-at-before (proof-locked-end) 'type)))
+    (let ((span (span-at-before (proof-unprocessed-begin) 'type)))
       (while (and span
 		  (not (eq (span-property span 'type) 'goalsave))
 		  (or (eq (span-property span 'type) 'proof)
@@ -2121,7 +2111,7 @@ up to the end of the locked region."
 			      (funcall proof-find-and-forget-fn target)
 			      delete-region))))
 
-    (proof-start-queue (min start end) (proof-locked-end) actions)))
+    (proof-start-queue (min start end) (proof-unprocessed-begin) actions)))
 
 ;; FIXME da:  I would rather that this function moved point to
 ;; the start of the region retracted?
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 3004c811..71099176 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1045,10 +1045,10 @@ and indentation.  Assumes proof-script-buffer is active."
 	;; a unit, i.e. sent to the proof assistant together.
 	;; FIXME da: this seems very similar to proof-insert-pbp-command
 	;; in proof-script.el.  Should be unified, I suspect.
-	(setq span (span-make (proof-locked-end) (point)))
+	(setq span (span-make (proof-unprocessed-begin) (point)))
 	(span-set-property span 'type 'pbp)
 	(span-set-property span 'cmd cmd)
-	(proof-set-queue-endpoints (proof-locked-end) (point))
+	(proof-set-queue-endpoints (proof-unprocessed-begin) (point))
 	(setq proof-action-list
 	      (cons (car proof-action-list)
 		    (cons (list span cmd 'proof-done-advancing)