Add input history ring. Cleanup comments.

2 files changed, 271 insertions, 63 deletions

diff --git a/generic/pg-user.el b/generic/pg-user.el
index dee6922e..80794058 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -171,7 +171,7 @@ handling of interrupt signals."
 ;; Movement commands
 ;;
 
-;; FIXME da: the next function is messy.  Also see notes in 'todo'
+;; TODO da: the next function is messy.
 (defun proof-goto-command-start ()
   "Move point to start of current (or final) command of the script."
   (interactive)
@@ -221,7 +221,7 @@ handling of interrupt signals."
 ;; be nicer behaviour than actually moving point into locked region
 ;; which is only useful for cut and paste, really.
 (defun proof-mouse-goto-point (event)
-  "Call proof-goto-point on the click position."
+  "Call proof-goto-point on the click position EVENT."
   (interactive "e")
   (proof-maybe-save-point
    (mouse-set-point event)
@@ -237,7 +237,7 @@ handling of interrupt signals."
 ;; Maybe by setting some of the mouse track hooks.
 ;; TODO: mouse-track-insert is XEmacs specific anyway.
 (defun proof-mouse-track-insert (event)
-  "Copy highlighted command under the mouse to point.  Ignore comments.
+  "Copy highlighted command under mouse EVENT to point.  Ignore comments.
 If there is no command under the mouse, behaves like mouse-track-insert."
   (interactive "e")
   (let ((str
@@ -276,7 +276,7 @@ If there is no command under the mouse, behaves like mouse-track-insert."
   "History of proof commands read from the minibuffer.")
 
 (defun proof-minibuffer-cmd (cmd)
-  "Prompt for a command in the minibuffer and send it to proof assistant.
+  "Send CMD to proof assistant.  Interactively, read from minibuffer.
 The command isn't added to the locked region.
 
 If a prefix arg is given and there is a selected region, that is
@@ -342,7 +342,7 @@ a proof command."
    ;; Sometimes may need to move point forwards, when locked region
    ;; is editable.
    ;; ((> (point) (proof-locked-end))
-   ;; (error "You can only move point backwards."))
+   ;; (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))))
@@ -351,38 +351,6 @@ a proof command."
 
 
 
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; command history  (unfinished)
-;;
-;; da: below functions for input history simulation are quick hacks.
-;; Could certainly be made more efficient.
-
-;(defvar proof-command-history nil
-;  "History used by proof-previous-matching-command and friends.")
-
-;(defun proof-build-command-history ()
-;  "Construct proof-command-history from script buffer.
-;Based on position of point."
-;  ;; let
-;  )
-
-;(defun proof-previous-matching-command (arg)
-;  "Search through previous commands for new command matching current input."
-;  (interactive))
-;  ;;(if (not (memq last-command '(proof-previous-matching-command
-;  ;; proof-next-matching-command)))
-;      ;; Start a new search
-      
-;(defun proof-next-matching-command (arg)
-;  "Search through following commands for new command matching current input."
-;  (interactive "p")
-;  (proof-previous-matching-command (- arg)))
-
-;;
-;; end command history stuff
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 	  
 
 
@@ -425,7 +393,7 @@ a proof command."
 
 ;;;###autoload
 (defmacro proof-define-assistant-command (fn doc cmdvar &optional body)
-  "Define command FN to send string BODY to proof assistant, based on CMDVAR.
+  "Define FN (docstring DOC) to send BODY to prover, based on CMDVAR.
 BODY defaults to CMDVAR, a variable."
   `(defun ,fn ()
      ,(concat doc
@@ -618,7 +586,7 @@ comment, and insert or skip to the next semi)."
 
 (defun proof-electric-terminator ()
   "Insert the terminator, perhaps sending the command to the assistant.
-If proof-electric-terminator-enable is non-nil, the command will be
+If `proof-electric-terminator-enable' is non-nil, the command will be
 sent to the assistant."
   (interactive)
   (if proof-electric-terminator-enable
@@ -812,7 +780,7 @@ If NUM is negative, move upwards.  Return new span."
 	    (let ((new-span
 		   (span-at insertpos 'type)));should be one we deleted.
 	      (span-set-property new-span 'children
-				 (pg-fixup-children-spans 
+				 (pg-fixup-children-spans
 				  new-span insertpos (point)))
 	      (span-set-end proof-locked-span lockedend)
 	      (undo-boundary)
@@ -820,7 +788,7 @@ If NUM is negative, move upwards.  Return new span."
 
 (defun pg-fixup-children-spans (new-parent start end)
   (append
-   (span-mapcar-spans 
+   (span-mapcar-spans
     (lambda (span)
       (if (span-property span 'controlspan)
 	  (progn
@@ -1155,5 +1123,240 @@ The function `substitute-command-keys' is called on the argument."
 	      (use-local-map oldkeymap)))
 	(remove-hook 'menu-bar-update-hook 'imenu-update-menubar)))))
 
+
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Command history  (added in PG 3.7)
+;;
+;; This implements a history ring for commands in the locked region.
+;; Inspired by (and code heavily copied from) comint in XEmacs.
+;;
+;; The current behaviour is not ideal: we only extend the input ring as
+;; we process (so history does not browse pink text while the
+;; prover is busy).  Moreover, instead of using a history, we might
+;; simply parse commands backwards (or forwards) in the buffer.
+;; (i.e, more like the copying behaviour implemented in Bibtex mode).
+;;
+
+(defvar pg-input-ring nil
+  "Ring of previous inputs")
+
+(defvar pg-input-ring-index nil
+  "Position of last matched command")
+
+(defvar pg-stored-incomplete-input nil
+  "Stored incomplete input: string between point and locked")
+
+(defun pg-previous-input (arg)
+  "Cycle backwards through input history, saving input."
+  (interactive "*p")
+  (if (and pg-input-ring-index
+	   (or		       ;; leaving the "end" of the ring
+	    (and (< arg 0)		; going down
+		 (eq pg-input-ring-index 0))
+	    (and (> arg 0)		; going up
+		 (eq pg-input-ring-index
+		     (1- (ring-length pg-input-ring)))))
+	   pg-stored-incomplete-input)
+      (pg-restore-input)
+    (pg-previous-matching-input "." arg)))
+
+(defun pg-next-input (arg)
+  "Cycle forwards through input history."
+  (interactive "*p")
+  (pg-previous-input (- arg)))
+
+(defun pg-delete-input ()
+  (let* ((unproc (proof-unprocessed-begin))
+	 (start  (save-excursion
+		   (goto-char unproc)
+		   (skip-chars-forward " \t\n")
+		   (point)))
+	 (end    (point-at-eol)))
+    (cond
+     ((< start end)
+      (delete-region start end))
+     ((< start (point-at-eol))
+      (delete-region start (point-at-eol))))))
+
+(defun pg-get-old-input ()
+  "Return text between end of locked region and point, up to EOL.
+If there is no text, return the empty string."
+  (let* ((unproc (proof-unprocessed-begin))
+	 (start  (save-excursion
+		   (goto-char unproc)
+		   (skip-chars-forward " \t\n")
+		   (point)))
+	 (end    (point-at-eol)))
+    (if (< start end)
+	(buffer-substring-no-properties start end)
+      nil)))
+
+
+(defun pg-restore-input ()
+  "Restore unfinished input."
+  (interactive)
+  (when pg-input-ring-index
+    (pg-delete-input)
+    (when (> (length pg-stored-incomplete-input) 0)
+      (insert pg-stored-incomplete-input)
+      (message "Input restored"))
+    (setq pg-input-ring-index nil)))
+
+
+(defun pg-search-start (arg)
+  "Index to start a directional search, starting at `pg-input-ring-index'."
+  (if pg-input-ring-index
+      ;; If a search is running, offset by 1 in direction of arg
+      (mod (+ pg-input-ring-index (if (> arg 0) 1 -1))
+	   (ring-length pg-input-ring))
+    ;; For a new search, start from beginning or end, as appropriate
+    (if (>= arg 0)
+	0				       ; First elt for forward search
+      (1- (ring-length pg-input-ring)))))  ; Last elt for backward search
+
+
+(defun pg-regexp-arg (prompt)
+  "Return list of regexp and prefix arg using PROMPT."
+  (let* (;; Don't clobber this.
+	 (last-command last-command)
+	 (regexp (read-from-minibuffer prompt nil nil nil
+				       'minibuffer-history-search-history)))
+    (list (if (string-equal regexp "")
+	      (setcar minibuffer-history-search-history
+		      (nth 1 minibuffer-history-search-history))
+	    regexp)
+	  (prefix-numeric-value current-prefix-arg))))
+
+(defun pg-search-arg (arg)
+  ;; First make sure there is a ring and that we are after the process mark
+  (cond ((not (>= (point) (proof-unprocessed-begin)))
+	 (error "Not in unlocked region"))
+	((or (null pg-input-ring)
+	     (ring-empty-p pg-input-ring))
+	 (error "Empty input ring"))
+	((zerop arg)
+	 ;; arg of zero resets search from beginning, and uses arg of 1
+	 (setq pg-input-ring-index nil)
+	 1)
+	(t
+	 arg)))
+
+(defun pg-previous-matching-input-string-position (regexp arg &optional start)
+  "Return the index matching REGEXP ARG places along the input ring.
+Moves relative to START, or `pg-input-ring-index'."
+  (if (or (not (ring-p pg-input-ring))
+	  (ring-empty-p pg-input-ring))
+      (error "No history"))
+  (let* ((len (ring-length pg-input-ring))
+	 (motion (if (> arg 0) 1 -1))
+	 (n (mod (- (or start (pg-search-start arg)) motion) len))
+	 (tried-each-ring-item nil)
+	 (prev nil))
+    ;; Do the whole search as many times as the argument says.
+    (while (and (/= arg 0) (not tried-each-ring-item))
+      ;; Step once.
+      (setq prev n
+	    n (mod (+ n motion) len))
+      ;; If we haven't reached a match, step some more.
+      (while (and (< n len) (not tried-each-ring-item)
+		  (not (string-match regexp (ring-ref pg-input-ring n))))
+	(setq n (mod (+ n motion) len)
+	      ;; If we have gone all the way around in this search.
+	      tried-each-ring-item (= n prev)))
+      (setq arg (if (> arg 0) (1- arg) (1+ arg))))
+    ;; Now that we know which ring element to use, if we found it, return that.
+    (if (string-match regexp (ring-ref pg-input-ring n))
+	n)))
+
+(defun pg-previous-matching-input (regexp n)
+  "Search backwards through input history for match for REGEXP.
+\(Previous history elements are earlier commands.)
+With prefix argument N, search for Nth previous match.
+If N is negative, find the next or Nth next match."
+  (interactive (pg-regexp-arg "Previous input matching (regexp): "))
+  (setq n (pg-search-arg n))
+  (let ((pos (pg-previous-matching-input-string-position regexp n)))
+    ;; Has a match been found?
+    (if (null pos)
+	(error "Match not found" regexp)
+      ;; If leaving the edit line, save partial input
+      (if (null pg-input-ring-index)	;not yet on ring
+	  (setq pg-stored-incomplete-input (pg-get-old-input)))
+      (setq pg-input-ring-index pos)
+      (message "History item: %d" (1+ pos))
+      (pg-delete-input)
+      (insert (ring-ref pg-input-ring pos)))))
+
+(defun pg-next-matching-input (regexp n)
+  "Search forwards through input history for match for REGEXP.
+\(Later history elements are more recent commands.)
+With prefix argument N, search for Nth following match.
+If N is negative, find the previous or Nth previous match."
+  (interactive (pg-regexp-arg "Next input matching (regexp): "))
+  (pg-previous-matching-input regexp (- n)))
+
+(defvar pg-matching-input-from-input-string ""
+  "Input previously used to match input history.")
+
+;;;###autoload
+(defun pg-previous-matching-input-from-input (n)
+  "Search backwards through input history for match for current input.
+\(Previous history elements are earlier commands.)
+With prefix argument N, search for Nth previous match.
+If N is negative, search forwards for the -Nth following match."
+  (interactive "p")
+  (if (not (memq last-command '(pg-previous-matching-input-from-input
+				pg-next-matching-input-from-input)))
+      ;; Starting a new search
+      (setq pg-matching-input-from-input-string (pg-get-old-input)
+	    pg-input-ring-index nil))
+  (if pg-matching-input-from-input-string
+      (pg-previous-matching-input
+       (concat "^" (regexp-quote pg-matching-input-from-input-string))
+       n)
+    (pg-previous-matching-input "." n)))
+
+;;;###autoload
+(defun pg-next-matching-input-from-input (n)
+  "Search forwards through input history for match for current input.
+\(Following history elements are more recent commands.)
+With prefix argument N, search for Nth following match.
+If N is negative, search backwards for the -Nth previous match."
+  (interactive "p")
+  (pg-previous-matching-input-from-input (- n)))
+
+
+
+;;;###autoload
+(defun pg-add-to-input-history (cmd)
+   "Maybe add CMD to the input history.
+CMD is only added to the input history if it is not a duplicate
+of the last item added."
+   (when (or (not (ring-p pg-input-ring))
+	     (ring-empty-p pg-input-ring)
+	     (not (string-equal (ring-ref pg-input-ring 0) cmd)))
+     (unless (ring-p pg-input-ring)
+       (setq pg-input-ring (make-ring pg-input-ring-size)))
+     (ring-insert pg-input-ring cmd)))
+
+;;;###autoload
+(defun pg-remove-from-input-history (cmd)
+  "Maybe remove CMD from the end of the input history.
+This is called when the command is undone.  It's only 
+removed if it matches the last item in the ring."
+  (if (and (ring-p pg-input-ring)
+	   (not (ring-empty-p pg-input-ring))
+	   (string-equal (ring-ref pg-input-ring 0) cmd))
+      (ring-remove pg-input-ring 0)))
+  
+
+;;;###autoload
+(defun  pg-clear-input-ring ()
+  (setq pg-input-ring nil))
+
+
 (provide 'pg-user)
 ;;; pg-user.el ends here
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 129e65b7..e8209f35 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -15,7 +15,7 @@
 (require 'span)				; abstraction of overlays/extents
 (require 'proof)			; loader (& proof-utils macros)
 (require 'proof-syntax)		        ; utils for manipulating syntax
-(require 'proof-menu)			; menus for script mode
+;(require 'proof-menu)			; menus for script mode
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -236,11 +236,10 @@ Otherwise set the locked region to be from (point-min) to END."
      (min (point-max) end) ;; safety: sometimes called with end>point-max(?)
     )))
 
-;; Reimplemented this to mirror above because of remaining
-;; span problen
 (defsubst proof-set-queue-end (end)
   "Set the queue span to end at END."
   (if (or (>= (point-min) end)
+	  (not (span-live-p  proof-queue-span))
 	  (<= end (span-start proof-queue-span)))
       (proof-detach-queue)
     (span-set-end proof-queue-span end)))
@@ -275,7 +274,8 @@ Also clear list of script portions."
   (span-detach proof-locked-span)
   (setq proof-last-theorem-dependencies nil)
   (setq proof-element-counters nil)
-  (pg-clear-script-portions))
+  (pg-clear-script-portions)
+  (pg-clear-input-ring))
 
 
 ;; ** Restarting and clearing spans
@@ -1120,14 +1120,9 @@ If the hooks issue commands to the proof assistant (via
 `proof-shell-invisible-command') which result in an error, the
 activation is considered to have failed and an error is given."
   (interactive)
-  ;; FIXME: the scope of this save-excursion is rather wide.
-  ;; Problems without it however: Use button behaves oddly
-  ;; when process is started already.
-  ;; Where is save-excursion needed?
-  ;; First experiment shows that it's the hooks that cause
-  ;; problem, maybe even the use of proof-cd-sync (can't see why).
+  ;; TODO: narrow the scope of this save-excursion.
+  ;; Where is it needed?  Maybe hook functions.
   (save-excursion
-    ;; FIXME: proof-shell-ready-prover here s
     (proof-shell-ready-prover queuemode)
     (cond
      ((not (eq proof-buffer-type 'script))
@@ -1148,10 +1143,9 @@ activation is considered to have failed and an error is given."
 		(error
 		 "You cannot have more than one active scripting buffer!"))))
 	    
-      ;; Now make sure that this buffer is off the included files
-      ;; list.  In case we re-activate scripting in an already
-      ;; completed buffer, it may be that the proof assistant
-      ;; needs to retract some of this buffer's dependencies.
+      ;; Ensure this buffer is off the included files list.  If we
+      ;; re-activate scripting in an already completed buffer, the
+      ;; proof assistant may need to retract some dependencies.
       (proof-unregister-buffer-file-name 'tell-the-prover)
 
       ;; If automatic retraction happened in the above step, we may
@@ -1343,7 +1337,11 @@ With ARG, turn on scripting iff ARG is positive."
        
        ;; CASE 5:  Some other kind of command (or a nested goal).
        (t
-	(proof-done-advancing-other span))))
+	(proof-done-advancing-other span)))
+
+      ;; Add the processed command to the input ring
+      (unless (eq (span-property span 'type) 'comment)
+	(pg-add-to-input-history cmd)))
 
   ;; Finally: state of scripting may have changed now, run hooks.
   (run-hooks 'proof-state-change-hook)))
@@ -2222,12 +2220,11 @@ appropriate."
 ;; code here is fairly straightforward.
 
 
-;; FIXME: we need to adjust proof-nesting-depth appropriately here.
+;; TODO: we need to adjust proof-nesting-depth appropriately here.
 ;; It would help to know the type of retraction which has just
 ;; occurred: a kill-proof may be assumed to set nesting depth
 ;; to zero; an undo sequence may alter it some other way.
-;; FIXME FIXME: at the moment, the adjustment is made in
-;; the wrong place!!
+;; NB: at the moment, the adjustment is made in the wrong place!!
 
 (defun proof-done-retracting (span)
   "Callback for proof-retract-until-point.
@@ -2238,7 +2235,7 @@ After an undo, we clear the proof completed flag.  The rationale
 is that undoing never leaves prover in a \"proof just completed\"
 state, which is true for some proof assistants (but probably not
 others)."
-  ;; FIXME: need to fixup proof-nesting-depth
+  ;; TODO: need to fixup proof-nesting-depth
   (setq proof-shell-proof-completed nil)
   (if (span-live-p span)
       (let ((start (span-start span))
@@ -2249,6 +2246,14 @@ others)."
 	(unless (proof-locked-region-empty-p)
 	  (proof-set-locked-end start)
 	  (proof-set-queue-end start))
+	;; Try to clean input history (NB: rely on order here)
+	(let ((cmds (spans-at-region-prop start end 'cmd))
+	      (fn   (lambda (span)
+		      (unless (eq (span-property span 'type) 'comment)
+			(pg-remove-from-input-history
+			 (span-property span 'cmd))))))
+	  (mapcar fn (reverse cmds)))
+	
 	(span-delete-spans start end 'type)
 	(span-delete-spans start end 'idiom)
 	(span-delete span)
@@ -2758,7 +2763,7 @@ finish setup which depends on specific proof assistant configuration."
 
   ;; Additional key definitions which depend on configuration for
   ;; specific proof assistant.
-  ;; FIXME da: generalize here.  Might have electric terminator for
+  ;; TODO da: generalize here.  Might have electric terminator for
   ;; other parsing mechanisms too, using new proof-script-parse-function
   ;; Could use a default terminal char
   (if proof-terminal-char
@@ -2767,7 +2772,7 @@ finish setup which depends on specific proof assistant configuration."
 	  (vconcat [(control c)] (vector proof-terminal-char))
 	  'proof-electric-terminator-toggle)
 	(define-key proof-mode-map (vector proof-terminal-char)
-	  'proof-electric-terminator-toggle)))
+	  'proof-electric-terminator)))
 
   (make-local-variable 'indent-line-function)
   (setq indent-line-function 'proof-indent-line)