implemented new buffer model. The goals buffer is now exclusively

reserved for goals.

8 files changed, 128 insertions, 59 deletions

diff --git a/Makefile.devel b/Makefile.devel
index 5c577b16..48ab9786 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -17,7 +17,7 @@
 ##    make rpm		  - make RPM packages based on etc/ProofGeneral.spec
 ##
 ##    make release	  - make tag, dist, and install it in RELEASEDIR.
-##    make releaseall	  - make release and rpmrelease.
+##    make releaseall	  - make release, local installation and rpmrelease.
 ##
 ##    make distinstall	  - install distribution build by 'make dist'
 ##			    into DISTINSTALLDIR.
@@ -332,7 +332,7 @@ releaseclean:
 ## releaseall:
 ##     Do everything!
 ##	  
-releaseall: release rpmrelease releaseclean
+releaseall: release rpmrelease distinstall releaseclean 
 
 ############################################################
 ##
diff --git a/generic/proof-config.el b/generic/proof-config.el
index b4f42458..9fcb13ec 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -198,6 +198,11 @@ Could come either from proof assistant or Proof General itself."
 ;; functions.  This is why prover-config appears under the
 ;; proof-general-internal group.
 
+(defcustom proof-assistant-home-page "http://www.dcs.ed.ac.uk/home/proofgen/"
+  "Web address of the proof assistant Proof General is using."
+  :type 'string
+  :group 'prover-config)
+
 (defcustom proof-assistant ""
   "Name of the proof assistant Proof General is using.
 This is set automatically by the mode stub defined in proof-site,
@@ -212,29 +217,38 @@ from the name given in proof-assistant-table."
 ;; 2. The major modes used by Proof General.
 ;;
 
-;; FIXME: these symbols could be set automatically to standard values,
+;; FIXME: these functions could be set automatically to standard values,
 ;; i.e. <assistant>-mode, <assistant>-shell-mode, <assistant>-pbp-mode.
 ;; FIXME: mode-for-script is unused at the moment, added just for
 ;; uniformity.  The other two are used when a shell buffer is started.
 
-(defcustom proof-mode-for-shell nil
+(defcustom proof-mode-for-shell 'proof-shell-mode
   "Mode for proof shell buffers.
+Usually customised for specific prover.
+Suggestion: this can be set in proof-pre-shell-start-hook."
+  :type 'function
+  :group 'prover-config)
+
+(defcustom proof-mode-for-response 'proof-response-mode
+  "Mode for proof response buffer.
+Usually customised for specific prover.
 Suggestion: this can be set in proof-pre-shell-start-hook."
-  :type 'symbol
+  :type 'function
   :group 'prover-config)
 
-(defcustom proof-mode-for-pbp nil
+(defcustom proof-mode-for-pbp 'pbp-mode
   "Mode for proof state display buffers.
+Usually customised for specific prover.
 Suggestion: this can be set in proof-pre-shell-start-hook."
-  :type 'symbol
+  :type 'function
   :group 'prover-config)
 
-(defcustom proof-mode-for-script nil
+(defcustom proof-mode-for-script 'ignore
   "Mode for proof script buffers.
 This is used by Proof General to find out which buffers 
 contain proof scripts.
 Suggestion: this can be set in the script mode configuration."
-  :type 'symbol
+  :type 'function
   :group 'prover-config)
 
 
diff --git a/generic/proof-script.el b/generic/proof-script.el
index fa09ede9..624a468e 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -272,10 +272,7 @@ to allow other files loaded by proof assistants to be marked read-only."
 (defun proof-warning (str)
   "Issue the warning STR."
     (proof-response-buffer-display str 'proof-warning-face)
-    (display-buffer proof-response-buffer)
-    (set-window-dedicated-p
-     (get-buffer-window proof-response-buffer) 'dedicated))
-
+    (proof-display-and-keep-buffer proof-response-buffer))
 
 (defun proof-register-possibly-new-processed-file (file)
   "Register a possibly new FILE as having been processed by the prover."
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index f39479c8..f4b31772 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -206,6 +206,8 @@ Does nothing if proof assistant is already running."
       (save-excursion
 	(set-buffer proof-shell-buffer)
 	(funcall proof-mode-for-shell)
+	(set-buffer proof-response-buffer)
+	(funcall proof-mode-for-response)
 	(set-buffer proof-pbp-buffer)
 	(funcall proof-mode-for-pbp))
 
@@ -338,7 +340,15 @@ Does nothing if proof assistant is already running."
 ;;   processed (assuming they're all successful)
 
 (defvar proof-shell-delayed-output nil
-  "Last interesting output from proof process output and what to do with it.")
+  "Last interesting output from proof process output and what to do with it.
+
+This is a list of tuples of the form (type . string). type is either
+'analyse or 'insert. 
+
+'analyse denotes that string's term structure  ought to be analysed
+         and displayed in the `proof-goals-buffer'
+'insert  denotes that string ought to be displayed in the
+         `proof-response-buffer' ")
 
 (defun proof-shell-analyse-structure (string)
   (save-excursion
@@ -351,7 +361,7 @@ Does nothing if proof assistant is already running."
 	    (progn (aset out op c)
 		   (incf op)))
 	(incf ip))
-      (display-buffer (set-buffer proof-pbp-buffer))
+      (proof-display-and-keep-buffer (set-buffer proof-pbp-buffer))
       (erase-buffer)
       (insert (substring out 0 op))
 
@@ -408,12 +418,10 @@ Does nothing if proof assistant is already running."
     (substring out 0 op)))
 
 (defun proof-shell-handle-output (start-regexp end-regexp append-face)
-  "Pretty print output in process buffer in specified region.
-The region begins with the match for START-REGEXP and is delimited by
+  "Displays output from `proof-shell-buffer' in
+  `proof-response-buffer'.
+The region in `proof-shell-buffer begins with the match for START-REGEXP and is delimited by
 END-REGEXP. The match for END-REGEXP is not part of the specified region.
-Removes any annotations in the region.
-Fontifies the region.
-Appends APPEND-FACE to the text property of the region .
 Returns the string (with faces) in the specified region."
   (let (start end string)
     (save-excursion
@@ -424,33 +432,38 @@ Returns the string (with faces) in the specified region."
 				   (length (match-string 0)))))
       (setq string
 	    (proof-shell-strip-annotations (buffer-substring start end)))
-      (delete-region start end)
+      (set-buffer proof-response-buffer)
+      (goto-char (point-max))
+      (newline)
+      (setq start (point-max))
       (insert string)
       (setq end (+ start (length string)))
+      ;; FIXME tms: FSF Emacs 20.2 problems
       ;; This doesn't work with FSF Emacs 20.2's version of Font-lock
       ;; because there are no known keywords in the process buffer
       ;; Never mind. In a forthcoming version, the process buffer will
       ;; not be tampered with. Fontification will take place in a
       ;; separate response buffer.
-      ;; (font-lock-fontify-region start end)
+      (font-lock-fontify-region start end)
       (font-lock-append-text-property start end 'face append-face)
       (buffer-substring start end))))
 
 (defun proof-shell-handle-delayed-output ()
+  "Display delayed output. 
+See the documentation fo `proof-shell-delayed-output' for furter details."
   (let ((ins (car proof-shell-delayed-output))
 	(str (cdr proof-shell-delayed-output)))
-    (display-buffer proof-pbp-buffer)
-    (save-excursion
-      (cond 
-       ((eq ins 'insert)
-	(setq str (proof-shell-strip-annotations str))
-	(set-buffer proof-pbp-buffer)
+    (cond 
+     ((eq ins 'insert)
+      (setq str (proof-shell-strip-annotations str))
+      (save-excursion
+	(set-buffer proof-response-buffer)
 	(erase-buffer)
 	(insert str))
-       ((eq ins 'analyse)
-	(proof-shell-analyse-structure str))
-       (t (set-buffer proof-pbp-buffer)
-	  (insert "\n\nbug???")))))
+      (proof-display-and-keep-buffer proof-response-buffer))
+     ((eq ins 'analyse)
+      (proof-shell-analyse-structure str))
+     (t (assert nil))))
   (run-hooks 'proof-shell-handle-delayed-output-hook)
   (setq proof-shell-delayed-output (cons 'insert "done")))
 
@@ -478,8 +491,8 @@ Returns the string (with faces) in the specified region."
 
 (defun proof-shell-handle-error (cmd string)
   "React on an error message triggered by the prover.
-We display the process buffer, scroll to the end, beep and fontify the
-error message. At the end it calls `proof-shell-handle-error-hook'. "
+The error message is displayed in the `proof-response-buffer'. Then,
+we call `proof-shell-handle-error-hook'. "
     ;; We extract all text between text matching
     ;; `proof-shell-error-regexp' and the following prompt.
     ;; Alternatively one could higlight all output between the
@@ -491,7 +504,7 @@ error message. At the end it calls `proof-shell-handle-error-hook'. "
   (proof-shell-handle-output
    proof-shell-error-regexp proof-shell-annotated-prompt-regexp
    'proof-error-face)
-  (save-excursion (display-buffer proof-shell-buffer)
+  (save-excursion (proof-display-and-keep-buffer proof-response-buffer)
 		  (beep)
 
 		  ;; unwind script buffer
@@ -559,10 +572,12 @@ assistant."
 
    ((and proof-shell-abort-goal-regexp
 	 (string-match proof-shell-abort-goal-regexp string))
-    (setq proof-shell-delayed-output (cons 'insert "\n\nAborted"))
+    (proof-clean-buffer proof-pbp-buffer)
+   (setq proof-shell-delayed-output (cons 'insert "\n\nAborted"))
     ())
 	 
    ((string-match proof-shell-proof-completed-regexp string)
+    (proof-clean-buffer proof-pbp-buffer)
     (setq proof-shell-proof-completed t)
     (setq proof-shell-delayed-output
 	  (cons 'insert (concat "\n" (match-string 0 string)))))
@@ -956,8 +971,25 @@ Annotations are characters 128-255."
 		  "Menu used in Proof General shell mode."
 		  (cons proof-mode-name (cdr proof-shell-menu)))
 
+(defun proof-font-lock-minor-mode ()
+  "Start font-lock as a minor mode in the current buffer."
+  (and (fboundp 'font-lock-set-defaults) (font-lock-set-defaults)))
+
+(defun proof-goals-config-done ()
+  "Initialise the goals buffer after the child has been configured."
+  (save-excursion
+    (set-buffer proof-pbp-buffer)
+    (proof-font-lock-minor-mode)))
+
+
+(defun proof-response-config-done ()
+  "Initialise the response buffer after the child has been configured."
+  (save-excursion
+    (set-buffer proof-response-buffer)
+    (proof-font-lock-minor-mode)))
+
 (defun proof-shell-config-done ()
-  "Initialise the specific proover after the child has been configured."
+  "Initialise the specific prover after the child has been configured."
   (save-excursion
     (set-buffer proof-shell-buffer)
     (accept-process-output (get-buffer-process proof-shell-buffer))
@@ -984,16 +1016,24 @@ Annotations are characters 128-255."
 	  ()
 	(error "Failed to initialise proof process")))))
 
+(eval-and-compile
+(define-derived-mode proof-universal-keys-only-mode fundamental-mode
+    proof-mode-name "Universal keymaps only"
+    (suppress-keymap proof-universal-keys-only-mode-map 'all)
+    (proof-define-keys pbp-mode-map proof-universal-keys)))
+
 (eval-and-compile			; to define vars
-(define-derived-mode pbp-mode fundamental-mode 
+(define-derived-mode pbp-mode proof-universal-keys-only-mode
   proof-mode-name "Proof by Pointing"
   ;; defined-derived-mode pbp-mode initialises pbp-mode-map
   (setq proof-buffer-type 'pbp)
-  (suppress-keymap pbp-mode-map 'all)
   ;; (define-key pbp-mode-map [(button2)] 'pbp-button-action)
-  (proof-define-keys pbp-mode-map proof-universal-keys)
   (erase-buffer)))
 
+(eval-and-compile
+(define-derived-mode proof-response-mode proof-universal-keys-only-mode
+  "PGResp" "Responses from Proof Assistant"
+  (setq proof-buffer-type 'response)))
 
 
 
diff --git a/generic/proof.el b/generic/proof.el
index 16149937..1d6580bc 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -103,6 +103,18 @@ The argument KBL is a list of tuples (k . f) where `k' is a keybinding
       ;; 
       (insert "\n"))))
 
+(defun proof-display-and-keep-buffer (buffer)
+  "Display BUFFER and mark window as dedicated."
+  (display-buffer buffer)
+  (set-window-dedicated-p (get-buffer-window buffer) 'dedicated))
+
+(defun proof-clean-buffer (buffer)
+  "Erase buffer and hide from display."
+  (save-excursion
+    (set-buffer buffer)
+    (erase-buffer))
+  (delete-windows-on buffer))
+
 ;;;
 ;;; Global variables
 ;;;
diff --git a/lego/lego-syntax.el b/lego/lego-syntax.el
index 20b0a326..f3a8f767 100644
--- a/lego/lego-syntax.el
+++ b/lego/lego-syntax.el
@@ -1,6 +1,6 @@
-;; lego-fontlock.el Font lock expressions for LEGO
-;; Copyright (C) 1994, 1995, 1996, 1997 LFCS Edinburgh. 
-;; Author: Healfdene Goguen, Thomas Kleymann and Dilip Sequeira
+;; lego-syntax.el Syntax of LEGO
+;; Copyright (C) 1994 - 1998 LFCS Edinburgh. 
+;; Author: Thomas Kleymann and Dilip Sequeira
 ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk>
 ;; Please let us know if you could maintain this package!
 ;;
@@ -63,7 +63,7 @@
   (list
 
    ; lambda binders
-     (list (lego-decl-defn-regexp "[:|]") 1
+     (list (lego-decl-defn-regexp "[:|?]") 1
 	   'proof-declaration-name-face)
 
      ; let binders
diff --git a/lego/lego.el b/lego/lego.el
index 869cf50a..3674979d 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -10,6 +10,8 @@
 ;;
 
 (require 'proof)
+(require 'proof-script)
+(require 'proof-shell)
 (require 'lego-syntax)
 
 ;; FIXME: outline should be autoloaded
@@ -178,10 +180,17 @@
    (easy-menu-change (list proof-mode-name) (car proof-help-menu)
 		     (append (cdr proof-help-menu) lego-help-menu-list)))
 
+(eval-and-compile
+  (define-derived-mode lego-response-mode proof-response-mode
+    "LEGOResp" nil
+    (setq font-lock-keywords lego-font-lock-terms)
+    (proof-response-config-done)))
+  
 (define-derived-mode lego-pbp-mode pbp-mode
-  "pbp" nil
+  "LEGOGoals" "LEGO Proof State"
   (lego-pbp-mode-config))
 
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Code that's lego specific                                      ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -354,9 +363,10 @@
 	     )))))
 
 (defun lego-pre-shell-start ()
-  (setq proof-prog-name lego-prog-name)
-  (setq proof-mode-for-shell 'lego-shell-mode)
-  (setq proof-mode-for-pbp 'lego-pbp-mode))
+  (setq proof-prog-name lego-prog-name
+	proof-mode-for-shell 'lego-shell-mode
+	proof-mode-for-response 'lego-response-mode
+	proof-mode-for-pbp 'lego-pbp-mode))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Configuring proof and pbp mode and setting up various utilities  ;;
@@ -365,7 +375,7 @@
 (defun lego-init-syntax-table ()
   "Set appropriate values for syntax table in current buffer."
 
-  (modify-syntax-entry ?_ "_")
+  (modify-syntax-entry ?_ "w")
   (modify-syntax-entry ?\' "_")
   (modify-syntax-entry ?\| ".")
   (modify-syntax-entry ?\* ". 23")
@@ -525,7 +535,9 @@ We assume that module identifiers coincide with file names."
 
 (defun lego-pbp-mode-config ()
   (setq pbp-change-goal "Next %s;"
-	pbp-error-regexp lego-error-regexp
-	))
+	pbp-error-regexp lego-error-regexp)
+  (setq font-lock-keywords lego-font-lock-terms)
+  (proof-goals-config-done))
+  
 
 (provide 'lego)
diff --git a/todo b/todo
index 861b4263..1d38d14e 100644
--- a/todo
+++ b/todo
@@ -59,6 +59,8 @@ C  Remove "FIXME notes" which are just notes I've put in about old
 
 C  Check on all FIXME notes.
 
+C  Toolbar icon for `proof-execute-minibuffer-cmd'
+
 A* Fixup for non-script buffer locking:
 
     proof-locked-end called from wrong buffer when error message
@@ -125,14 +127,6 @@ B Implement more generic mechanism for large undos (4h tms)
     LEGO: consider Discharge; perhaps unrol to the beginning of the
           module?
 
-A New buffer model (4h tms):
-
-    1. Script buffers
-    2. Response buffer
-    3. (optionally part of response buffer) goals buffer
-    4. (hidden) process buffer
-    5. Minibuffer for additionally sending information to the process 
-
 A Revise ProofGeneral.texi and publish LaTeX version as an LFCS
   Technical Report (2 days; da + tms)