Many rearrangements for compatibility, efficient/correct compilation, namespaces fixes.

pre-shell-start-hook: remove this, use default names for modes
proof-compat: simplify architecture flags, use standard (featurep 'xemacs).

1 files changed, 73 insertions, 222 deletions

diff --git a/generic/pg-goals.el b/generic/pg-goals.el
index e726ecdd..f1558217 100644
--- a/generic/pg-goals.el
+++ b/generic/pg-goals.el
@@ -1,6 +1,6 @@
-;; pg-goals.el  Proof General goals buffer mode.
+;; pg-goals.el ---  Proof General goals buffer mode.
 ;;
-;; Copyright (C) 1994-2002 LFCS Edinburgh. 
+;; Copyright (C) 1994-2008 LFCS Edinburgh.
 ;; Authors:   David Aspinall, Yves Bertot, Healfdene Goguen,
 ;;            Thomas Kleymann and Dilip Sequeira
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
@@ -8,33 +8,36 @@
 ;; $Id$
 ;;
 
-;; A sub-module of proof-shell; assumes proof-script loaded.
-(require 'pg-assoc)
+;;; Code:
+(eval-when-compile
+  (require 'easymenu)			; easy-menu-add, etc
+  (require 'cl)				; incf
+  (require 'span)			; span-*
+  (require 'proof-utils))
+
+
+;;; Commentary:
+;; 
 
+(require 'proof-site)
 (require 'bufhist)
+;(require 'pg-assoc)
 
-;; Nuke some byte compiler warnings.
-(eval-when-compile
-  (require 'easymenu))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Goals buffer mode
 ;;
 
-;;
-;; The mode itself
-;;
-(eval-and-compile			; to define proof-goals-mode-map
+;;;###autload
 (define-derived-mode proof-goals-mode proof-universal-keys-only-mode
-  proof-general-name 
-  "Mode for goals display.  
+  proof-general-name
+  "Mode for goals display.
 May enable proof-by-pointing or similar features.
 \\{proof-goals-mode-map}"
   (setq proof-buffer-type 'goals)
   ;; font-lock-keywords isn't automatically buffer-local in Emacs 21.2
   (make-local-variable 'font-lock-keywords)
-  (make-local-hook 'kill-buffer-hook)
   (add-hook 'kill-buffer-hook 'pg-save-from-death nil t)
   (easy-menu-add proof-goals-mode-menu proof-goals-mode-map)
   (easy-menu-add proof-assistant-menu proof-goals-mode-map)
@@ -42,47 +45,51 @@ May enable proof-by-pointing or similar features.
   (erase-buffer)
   (buffer-disable-undo)
   (if proof-keep-response-history (bufhist-mode)) ; history for contents
-  (set-buffer-modified-p nil)))
+  (set-buffer-modified-p nil))
 
 ;;
-;; Keys for goals buffer
+;; Menu for goals buffer
 ;;
-(define-key proof-goals-mode-map [q] 'bury-buffer)
-(cond 
-(proof-running-on-XEmacs
-(define-key proof-goals-mode-map [(button2)] 'pg-goals-button-action)
-(define-key proof-goals-mode-map [(control button2)] 'proof-undo-and-delete-last-successful-command)
-;; button 2 is a nuisance on 2 button mice, so we'll do 1 as well.
-;; Actually we better hadn't, people like to use it for cut and paste.
-;; (define-key proof-goals-mode-map [(button1)] 'pg-goals-button-action)
-;; (define-key proof-goals-mode-map [(control button1)] 'proof-undo-and-delete-last-successful-command)
-;; C Raffalli: The next key on button3 will be remapped to proof by contextual 
-;; menu by pg-pbrpm.el. In this case, control button3 is mapped to 
-;; 'pg-goals-yank-subterm
-(define-key proof-goals-mode-map [(button3)] 'pg-goals-yank-subterm))
-(t
-(define-key proof-goals-mode-map [mouse-2] 'pg-goals-button-action)
-(define-key proof-goals-mode-map [C-mouse-2] 'proof-undo-and-delete-last-successful-command)
-;; (define-key proof-goals-mode-map [mouse-1] 'pg-goals-button-action)
-;; (define-key proof-goals-mode-map [C-mouse-1] 'proof-undo-and-delete-last-successful-command)
-;; C Raffalli: The next key on button3 will be remapped to proof by contextual 
-;; menu by pg-pbrpm.el. In this cans, control button3 is mapped to 
-;; 'pg-goals-yank-subterm
-(define-key proof-goals-mode-map [mouse-3] 'pg-goals-yank-subterm)))
+(proof-eval-when-ready-for-assistant ; proof-aux-menu depends on <PA>
+    (easy-menu-define proof-goals-mode-menu
+      proof-goals-mode-map
+      "Menu for Proof General goals buffer."
+      (proof-aux-menu)))
 
 
 ;;
-;; Menu for goals buffer
+;; Keys for goals buffer
 ;;
-(easy-menu-define proof-goals-mode-menu
-		  proof-goals-mode-map
-		  "Menu for Proof General goals buffer."
-		  proof-aux-menu)
+(define-key proof-goals-mode-map [q] 'bury-buffer)
+
+(cond
+ ((featurep 'xemacs)
+  (define-key proof-goals-mode-map [(button2)] 'pg-goals-button-action)
+  (define-key proof-goals-mode-map [(control button2)] 'proof-undo-and-delete-last-successful-command)
+  ;; button 2 is a nuisance on 2 button mice, so we'll do 1 as well.
+  ;; Actually we better hadn't, people like to use it for cut and paste.
+  ;; (define-key proof-goals-mode-map [(button1)] 'pg-goals-button-action)
+  ;; (define-key proof-goals-mode-map [(control button1)] 'proof-undo-and-delete-last-successful-command)
+  ;; C Raffalli: The next key on button3 will be remapped to proof by contextual
+  ;; menu by pg-pbrpm.el.  In this case, control button3 is mapped to
+  ;; 'pg-goals-yank-subterm
+  (define-key proof-goals-mode-map [(button3)] 'pg-goals-yank-subterm))
+ (t
+  (define-key proof-goals-mode-map [mouse-2] 'pg-goals-button-action)
+  (define-key proof-goals-mode-map [C-mouse-2] 'proof-undo-and-delete-last-successful-command)
+  ;; (define-key proof-goals-mode-map [mouse-1] 'pg-goals-button-action)
+  ;; (define-key proof-goals-mode-map [C-mouse-1] 'proof-undo-and-delete-last-successful-command)
+  ;; C Raffalli: The next key on button3 will be remapped to proof by contextual
+  ;; menu by pg-pbrpm.el.  In this case, control button3 is mapped to
+  ;; 'pg-goals-yank-subterm
+  (define-key proof-goals-mode-map [mouse-3] 'pg-goals-yank-subterm)))
+
 
 
 ;;
 ;; The completion of init
 ;;
+;;;###autoload
 (defun proof-goals-config-done ()
   "Initialise the goals buffer after the child has been configured."
   (proof-font-lock-configure-defaults nil)
@@ -110,7 +117,7 @@ and properly fontifies STRING using proof-fontify-region."
     
     ;; Erase the response buffer if need be, maybe removing the
     ;; window.  Indicate it should be erased before the next output.
-    (proof-shell-maybe-erase-response t t)
+    (pg-response-maybe-erase t t)
 
     ;; Erase the goals buffer and add in the new string
     (set-buffer proof-goals-buffer)
@@ -131,7 +138,7 @@ and properly fontifies STRING using proof-fontify-region."
       ;; for special characters 128-255, which is inconsistent with
       ;; UTF-8 interaction.
       (unless proof-shell-unicode
-	(pg-goals-analyse-structure (point-min) (point-max)))
+	(pg-assoc-analyse-structure (point-min) (point-max)))
 
       (unless pg-use-specials-for-fontify
 	;; provers which use ordinary keywords to fontify output must
@@ -139,173 +146,16 @@ and properly fontifies STRING using proof-fontify-region."
 	(proof-fontify-region (point-min) (point-max)))
       
       ;; Record a cleaned up version of output string
-      (setq proof-shell-last-output 
+      (setq proof-shell-last-output
 	    (buffer-substring (point-min) (point-max)))
       
       (set-buffer-modified-p nil)	; nicety
       
-      ;; Keep point at the start of the buffer.  
-      (proof-display-and-keep-buffer 
+      ;; Keep point at the start of the buffer.
+      (proof-display-and-keep-buffer
        proof-goals-buffer (point-min)))))
 
 
-(defun pg-goals-analyse-structure (start end)
-  "Analyse the region between START and END for subterm and PBP markup.
-
-For subterms, we can make nested regions in the concrete syntax into
-active mouse-highlighting regions, each of which can be used to
-communicate a selected term back to the prover.  The output text is
-marked up with the annotation scheme:
-
- 	 [  <annotation>      |       <subterm/concrete> ] 
-
-         ^                    ^                          ^
-	 |                    |                          |
-pg-subterm-start-char  pg-subterm-sep-char  pg-subterm-end-char
-
-The annotation is intended to indicate a node in the abstract syntax
-tree inside the prover, which can be used to pick out the internal
-representation of the term itself.  We assume that the annotation
-takes the form of a sequence of characters:
-
-   <length of shared prefix previous>  <ann1> <ann2> .. <annN>
-
-Where each element <..> is a character which is *less* than
-pg-subterm-first-special-char, but *greater* than 128.  Each 
-character code has 128 subtracted to yield a number.  The first
-character allows a simple optimisation by sharing a prefix of
-the previous (left-to-right) subterm's annotation.  (See the
-variable `pg-subterm-anns-use-stack' for an alternative 
-optimisation.)
-
-For subterm markup without communication back to the prover, the
-annotation is not needed, but the first character must still be given.
-
-For proof-by-pointing (PBP) oriented markup, `pg-topterm-regexp' and
-`pg-topterm-goalhyplit-fn' should be set.  Together these allow
-further active regions to be defined, corresponding to \"top elements\"
-in the proof-state display.  A \"top element\" is currently assumed
-to be either a hypothesis or a subgoal, and is assumed to occupy 
-a line (or at least a line).  The markup is simply
-  
-                 & <goal or hypthesis line in proof state>
-                 ^
-		 |
-   pg-topterm-regexp
-
-And the function `pg-topterm-goalhyplit-fn' is called to do the
-further analysis, to return an indication of the goal/hyp and
-record a name value.  These values are used to construct PBP
-commands which can be sent to the prover."
-  (if (or pg-subterm-start-char pg-topterm-regexp) ;; markup for topterm alone
-  (let* 
-      ((cur start)
-       (len (- end start))
-       (ann (make-string len ?x)) ; (more than) enough space for longest ann'n
-       (ap  0)
-       c stack topl span)
-
-    (while (< cur end)
-      (setq c (char-after cur))
-      (cond
-       ;; Seen goal regexp: this is the start of a top extent
-       ;; (assumption, goal, literal command)
-       ((save-excursion
-	  (goto-char cur)
-	  (looking-at pg-topterm-regexp))
-	(setq topl (cons cur topl))
-	(setq ap 0))
-
-       ;; Seen subterm start char: it's followed by a char
-       ;; indicating the length of the annotation prefix
-       ;; which can be shared with the previous subterm.
-       ((and pg-subterm-start-char ;; ignore if subterm start not set
-	     (= c pg-subterm-start-char))
-	(incf cur)
-	(if pg-subterm-anns-use-stack
-	    (setq ap (- ap (- (char-after cur) 128)))
-	  (setq ap (- (char-after cur) 128)))
-	(incf cur)
-	;; Now search for a matching end-annotation char, recording the 
-	;; annotation found.
-	(while (not (= (setq c (char-after cur)) pg-subterm-sep-char))
-	  (aset ann ap (- c 128))
-	  (incf ap)
-	  (incf cur))
-	;; Push the buffer pos and annotation
-	(setq stack (cons cur 
-			  (cons (substring ann 0 ap) stack))))
-
-       ;; Seen a subterm end char, terminating an annotated region
-       ;; in the concrete syntax.  We make a highlighting span now.
-       ((and (consp stack) (= c pg-subterm-end-char))
-	;; (consp stack) added to make the code more robust.
-	;; [ Condition violated with lego/example.l and GNU Emacs 20.3 ]
-	(setq span (make-span (car stack) cur))
-	(set-span-property span 'mouse-face 'highlight)
-	(set-span-property span 'goalsave (cadr stack));; FIXME: 'goalsave?
-	;; (set-span-property span 'balloon-help helpmsg)
-	(set-span-property span 'help-echo 'pg-goals-get-subterm-help)
-	(if pg-subterm-anns-use-stack
-	    ;; Pop annotation off stack
-	    (progn
-	      (setq ap 0)
-	      (while (< ap (length (cadr stack)))
-		(aset ann ap (aref (cadr stack) ap))
-		(incf ap))))
-	;; Finish popping annotations
-	(setq stack (cdr (cdr stack)))))
-      ;; On to next char
-      (incf cur))
-    
-    ;; List of topterm beginning positions (goals/hyps) found
-    (setq topl (reverse (cons end topl)))
-    
-    ;; Proof-by-pointing markup assumes "top" elements which define a
-    ;; context for a marked-up (sub)term: we assume these contexts to
-    ;; be either a subgoal to be solved or a hypothesis.  
-    ;; Top element spans are only made if pg-topterm-goalhyplit-fn is set.
-    ;; NB: If we want Coq pbp: (setq coq-current-goal 1) 
-    (if pg-topterm-goalhyplit-fn
-	(while (setq ap (car topl) 
-		     topl (cdr topl))
-	  (pg-goals-make-top-span ap (car topl))))
-
-    ;; Finally: strip the specials.  This should
-    ;; leave the spans in exactly the right place.
-    (pg-assoc-strip-subterm-markup-buf start end))))
-
-
-(defun pg-goals-make-top-span (start end)
-  "Make a top span (goal/hyp area) for mouse active output."
-  (let (span typname)
-    (goto-char start)
-    ;; skip the pg-topterm-regexp itself
-    (if (looking-at pg-topterm-regexp) 
-	(forward-char (- (match-end 0) (match-beginning 0))))
-    ;; typname is expected to be a cons-cell of a type (goal/hyp)
-    ;; with a name, retrieved from the text immediately following
-    ;; the topterm-regexp annotation.
-    (let ((topterm (point))) 
-      (setq typname (funcall pg-topterm-goalhyplit-fn)) ;; should be non-nil!
-      (goto-char topterm))
-    (setq start (point))
-    (if (eq (car-safe typname) 'lit)
-	;; Use length of literal command for end point
-	(forward-char (length (cdr typname)))
-      ;; Otherwise, use start/end of line before next annotation/buffer end
-      (goto-char start)
-      (beginning-of-line)
-      (setq start (point))
-      (goto-char end) ;; next annotation/end of buffer
-      (beginning-of-line)
-      (backward-char))
-    (setq span (make-span start (point)))
-    (set-span-property span 'mouse-face 'highlight)
-    (set-span-property span 'face 'proof-active-area-face)
-    (set-span-property span 'proof-top-element typname)))
-
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Commands to prover based on subterm markup (inc PBP).
@@ -322,7 +172,7 @@ This function should be bound to a mouse button in the Proof General
 goals buffer.
 
 The EVENT is used to find the smallest subterm around a point.  The
-subterm is copied to the kill-ring, and immediately yanked (copied)
+subterm is copied to the `kill-ring', and immediately yanked (copied)
 into the current buffer at the current cursor position.
 
 In case the current buffer is the goals buffer itself, the yank
@@ -334,11 +184,11 @@ explicit yank."
       (save-excursion
 	(mouse-set-point event)
 	;; Get either the proof body or whole goalsave
-	(setq span (or 
+	(setq span (or
 		    (span-at (point) 'proof)
 		    (span-at (point) 'goalsave)))
 	(if span (copy-region-as-kill
-		  (span-start span) 
+		  (span-start span)
 		  (span-end span)))))
     (if (and span (not (eq proof-buffer-type 'goals)))
 	(yank))))
@@ -354,7 +204,7 @@ it to construct an appropriate proof command.  The command which is
 constructed will be inserted at the end of the locked region in the
 proof script buffer, and immediately sent back to the proof assistant.
 If it succeeds, the locked region will be extended to cover the
-proof-by-pointing command, just as for any proof command the 
+proof-by-pointing command, just as for any proof command the
 user types by hand."
    (interactive "e")
    (mouse-set-point event)
@@ -366,15 +216,15 @@ user types by hand."
 
 (defun proof-expand-path (string)
   (let ((a 0) (l (length string)) ls)
-    (while (< a l) 
-      (setq ls (cons (int-to-string 
+    (while (< a l)
+      (setq ls (cons (int-to-string
 		      (char-to-int (aref string a)))
 		     (cons " " ls)))
       (incf a))
     (apply 'concat (nreverse ls))))
 
 (defun pg-goals-construct-command ()
-  ;; Examine the goals 
+  "Examine the goals "
   (let* ((span (span-at (point) 'goalsave)) ;; goalsave means subgoal no/name
 	 (top-span (span-at (point) 'proof-top-element))
 	 top-info)
@@ -383,10 +233,10 @@ user types by hand."
       (pop-to-buffer proof-script-buffer)
       (cond
        (span
-	(proof-shell-invisible-command 
-	 (format (if (eq 'hyp (car top-info)) pbp-hyp-command 
+	(proof-shell-invisible-command
+	 (format (if (eq 'hyp (car top-info)) pbp-hyp-command
 		                              pbp-goal-command)
-		 (concat (cdr top-info) (proof-expand-path 
+		 (concat (cdr top-info) (proof-expand-path
 					 (span-property span 'goalsave))))))
        ((eq (car top-info) 'hyp)
 	;; Switch focus to another subgoal; a non-scripting command
@@ -409,21 +259,22 @@ user types by hand."
 	(or (span-property span 'cachedhelp) ;; already got
 	    (progn
 	      (if (proof-shell-available-p)
-		  (let ((result 
-			 (proof-shell-invisible-cmd-get-result 
+		  (let ((result
+			 (proof-shell-invisible-cmd-get-result
 			  (format pg-subterm-help-cmd (span-string span))
 			  'ignorerrors)))
 		    ;; FIXME: generalise, and make output readable
 		    ;; (fontify?  does that work for GNU Emacs?
 		    ;;  how can we do it away from a buffer?)
 		    (setq result
-			  (replace-in-string 
-			   result 
-			   (concat "\n\\|" pg-special-char-regexp) ""))		    
-		    (set-span-property span 'cachedhelp result)
+			  (replace-in-string
+			   result
+			   (concat "\n\\|" pg-special-char-regexp) ""))
+		    (span-set-property span 'cachedhelp result)
 		    result)))))))
 
 
 
 (provide 'pg-goals)
-;; pg-goals.el ends here.
+
+;;; pg-goals.el ends here