Added option for sending qed output to goals buffer for Isabelle

2 files changed, 59 insertions, 19 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 4ec803ee..24ab08d5 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -95,7 +95,6 @@ it is called to take some action for the new setting."
   :type 'boolean
   :group 'proof-user-options)
 
-
 (defcustom proof-electric-terminator-enable nil 
   "*If non-nil, use electric terminator mode on start-up.
 If electric terminator mode is enabled, pressing a terminator will 
@@ -122,7 +121,11 @@ inside your Emacs."
   :group 'proof-user-options)
 
 (defcustom proof-output-fontify-enable t
-  "*Whether to fontify output from the proof assistant."
+  "*Whether to fontify output from the proof assistant.
+If non-nil, output from the proof assistant will be highlighted
+in the goals and response buffers.
+(This is providing font-lock-keywords have been set for the 
+buffer modes)."
   :type 'boolean
   :group 'proof-user-options)
 
@@ -170,7 +173,8 @@ experienced Emacs users."
   :type 'boolean 
   :group 'proof-user-options)
 
-(defcustom proof-auto-delete-windows nil
+(defcustom proof-auto-delete-windows 
+  nil
   "*If non-nil, automatically remove windows when they are cleaned.
 For example, at the end of a proof the goals buffer window will
 be cleared; if this flag is set it will automatically be removed.
@@ -181,7 +185,8 @@ selected frame will be automatically deleted."
   :type 'boolean
   :group 'proof-user-options)
 
-(defcustom proof-toolbar-use-button-enablers t
+(defcustom proof-toolbar-use-button-enablers 
+  t
   "*If non-nil, toolbars buttons may be enabled/disabled automatically.
 Toolbar buttons can be automatically enabled/disabled according to
 the context.  Set this variable to nil if you don't like this feature
@@ -196,7 +201,7 @@ next start Proof General."
   :type 'boolean
   :group 'proof-user-options)
 
-(defcustom proof-auto-retract
+(defcustom proof-auto-retract 
   nil
   "*If non-nil, retract automatically when locked region is edited.
 With this option active, the locked region will automatically be
@@ -207,7 +212,7 @@ Note: this feature has not been implemented yet, it is only an idea."
   :type 'boolean
   :group 'proof-user-options)
 
-(defcustom proof-query-file-save-when-activating-scripting
+(defcustom proof-query-file-save-when-activating-scripting 
   t
 "*If non-nil, query user to save files when activating scripting.
 
@@ -223,7 +228,8 @@ files which are out of date with respect to the lodead buffers!"
   :type 'boolean
   :group 'proof-user-options)
 
-(defcustom proof-script-indent nil
+(defcustom proof-script-indent 
+  nil
   ;; Particular proof assistants can enable this if they feel
   ;; confident about it.  (I don't). -da
   "*If non-nil, enable indentation code for proof scripts.
@@ -233,25 +239,29 @@ provers.  Enable it if it works for you."
   :type 'boolean 
   :group 'proof-user-options)
 
-(defcustom proof-prog-name-ask nil
+;; FIXME: implement it!  Use in indentation code.
+(defcustom proof-one-command-per-line 
+  nil
+  "*If non-nil, format for newlines after each proof command in a script.
+This option is not fully-functional at the moment."
+  :type 'boolean
+  :group 'proof-user-options)
+
+
+(defcustom proof-prog-name-ask 
+  nil
   "*If non-nil, query user which program to run for the inferior process."
   :type 'boolean
   :group 'proof-user-options)
 
-(defcustom proof-prog-name-guess nil
+(defcustom proof-prog-name-guess 
+  nil
   "*If non-nil, use `proof-guess-command-line' to guess proof-prog-name.
 This option is compatible with proof-prog-name-ask.
 No effect if proof-guess-command-line is nil."
   :type 'boolean
   :group 'proof-user-options)
 
-;; FIXME: rationalize and combine next two
-(defcustom proof-one-command-per-line nil
-  "*If non-nil, format for newlines after each proof command in a script.
-This option is not fully-functional at the moment."
-  :type 'boolean
-  :group 'proof-user-options)
-
 (defcustom proof-tidy-response
   t
   "*Non-nil indicates that the response buffer should be cleared often.
@@ -275,6 +285,8 @@ you should set `proof-tidy-response' to nil."
   :type 'boolean
   :group 'proof-user-options)
 
+;;; NON BOOLEAN OPTIONS 
+
 (defcustom proof-toolbar-follow-mode 'locked
   "*Choice of how point moves with toolbar commands.
 One of the symbols: 'locked, 'follow, 'ignore.
@@ -1420,6 +1432,17 @@ See documentation of proof-shell-start-char."
   :type '(choice character (const nil))
   :group 'proof-goals)
 
+(defcustom proof-goals-display-qed-message nil
+  "If non-nil, display the proof-completed message in the goals buffer.
+For some proof assistants (e.g. Isabelle) it seems aesthetic to
+display the QED message in the goals buffer, even though it doesn't
+contain any goals and shouldn't be marked up for proof-by-pointing.
+
+If this setting is non-nil, QED messages appear in the goals
+buffer.  Otherwise they appear in the response buffer."
+  :type 'boolean
+  :group 'proof-goals)
+
 
 
 ;;
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 44ef4e5e..ba32e565 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -639,7 +639,9 @@ This is a list of tuples of the form (TYPE . STRING). type is either
          `proof-response-buffer' ")
 
 (defun proof-shell-analyse-structure (string)
-  "Analyse the term structure of STRING and display it in proof-goals-buffer."
+  "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
     (let* ((ip 0) (op 0) ap (l (length string)) 
 	   (ann (make-string (length string) ?x))
@@ -649,7 +651,14 @@ This is a list of tuples of the form (TYPE . STRING). type is either
 
       ;; Form output string by removing characters 128 or greater,
       ;; (ALL annotations), unless proof-shell-leave-annotations-in-output 
-      ;; is set.
+      ;; is set.  
+
+      ;; FIXME da: this can be removed now that we strip annotations
+      ;; immediately after fontification in proof-fontify-region.  We
+      ;; may no longer need the setting
+      ;; proof-shell-leave-annotations-in-ouput, unless it breaks LEGO
+      ;; font lock patterns for example.
+
       (unless proof-shell-leave-annotations-in-output
 	(while (< ip l)	
 	  (if (< (setq c (aref string ip)) 128)
@@ -698,6 +707,10 @@ This is a list of tuples of the form (TYPE . STRING). type is either
       ;; character codes in this buffer 8 bit)
       ;; But this is a more general problem in Proof General
       ;; which requires re-engineering all this 128 mess.
+      ;; FIXME Mk II:
+      ;; This is also going to be broken for X-Symbol interaction,
+      ;; when tokens (several chars long) are replaced by single
+      ;; characters.
       (unless
 	  ;; Don't do it for Emacs 20.3 or any version which
 	  ;; has this suspicious function.
@@ -760,6 +773,7 @@ This is a list of tuples of the form (TYPE . STRING). type is either
       (incf ip))
     (substring out 0 op)))
 
+;; FIXME: dead code
 (defun proof-shell-strip-eager-annotation-specials (string)
   "Strip special eager annotations from STRING, returning cleaned up string.
 The input STRING should be annotated with expressions matching
@@ -879,6 +893,7 @@ See the documentation for `proof-shell-delayed-output' for further details."
 ;; FIXME da: the magical use of "Done." and "done" as values in
 ;; proof-shell-handled-delayed-output is horrendous.  Should
 ;; be changed to something more understandable!!
+
 (defun proof-shell-handle-error (cmd string)
   "React on an error message triggered by the prover.
 Called with shell buffer current.
@@ -997,7 +1012,9 @@ assistant."
     (proof-clean-buffer proof-goals-buffer)
     (setq proof-shell-proof-completed t)
     (setq proof-shell-delayed-output
-	  (cons 'insert (concat "\n" (match-string 1 string)))))
+	  (cons (if proof-goals-display-qed-message
+		    'analyse 'insert)
+		(match-string 1 string))))
 
    ((proof-shell-string-match-safe proof-shell-start-goals-regexp string)
     (setq proof-shell-proof-completed nil)