Refactoring

1 files changed, 350 insertions, 0 deletions

diff --git a/generic/pg-goals.el b/generic/pg-goals.el
new file mode 100644
index 00000000..66b932f1
--- /dev/null
+++ b/generic/pg-goals.el
@@ -0,0 +1,350 @@
+;; pg-goals.el  Proof General goals buffer mode.
+;;
+;; Copyright (C) 1994-2002 LFCS Edinburgh. 
+;; Authors:   David Aspinall, Yves Bertot, Healfdene Goguen,
+;;            Thomas Kleymann and Dilip Sequeira
+;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
+;;
+;; $Id$
+;;
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Goals buffer mode
+;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(eval-and-compile			; to define proof-goals-mode-map
+(define-derived-mode proof-goals-mode proof-universal-keys-only-mode
+  proof-general-name 
+  "Mode for goals display.  
+May enable proof-by-pointing or similar features.
+\\{proof-goals-mode-map}"
+  ;; defined-derived-mode proof-goals-mode initialises proof-goals-mode-map
+  (setq proof-buffer-type 'goals)
+  (easy-menu-add proof-goals-mode-menu proof-goals-mode-map)
+  (easy-menu-add proof-assistant-menu proof-goals-mode-map)
+  (proof-toolbar-setup)
+  (erase-buffer)))
+
+;;
+;; Keys for goals buffer
+;;
+(define-key proof-goals-mode-map [q] 'bury-buffer)
+(cond 
+(proof-running-on-XEmacs
+(define-key proof-goals-mode-map [(button2)] 'pbp-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)] 'pbp-button-action)
+;; (define-key proof-goals-mode-map [(control button1)] 'proof-undo-and-delete-last-successful-command)
+(define-key proof-goals-mode-map [(button3)] 'pbp-yank-subterm))
+(t
+(define-key proof-goals-mode-map [mouse-2] 'pbp-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] 'pbp-button-action)
+;; (define-key proof-goals-mode-map [C-mouse-1] 'proof-undo-and-delete-last-successful-command)
+(define-key proof-goals-mode-map [mouse-3] 'pbp-yank-subterm)))
+
+
+;;
+;; Menu for goals buffer  (identical to response mode menu currently)
+;;
+(easy-menu-define proof-goals-mode-menu
+		  proof-goals-mode-map
+		  "Menu for Proof General goals buffer."
+		  (cons proof-general-name 
+			(append
+			 proof-toolbar-scripting-menu
+			 proof-shared-menu
+			 proof-config-menu
+			 proof-bug-report-menu)))
+
+(defun proof-goals-config-done ()
+  "Initialise the goals buffer after the child has been configured."
+  (proof-font-lock-configure-defaults nil)
+  (proof-x-symbol-configure))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Subterm markup and Proof-by-Pointing functionality
+;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; Fairly specific to the mechanism implemented in LEGO
+;; To make sense of this code, you should read the
+;; relevant LFCS tech report by tms, yb, and djs
+
+(defun pbp-yank-subterm (event)
+  "Copy the subterm indicated by the mouse-click EVENT.
+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)
+into the current buffer at the current cursor position.
+
+In case the current buffer is the goals buffer itself, the yank
+is not performed.  Then the subterm can be retrieved later by an
+explicit yank."
+  (interactive "e")
+  (let (span)
+    (save-window-excursion
+      (save-excursion
+	(mouse-set-point event)
+	;; Get either the proof body or whole goalsave
+	(setq span (or 
+		    (span-at (point) 'proof)
+		    (span-at (point) 'goalsave)))
+	(if span (copy-region-as-kill
+		  (span-start span) 
+		  (span-end span)))))
+    (if (and span (not (eq proof-buffer-type 'goals)))
+	(yank))))
+
+(defun pbp-button-action (event)
+  "Construct a proof-by-pointing command based on the mouse-click EVENT.
+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.  A
+position code for the subterm is sent to the proof assistant, to ask
+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 
+user types by hand."
+   (interactive "e")
+   (mouse-set-point event)
+   (pbp-construct-command))
+
+;; Using the spans in a mouse behavior is quite simple: from the
+;; mouse position, find the relevant span, then get its annotation
+;; and produce a piece of text that will be inserted in the right
+;; buffer.  
+
+(defun proof-expand-path (string)
+  (let ((a 0) (l (length string)) ls)
+    (while (< a l) 
+      (setq ls (cons (int-to-string 
+		      (char-to-int (aref string a)))
+		     (cons " " ls)))
+      (incf a))
+    (apply 'concat (nreverse ls))))
+
+(defun pbp-construct-command ()
+  (let* ((span (span-at (point) 'goalsave))
+	 (top-span (span-at (point) 'proof-top-element))
+	 top-info)
+    (if (null top-span) ()
+      (setq top-info (span-property top-span 'proof-top-element))
+      (pop-to-buffer proof-script-buffer)
+      (cond
+       (span
+	(proof-shell-invisible-command 
+	 (format (if (eq 'hyp (car top-info)) pbp-hyp-command 
+		                              pbp-goal-command)
+		 (concat (cdr top-info) (proof-expand-path 
+					 (span-property span 'goalsave))))))
+       ((eq (car top-info) 'hyp)
+	(proof-shell-invisible-command
+	 (format pbp-hyp-command (cdr top-info))))
+       (t
+	 (proof-insert-pbp-command
+	  (format pbp-change-goal (cdr top-info))))))))
+
+;;
+;; Goals buffer processing
+;;
+;; FIXME: rename next fn proof-display-in-goals or similar
+(defun proof-shell-analyse-structure (string)
+  "Analyse the term structure of STRING and display it in proof-goals-buffer.
+This function converts proof-by-pointing markup into mouse-highlighted
+extents."
+  (save-excursion
+      ;; Response buffer may be out of date. It may contain (error)
+      ;; messages relating to earlier proof states
+      
+      ;; FIXME da: this isn't always the case.  In Isabelle
+      ;; we get <WARNING MESSAGE> <CURRENT GOALS> output,
+      ;; or <WARNING MESSAGE> <ORDINARY MESSAGE>.  Both times
+      ;; <WARNING MESSAGE> would be relevant.
+      ;; We should only clear the output that was displayed from
+      ;; the *previous* prompt.
+
+      ;; Erase the response buffer if need be, maybe also removing the
+      ;; window.  Indicate that it should be erased before the next
+      ;; output.
+      (proof-shell-maybe-erase-response t t)
+
+      ;; Erase the goals buffer and add in the new string
+      (set-buffer proof-goals-buffer)
+      (erase-buffer)
+      (insert string)
+      
+      ;; Do term-structure markup if its enabled
+      (unless (not proof-shell-goal-char) 
+	(proof-shell-analyse-structure1 (point-min) (point-max)))
+
+      ;; Now get fonts and characters right
+      ;; FIXME: this may be broken by markup or aided by it!
+      (proof-fontify-region (point-min) (point-max))
+
+      ;; 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
+
+      ;; Keep point at the start of the buffer.  Might be nicer to
+      ;; keep point at "current" subgoal a la Isamode, but never mind
+      ;; just now.
+      (proof-display-and-keep-buffer proof-goals-buffer (point-min))))
+
+
+(defun proof-shell-analyse-structure1 (start end)
+  "Really analyse the structure here."
+  (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 char: this is the start of a top extent
+       ;; (assumption or goal)
+       ((= c proof-shell-goal-char)
+	(setq topl (cons cur topl))
+	(setq ap 0))
+
+       ;; Seen subterm start char: it's followed by at least 
+       ;; one subterm pointer byte
+       ((= c proof-shell-start-char)
+	(incf cur)
+	(if proof-analyse-using-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)) proof-shell-end-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 field char, which terminates an annotated position
+       ;; in the concrete syntax.  We make a highlighting span now.
+       ((and (consp stack) (= c proof-shell-field-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?
+	(if proof-analyse-using-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 subterm regions (goals) found
+    (setq topl (reverse (cons end topl)))
+    
+    ;; If we want Coq pbp: (setq coq-current-goal 1)
+    (if proof-goal-hyp-fn
+	(while (setq ip (car topl) 
+		     topl (cdr topl))
+	  (pbp-make-top-span ip (car topl))))
+
+    ;; Finally: strip the specials.  This should
+    ;; leave the spans in exactly the right place.
+    (proof-shell-strip-special-annotations-buf start end)))
+
+
+(defun pbp-make-top-span (start end)
+  "Make a top span (goal area) for mouse active output."
+  (let (span name)
+    (goto-char start)
+    ;; We need to skip an annotation here for proof-goal-hyp-fn
+    ;; to work again now we don't strip buffers.  Is it
+    ;; safe to assume that we're called exactly at proof-goal-char?
+    ;; [maybe except for last case?]
+    (forward-char)
+    (setq name (funcall proof-goal-hyp-fn))
+    (beginning-of-line)
+    (setq start (point))
+    (goto-char end)
+    (beginning-of-line)
+    (backward-char)
+    (setq span (make-span start (point)))
+    (set-span-property span 'mouse-face 'highlight)
+    (set-span-property span 'proof-top-element name)))
+
+
+(defun proof-shell-strip-special-annotations (string)
+  "Strip special annotations from a string, returning cleaned up string.
+*Special* annotations are characters with codes higher than
+'proof-shell-first-special-char'.
+If proof-shell-first-special-char is unset, return STRING unchanged."
+  (if proof-shell-first-special-char
+      (let* ((ip 0) (op 0) (l (length string)) (out (make-string l ?x )))
+	(while (< ip l)
+	  (if (>= (aref string ip) proof-shell-first-special-char)
+	      (if (char-equal (aref string ip) proof-shell-start-char)
+		  (progn (incf ip)
+			 (while 
+			     ;; FIXME: this relies on annotations 
+			     ;; being characters between 
+			     ;; \200 and \360 (first special char).
+			     ;; Why do we not just look for the 
+			     ;; field char??
+			     (< (aref string ip) 
+				proof-shell-first-special-char)
+			   (incf ip))))
+	    (aset out op (aref string ip))
+	    (incf op))
+	  (incf ip))
+	(substring out 0 op))
+    string))
+
+(defun proof-shell-strip-special-annotations-buf (start end)
+  "Strip specials and return new END value."
+  (let (c)
+    (goto-char start)
+    (while (< (point) end)
+      ;; FIXME: small OBO here: if char at end is special
+      ;; it won't be removed.
+      (if (>= (setq c (char-after (point))) 
+	      proof-shell-first-special-char)
+	  (progn
+	    (delete-char 1)
+	    (decf end)
+	    (if (char-equal c proof-shell-start-char)
+		(progn 
+		  ;; FIXME: could simply replace this by replace
+		  ;; match, matching on field-char??
+		  (while (and (< (point) end)
+			      (< (char-after (point))
+				 proof-shell-first-special-char))
+		    (delete-char 1)
+		    (decf end)))))
+	(forward-char)))
+    end))
+
+
+(provide 'pg-goals)
+;; pg-goals.el ends here.