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, 174 insertions, 11 deletions

diff --git a/generic/pg-assoc.el b/generic/pg-assoc.el
index d49ccc9e..45dd3cbd 100644
--- a/generic/pg-assoc.el
+++ b/generic/pg-assoc.el
@@ -1,23 +1,26 @@
-;; pg-assoc.el  Functions for associated buffers
+;;; pg-assoc.el --- Functions for associated buffers
 ;;
-;; 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)
 ;;
 ;; $Id$
 ;;
-
-;; A sub-module of proof-shell; assumes proof-script loaded.
-(require 'proof-script)
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Defines an empty mode inherited by modes of the associated buffers.
 ;;
 
-(eval-and-compile
-(define-derived-mode proof-universal-keys-only-mode fundamental-mode
+;;; Code:
+
+(eval-when-compile 
+  (require 'proof)				; globals
+  (require 'proof-syntax)			; proof-replace-{string,regexp}
+  (require 'span)
+  (require 'cl))				; incf
+
+(eval-and-compile ; to define proof-universal-keys-only-mode-map at compile time
+  (define-derived-mode proof-universal-keys-only-mode fundamental-mode
     proof-general-name "Universal keymaps only"
     ;; Doesn't seem to supress TAB, RET
     (suppress-keymap proof-universal-keys-only-mode-map 'all)
@@ -108,7 +111,7 @@ If pg-subterm-first-special-char is unset, return STRING unchanged."
 	  
 	 
 (defun pg-assoc-strip-subterm-markup-buf-old (start end)
-  "Remove subterm and pbp annotations from region."
+  "Remove subterm and pbp annotations from region START END."
   (let (c)
     (goto-char start)
     (while (< (point) end)
@@ -131,7 +134,167 @@ If pg-subterm-first-special-char is unset, return STRING unchanged."
 	(forward-char)))
     end))
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;
+;;; Subterm and PBP markup (goals and possibly response buffer)
+;;; 
+
+(defun pg-assoc-make-top-span (start end)
+  "Make a top span (goal/hyp area) for mouse active output in START END."
+  (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 (span-make start (point)))
+    (span-set-property span 'mouse-face 'highlight)
+    (span-set-property span 'face 'proof-active-area-face)
+    (span-set-property span 'proof-top-element typname)))
+
+(defun pg-assoc-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 (span-make (car stack) cur))
+	(span-set-property span 'mouse-face 'highlight)
+	(span-set-property span 'goalsave (cadr stack));; FIXME: 'goalsave?
+	;; (span-set-property span 'balloon-help helpmsg)
+	(span-set-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-assoc-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))))
+
 
 
 (provide 'pg-assoc)
-;; pg-assoc.el ends here.
+;;; pg-assoc.el ends here