Add proof-shell-strip-output-markup to handle pasting markedup texdt. Minor cleanups

7 files changed, 71 insertions, 37 deletions

diff --git a/generic/pg-goals.el b/generic/pg-goals.el
index 35ea669c..e3e53c5a 100644
--- a/generic/pg-goals.el
+++ b/generic/pg-goals.el
@@ -101,13 +101,10 @@ Converts term substructure markup into mouse-highlighted extents."
 
     ;; Only display if string is non-empty.
     (unless (string-equal string "")
+      (setq buffer-read-only nil)
       (insert string)
-
-      ;; Record a cleaned up version of output string
-      (setq proof-shell-last-output
-	    (buffer-substring (point-min) (point-max)))
-      
-      (set-buffer-modified-p nil)	; nicety
+      (setq buffer-read-only t)
+      (set-buffer-modified-p nil)
       
       ;; Keep point at the start of the buffer.
       (proof-display-and-keep-buffer
diff --git a/generic/pg-response.el b/generic/pg-response.el
index 7176fae3..c416843c 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -251,23 +251,16 @@ Returns non-nil if response buffer was cleared."
 
 (defun pg-response-display (str)
   "Show STR as a response in the response buffer."
-  ;; FIXME removed for PG 4.0:
-  ;; (unless (or proof-shell-unicode
-  ;;    pg-use-specials-for-fontify)
-  ;; (setq str (pg-assoc-strip-subterm-markup str)))
 
   (pg-response-maybe-erase t nil)
-  ;;(unless (or (string-equal str "") (string-equal str "\n"))
-    ;; don't display an empty buffer [ NB: above test repeated below,
-    ;; but response-display reused elsewhere ]
   (pg-response-display-with-face str)
+
   ;; NB: this displays an empty buffer sometimes when it's not
   ;; so useful.  It _is_ useful if the user has requested to
   ;; see the proof state and there is none
   ;; (Isabelle/Isar displays nothing: might be better if it did).
   (proof-display-and-keep-buffer proof-response-buffer))
 
-
 ;;
 ;; Images for the response buffer
 ;;
@@ -282,13 +275,15 @@ Returns non-nil if response buffer was cleared."
 ;; pg-response-maybe-erase-buffer.
 ;;;###autoload
 (defun pg-response-display-with-face (str &optional face)
-  "Display STR with FACE in response buffer."
+  "Display STR with FACE in response buffer.
+Also updates `proof-shell-last-output'."
   (cond
    ((string-equal str ""))
    ((string-equal str "\n"))		; quick exit, no display.
    (t
     (let (start end)
       (with-current-buffer proof-response-buffer
+	(setq buffer-read-only nil)
 	;; da: I've moved newline before the string itself, to match
 	;; the other cases when messages are inserted and to cope
 	;; with warnings after delayed output (non newline terminated).
@@ -299,12 +294,14 @@ Returns non-nil if response buffer was cleared."
 	  (newline))
 	(setq start (point))
 	(insert str)
+	(setq proof-shell-last-output str)
 	(unless (bolp) (newline))
  	(when face
  	  (overlay-put
  	   (make-overlay start (point-max))
  	   'face face))
 
+	(setq buffer-read-only t)
 	(set-buffer-modified-p nil))))))
 
 (defun pg-response-clear-displays ()
diff --git a/generic/pg-user.el b/generic/pg-user.el
index d226aa49..81cc5a3b 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -567,6 +567,10 @@ last use time, to discourage saving these into the users database."
 		(add-completion cmpl -1000 0)))
 	  (proof-ass completion-table)))
 
+;; completion not autoloaded in GNU Emacs
+(or (fboundp 'complete)
+    (autoload 'complete "completion"))
+
 ;; NB: completion table is expected to be set when proof-script
 ;; is loaded!  Can call proof-script-add-completions if the table
 ;; is updated.
@@ -605,14 +609,9 @@ last use time, to discourage saving these into the users database."
   "Insert the last output from the proof system as a comment in the proof script."
   (interactive)
   (if proof-shell-last-output
-      ;; There may be a system specific function to insert the comment
-      (if pg-insert-output-as-comment-fn
-	  (funcall pg-insert-output-as-comment-fn proof-shell-last-output)
-	;; Otherwise the default behaviour is to use comment-region
-	(let  ((beg (point)) end)
-	  (insert proof-shell-last-output)
-	  (comment-region beg end)))))
-
+      (let  ((beg (point)))
+	(insert (proof-shell-strip-output-markup proof-shell-last-output))
+	(comment-region beg (point)))))
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
diff --git a/generic/proof-config.el b/generic/proof-config.el
index c3f13b4b..258d501b 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -907,12 +907,6 @@ but you can set this variable to something else more precise if necessary."
   :type 'string
   :group 'proof-script)
 
-(defcustom pg-insert-output-as-comment-fn nil
-  "Function to insert last output as a comment.  Passed output as arg.
-If left as nil, the default behaviour is to insert and call `comment-region'."
-  :type '(choice function nil)
-  :group 'proof-script)
-
 (defcustom proof-string-start-regexp "\""
   "Matches the start of a quoted string in the proof assistant command language."
   :type 'string
@@ -1836,6 +1830,15 @@ The default value is \"\\n\" to match up to the end of the line."
   :type '(choice regexp (const :tag "Unset" nil))
   :group 'proof-shell)
 
+(defcustom proof-shell-strip-output-markup 'identity
+  "A function which strips markup from the process output.
+This should remove any markup which is made invisible by font-lock
+when displayed in the output buffer.  This is used in 
+`pg-insert-last-output-as-comment' to insert output into the
+proof script, and for cut and paste operations."
+  :type 'function
+  :group 'proof-shell)
+
 (defcustom proof-shell-assumption-regexp nil
   "A regular expression matching the name of assumptions.
 
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 91f2646e..7599f005 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -635,10 +635,9 @@ suitable for adding to the proof assistant menu."
        (key (if (y-or-n-p "Set a keybinding for this command? : ")
 		;; FIXME: better validation here would be to check
 		;; this is a new binding, or remove old binding below.
-		(events-to-keys
 		 (read-key-sequence 
 		  "Type the key to use (binding will be C-c C-a <key>): " 
-		  nil t)))))
+		  nil t))))
     ;; result
     (list cmd ins men key)))
 	  
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 0c191c8a..30b430c5 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -639,6 +639,11 @@ are not dealt with eagerly during script processing, namely
    )
   (run-hooks 'proof-shell-handle-delayed-output-hook))
 
+(defsubst proof-shell-strip-output-markup (string &optional push)
+  "Strip output markup from STRING.
+Convenience function to call ` proof-shell-strip-output-markup'."
+  (funcall proof-shell-strip-output-markup string))
+
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; 
@@ -1111,9 +1116,10 @@ and indentation.  Assumes proof-script-buffer is active."
 
 (defun proof-shell-message (str)
   "Output STR in minibuffer."
-  ;; %s is used below to escape characters special to 
-  ;; 'format' which could appear in STR.
-  (message "%s" (concat "[" proof-assistant "] " str)))
+  (message "%s" ;; to escape format characters
+	   (concat "[" proof-assistant "] " 
+		   ;; TODO: rather than stripping, could try fontifying
+		   (proof-shell-strip-output-markup str))))
 
 (defun proof-shell-process-urgent-message (message)
   "Analyse urgent MESSAGE for various cases.
@@ -1762,6 +1768,9 @@ usual, unless NOERROR is non-nil."
   (setq proof-shell-urgent-message-scanner (make-marker))
   (set-marker proof-shell-urgent-message-scanner (point-min))
 
+  ;; Make cut functions work with proof shell output 
+  (add-hook 'buffer-substring-filters 'proof-shell-strip-output-markup)
+
   ;; FIXME da: before entering proof assistant specific code,
   ;; we'd do well to check that process is actually up and
   ;; running now.  If not, call the process sentinel function
@@ -1810,11 +1819,11 @@ processing."
 
       ;; Flush pending output from startup (it gets hidden from the user)
       ;; while waiting for the prompt to appear
-      (while (and (process-live-p proc)
+      (while (and (memq (process-status proc) '(open run))
 		  (null (marker-position proof-marker)))
 	(accept-process-output proc 1))
 
-      (if (process-live-p proc)
+      (if (memq (process-status proc) '(open run))
 	  (progn
 	    ;; Also ensure that proof-action-list is initialised. 
 	    (setq proof-action-list nil)
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index c016c686..9e5ca52c 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -803,10 +803,40 @@ EXTRAPATH is a list of extra path components"
        (executable-find progname)))
     ((fboundp 'locate-file)
      (locate-file progname
-		  (append (split-path (getenv "PATH")) extrapath)
+		  (append (split-string path 
+					(regexp-quote (getenv "PATH")))
+			  extrapath)
 		  (if proof-running-on-win32 '(".exe"))
 		  1)))
    (if returnnopath progname)))
 
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Extracting visible text in a buffer
+;;
+;; NB: this is possible automatic alternative to proof-shell-strip-output,
+;; but is more reliable to have specific setting.
+;;
+;; (defun proof-buffer-substring-visible (start end)
+;;   "Return the substring from START to END with no invisible property set."
+;;   (let ((pos start) 
+;; 	(vis (get-text-property start 'invisible))
+;; 	(result "")
+;; 	nextpos)
+;;     (while (and (< pos end)
+;; 		(setq nextpos (next-single-property-change pos 'invisible
+;; 							   nil end)))
+;;       (unless (get-text-property pos 'invisible)
+;; 	(setq result (concat result (buffer-substring-no-properties
+;; 				     pos nextpos))))
+;;       (setq pos nextpos))
+;;     (unless (get-text-property end 'invisible)
+;;       (setq result (concat result (buffer-substring-no-properties
+;; 				   pos end))))))
+
+
+
+
 (provide 'proof-utils)
 ;;; proof-utils.el ends here