merge ProofTreeBranch into main trunk:

- add support for proof-tree displays (currently Coq only)
- new file generic/proof-tree.el contains generic code
- Coq specific code has been added to coq/coq.el

Changes to existing Proof General functions:
- proof-shell-exec-loop and proof-shell-filter-manage-output call
  proof-tree display functions, when the proof-tree display is on
- proof-shell-exec-loop returns t if proof-action-list is empty
  _or_ contains only items for updating the proof-tree
- proof-shell-should-be-silent returns nil when the proof-tree
  display is on
- coq-last-prompt-info, coq-last-prompt-info-safe return as
  additional 4th element the name of the current proof

12 files changed, 1967 insertions, 36 deletions

diff --git a/coq/coq.el b/coq/coq.el
index c7ad9650..f36e4edd 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -23,6 +23,7 @@
     (defvar smie-indent-basic nil)
     (defvar smie-rules-function nil))
   (defvar queueitems nil)       ; dynamic scope in p-s-extend-queue-hook
+  (defvar proof-info nil)       ; dynamic scope in proof-tree-urgent-action
   (defvar coq-time-commands nil)        ; defpacustom
   (defvar coq-use-editing-holes nil)    ; defpacustom
   (defvar coq-compile-before-require nil)       ; defpacustom
@@ -190,6 +191,82 @@ A setting of nil means show all output from Coq. See also
 
 
 ;;
+;; prooftree customization
+;;
+
+(defgroup coq-proof-tree ()
+  "Coq specific customization for prooftree."
+  :group 'coq-config
+  :package-version '(ProofGeneral . "4.2"))
+
+(defcustom coq-proof-tree-ignored-commands-regexp
+  "^\\(Show\\)\\|\\(Locate\\)"
+  "Regexp for `proof-tree-ignored-commands-regexp'."
+  :type 'regexp
+  :group 'coq-proof-tree)
+
+(defcustom coq-navigation-command-regexp
+  "^\\(Focus\\)\\|\\(Unfocus\\)"
+  "Regexp for `proof-tree-navigation-command-regexp'."
+  :type 'regexp
+  :group 'coq-proof-tree)
+
+(defcustom coq-proof-tree-cheating-regexp
+  "admit"
+  "Regexp for `proof-tree-cheating-regexp'."
+  :type 'regexp
+  :group 'coq-proof-tree)
+
+(defcustom coq-proof-tree-current-goal-regexp
+  (concat "^[0-9]+ subgoal\\(?:s, subgoal 1\\)? "
+	  "(ID \\([0-9]+\\))\n\\s-*\n\\(\\(?:.+\n\\)*\\)\\(?:\n\\|$\\)")
+  "Regexp for `proof-tree-current-goal-regexp'."
+  :type 'regexp
+  :group 'coq-proof-tree)
+
+(defcustom coq-proof-tree-update-goal-regexp
+  (concat "^goal / evar \\([0-9]+\\) is:\n"
+          "\\s-*\n\\(\\(?:.+\n\\)*\\)\\(?:\n\\|$\\)")
+  "Regexp for `proof-tree-update-goal-regexp'."
+  :type 'regexp
+  :group 'coq-proof-tree)
+
+(defcustom coq-proof-tree-additional-subgoal-ID-regexp
+  "^subgoal [0-9]+ (ID \\([0-9]+\\)) is:"
+  "Regexp for `proof-tree-additional-subgoal-ID-regexp'."
+  :type 'regexp
+  :group 'coq-proof-tree)
+
+(defcustom coq-proof-tree-existential-regexp "\\(\\?[0-9]+\\)"
+  "Regexp for `proof-tree-existential-regexp'."
+  :type 'regexp
+  :group 'coq-proof-tree)
+
+(defcustom coq-proof-tree-instantiated-existential-regexp
+  (concat coq-proof-tree-existential-regexp " using")
+  "Regexp for recognizing an instantiated existential variable."
+  :type 'regexp
+  :group 'coq-proof-tree)
+
+(defcustom coq-proof-tree-existentials-state-start-regexp
+  "^(dependent evars:"
+  "Coq instance of `proof-tree-existentials-state-start-regexp'."
+  :type 'regexp
+  :group 'coq-proof-tree)
+
+(defcustom coq-proof-tree-existentials-state-end-regexp ")\n"
+  "Coq instance of `proof-tree-existentials-state-end-regexp'."
+  :type 'regexp
+  :group 'coq-proof-tree)
+
+(defcustom coq-proof-tree-proof-completed-regexp
+  "^\\(?:Proof completed\\)\\|\\(?:No more subgoals\\)\\."
+  "Regexp for `proof-tree-proof-completed-regexp'."
+  :type 'regexp
+  :group 'coq-proof-tree)
+
+
+;;
 ;; Outline mode
 ;;
 
@@ -635,18 +712,26 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies."
   "Extract info from the coq prompt S.  See `coq-last-prompt-info-safe'."
   (let ((lastprompt (or s (error "No prompt !!?")))
         (regex
-         (concat "\\(" coq-id-shy "\\) < \\([0-9]+\\) |\\(\\(?:" coq-id-shy
+         (concat ">\\(" coq-id-shy "\\) < \\([0-9]+\\) |\\(\\(?:" coq-id-shy
                  "|?\\)*\\)| \\([0-9]+\\) < ")))
     (when (string-match regex lastprompt)
-      (list (string-to-number (match-string 2 lastprompt))
-            (string-to-number (match-string 4 lastprompt))
-            (build-list-id-from-string (match-string 3 lastprompt))))))
+      (let ((current-proof-name (match-string 1 lastprompt))
+            (state-number (string-to-number (match-string 2 lastprompt)))
+            (proof-state-number (string-to-number (match-string 4 lastprompt)))
+            ;; bind pending-proofs last, because build-list-id-from-string
+            ;; modifies the match data
+            (pending-proofs
+             (build-list-id-from-string (match-string 3 lastprompt))))
+        (list state-number proof-state-number pending-proofs
+              (if pending-proofs current-proof-name nil))))))
 
 
 (defun coq-last-prompt-info-safe ()
   "Return a list with all informations from the last prompt.
-The list contains the state number, the proof stack depth, and the names of all
-pending proofs (in a list)."
+The list contains in the following order the state number, the
+proof stack depth, a list with the names of all pending proofs,
+and as last element the name of the current proof (or nil if
+there is none)."
   (coq-last-prompt-info proof-shell-last-prompt))
 
 (defvar coq-last-but-one-statenum 1
@@ -750,7 +835,7 @@ If locked span already has a state number, then do nothing. Also updates
       ;; infos = promt infos of the very last prompt
       ;; sp = last locked span, which we want to fill with prompt infos
       (let ((sp    (if proof-script-buffer (proof-last-locked-span)))
-            (infos (or (coq-last-prompt-info-safe) '(0 0 nil))))
+            (infos (or (coq-last-prompt-info-safe) '(0 0 nil nil))))
         (unless (or (not sp) (coq-get-span-statenum sp))
           (coq-set-span-statenum sp coq-last-but-one-statenum))
         (setq coq-last-but-one-statenum (car infos))
@@ -1152,6 +1237,13 @@ This is specific to `coq-mode'."
   ;; holes
   (if coq-use-editing-holes (holes-mode 1))
 
+  ;; prooftree config
+  (setq
+   proof-tree-configured t
+   proof-tree-get-proof-info 'coq-proof-tree-get-proof-info
+   proof-tree-find-begin-of-unfinished-proof
+     'coq-find-begin-of-unfinished-proof)   
+
   (proof-config-done)
 
   ;; outline
@@ -1223,6 +1315,27 @@ This is specific to `coq-mode'."
   (coq-init-syntax-table)
   ;; (holes-mode 1)  da: does the shell really need holes mode on?
   (setq proof-shell-font-lock-keywords 'coq-font-lock-keywords-1)
+
+  ;; prooftree config
+  (setq
+   proof-tree-ignored-commands-regexp coq-proof-tree-ignored-commands-regexp
+   proof-tree-navigation-command-regexp coq-navigation-command-regexp
+   proof-tree-cheating-regexp coq-proof-tree-cheating-regexp
+   proof-tree-current-goal-regexp coq-proof-tree-current-goal-regexp
+   proof-tree-update-goal-regexp coq-proof-tree-update-goal-regexp
+   proof-tree-existential-regexp coq-proof-tree-existential-regexp
+   proof-tree-existentials-state-start-regexp
+                      coq-proof-tree-existentials-state-start-regexp
+   proof-tree-existentials-state-end-regexp
+                        coq-proof-tree-existentials-state-end-regexp
+   proof-tree-additional-subgoal-ID-regexp
+                              coq-proof-tree-additional-subgoal-ID-regexp
+   proof-tree-proof-completed-regexp coq-proof-tree-proof-completed-regexp
+   proof-tree-extract-instantiated-existentials
+     'coq-extract-instantiated-existentials
+   proof-tree-show-sequent-command 'coq-show-sequent-command
+   )
+        
   (proof-shell-config-done))
 
 (defun coq-goals-mode-config ()
@@ -2110,6 +2223,97 @@ correct in the new scripting buffer."
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
+;; prooftree support
+;;
+
+(defun coq-proof-tree-get-proof-info ()
+  "Coq instance of `proof-tree-get-proof-info'."
+  (let* ((info (or (coq-last-prompt-info-safe) '(0 0 nil nil))))
+         ;; info is now a list with
+         ;; * the state number
+         ;; * the proof stack depth
+         ;; * the list of all open proofs
+         ;; * the name of the current proof or nil
+    (list (car info) (nth 3 info))))
+
+(defun coq-extract-instantiated-existentials (start end)
+  "Coq specific function for `proof-tree-extract-instantiated-existentials'.
+Returns the list of currently instantiated existential variables."
+  (proof-tree-extract-list
+   start end
+   coq-proof-tree-existentials-state-start-regexp
+   coq-proof-tree-existentials-state-end-regexp
+   coq-proof-tree-instantiated-existential-regexp))
+
+(defun coq-show-sequent-command (sequent-id)
+  "Coq specific function for `proof-tree-show-sequent-command'."
+  (format "Show Goal \"%s\"." sequent-id))
+
+(defun coq-proof-tree-get-new-subgoals ()
+  "Check for new subgoals and issue appropriate Show commands.
+This is a hook function for `proof-tree-urgent-action-hook'. This
+function examines the current goal output and searches for new
+unknown subgoals. Those subgoals have been generated by the last
+proof command and we must send their complete sequent text
+eventually to prooftree. Because subgoals may change with
+the next proof command, we must execute the additionally needed
+Show commands before the next real proof command.
+
+The ID's of the open goals are checked with
+`proof-tree-sequent-hash' in order to find out if they are new.
+For any new goal an appropriate Show Goal command with a
+'proof-tree-show-subgoal flag is inserted into
+`proof-action-list'. Then, in the normal delayed output
+processing, the sequent text is send to prooftree as a sequent
+update (see `proof-tree-update-sequent') and the ID of the
+sequent is registered as known in `proof-tree-sequent-hash'.
+
+The not yet delayed output is in the region
+\[proof-shell-delayed-output-start, proof-shell-delayed-output-end]."
+  ;; (message "CPTGNS start %s end %s"
+  ;;          proof-shell-delayed-output-start
+  ;;          proof-shell-delayed-output-end)
+  (with-current-buffer proof-shell-buffer
+    (let ((start proof-shell-delayed-output-start)
+          (end proof-shell-delayed-output-end))
+      (goto-char start)
+      (while (proof-re-search-forward
+              coq-proof-tree-additional-subgoal-ID-regexp end t)
+        (let ((subgoal-id (match-string-no-properties 1)))
+          (unless (gethash subgoal-id proof-tree-sequent-hash)
+            (setq proof-action-list
+                  (cons (proof-shell-action-list-item
+                         (coq-show-sequent-command subgoal-id)
+                         (proof-tree-make-show-goal-callback (car proof-info))
+                         '(no-goals-display
+                           no-response-display
+                           proof-tree-show-subgoal))
+                        proof-action-list))))))))
+  
+(add-hook 'proof-tree-urgent-action-hook 'coq-proof-tree-get-new-subgoals)
+
+
+(defun coq-find-begin-of-unfinished-proof ()
+  "Return start position of current unfinished proof or nil."
+  (let ((span (span-at (1- (proof-unprocessed-begin)) 'type)))
+    ;; go backward as long as we are inside the proof
+    ;; the proofstack property is set inside the proof
+    ;; the command before the proof has the goalcmd property
+    (while (and span
+                (span-property span 'proofstack)
+                (not (span-property span 'goalcmd)))
+          (setq span (span-at (1- (span-start span)) 'type)))
+    ;; Beware of completed proofs! They have type goalsave and for
+    ;; strange reasons the whole completed proof has the goalcmd property.
+    (if (and span
+             (not (eq 'goalsave (span-property span 'type)))
+             (span-property span 'goalcmd))
+        (span-start span)
+      nil)))
+    
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
 ;; Pre-processing of input string
 ;;
 
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index 7574e0f1..b039d187 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -161,6 +161,7 @@ Proof General.
 * Configuring Editing Syntax::
 * Configuring Font Lock::
 * Configuring Tokens::
+* Configuring Proof-Tree Visualization::
 * Writing More Lisp Code::
 * Internals of Proof General::  
 * Plans and Ideas::             
@@ -1655,6 +1656,7 @@ Regexp matching the start of the proof state output.@*
 This is an important setting.  Output between @samp{@code{proof-shell-start-goals-regexp}}
 and @samp{@code{proof-shell-end-goals-regexp}} will be pasted into the goals buffer
 and possibly analysed further for proof-by-pointing markup.
+If it is left as nil, the goals buffer will not be used.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-shell-end-goals-regexp
 @defvar proof-shell-end-goals-regexp 
@@ -2465,6 +2467,407 @@ tokens (for example, editing documentation or source code files).
 
 
 
+@node Configuring Proof-Tree Visualization
+@chapter Configuring Proof-Tree Visualization
+
+The proof-tree visualization feature was written with the idea of
+supporting Coq as well as other proof assistants. Nevertheless,
+supporting proof-tree visualization for a second proof assistant
+will almost certainly require changes in the generic Elisp code
+in @code{generic/proof-tree.el} as well as in the
+Prooftree program.
+
+@menu
+* Prerequisites::
+* Proof-Tree Display Internals::
+* Configuring Prooftree for a New Proof Assistant::
+@end menu
+
+
+@node Prerequisites
+@section Prerequisites
+
+Proof-tree visualization requires certain support from the proof
+assistant. Patching the proof assistant is therefore the first
+step of adding support for proof-tree visualization. The
+following features are needed.
+
+@table @asis
+@item Unique goal identification
+The proof assistant must assign and output a unique string for
+each goal. For Coq the internal @code{evar} index number is used,
+which is printed for each goal in the form @code{(ID XXX)} when
+Coq is started with the option @code{-emacs}.
+
+The unique goal identification is needed to distinguish newly
+spawned subgoals from older open subgoals and to mark the current
+goal in the proof-tree display.
+
+@item Indication of newly generated subgoals
+A proof command that spawns additional subgoals must somehow
+indicate the goal ID's of these new subgoals. Otherwise the
+proof-tree display will not be able to reconstruct the proof-tree
+structure. 
+
+For Coq the newly spawned subgoals appear always in the list of
+additional subgoals below the current goal. Note, that it is not
+required to mark the newly spawned subgoals. They may appear in a
+mixed list with older open subgoals. Note further, that it is not
+required that always the complete set of all open subgoals is
+printed (which is indeed not the case after of @code{Focus}
+command in Coq). It is only required that the goal ID's of all
+newly spawned subgoals is somehow printed.
+
+@item State number for undo
+There must be a state number that is strictly increasing when
+asserting proof commands and that is reset to the appropriate
+number after retracting some proof commands.
+
+For Coq the state number in the extended prompt (visible only
+with option @code{-emacs}) is used. 
+
+@item Information about existential variables
+Existential variables are placeholders that might or must be
+instantiated later in the proof. Prooftree supports
+existential variables with three features. Firstly, it can update
+goals when existential variables get instantiated. Secondly, it
+can mark the proof commands that introduced or instantiated
+existential variables and, thirdly, it can display and track
+dependencies between existential variables.
+
+For the first feature, the proof assistant must list the currently
+instantiated existential variables for every goal. For the second
+feature it must additionally list the not instantiated
+existential variables. Finally, for the third feature, it must
+display the dependencies for instantiated existential variables.
+
+For Coq, all necessary information is provided in the existential
+evar line, that is printed with the @code{-emacs} switch.
+
+@end table
+
+
+@node Proof-Tree Display Internals
+@section Proof-Tree Display Internals
+
+This section gives some information about the inner structure of
+the code that realizes the proof-tree display. The idea here is
+that this section provides the background information to make the
+documentation of the customizable variables of the proof-tree
+Elisp code easy to understand.
+
+@menu
+* Organization of the Code::
+* Communication::
+* Guards::
+* Urgent and Delayed Actions::
+* Full Annotation::
+@end menu
+
+
+@node Organization of the Code
+@subsection Organization of the Code
+
+The proof-tree display is realized by Proof General in
+cooperation with the external Prooftree program. The
+latter is a GTK application in OCaml. Both, the Elisp code in
+Proof General and the Prooftree OCaml code is divided into
+a generic and a proof assistant specific part.
+
+The generic Elisp code lives in @code{generic/proof-tree.el}. As
+usual in Proof General, it contains various customizable
+variables, which the proof assistant specific code must set. Most
+of these variables contain regular expressions, but there are also
+some that hold functions. The Coq specific code for the
+proof-tree display is distributed in a few chunks over
+@code{coq/coq.el}. 
+
+The main task of the Elisp code is to extract goals, undo events
+and information about existential variables from the
+proof-assistant output and to send all this data to Prooftree.
+The Elisp code does also determine if additional output must be
+requested from the proof assistant. In that case it adds
+appropriate commands to @code{proof-action-list}, @pxref{Proof
+script mode}. These additional commands are flagged with
+@code{proof-tree-show-subgoal}, @code{no-goals-display} and
+@code{no-response-display}. The flag
+@code{proof-tree-show-subgoal} ensures that a number of internal
+functions ignore these additional commands. The other two flags
+ensure that their output is neither displayed in the goals nor
+the response buffer.
+
+For the decision about which goals must be sent to Prooftree, the
+Elisp code maintains the following two state variables.
+
+@c TEXI DOCSTRING MAGIC: proof-tree-sequent-hash
+@defvar proof-tree-sequent-hash 
+Hash table to remember sequent ID's.@*
+Needed because some proof assistants do not distinguish between
+new subgoals, which have been created by the last proof command,
+and older, currently unfocussed subgoals. If Proof General meets
+a goal, it is treated as new subgoal if it is not in this hash yet.
+
+The hash is mostly used as a set of sequent ID's. However, for
+undo operations it is necessary to delete all those sequents from
+the hash that have been created in a state later than the undo
+state. For this purpose this hash maps sequent ID's to the state
+number in which the sequent has been created.
+
+The hash table is initialized in @samp{@code{proof-tree-start-process}}.
+@end defvar
+
+
+@c TEXI DOCSTRING MAGIC: proof-tree-existentials-alist
+@defvar proof-tree-existentials-alist 
+Alist mapping existential variables to sequent ID's.@*
+Used to remember which goals need a refresh when an existential
+variable gets instantiated. To support undo commands the old
+contents of this list must be stored in
+@samp{@code{proof-tree-existentials-alist-history}}. To ensure undo is
+properly working, this variable should only be changed by using
+@samp{@code{proof-tree-delete-existential-assoc}},
+@samp{@code{proof-tree-add-existential-assoc}} or
+@samp{@code{proof-tree-reset-existentials}}.
+@end defvar
+
+When retracting these two variables must be set to their previous
+state. For @code{proof-tree-sequent-hash} this is done with the
+state numbers that are stored in the hash. For
+@code{proof-tree-existentials-alist} a separate alist stores
+previous states.
+
+@c TEXI DOCSTRING MAGIC: proof-tree-existentials-alist-history
+@defvar proof-tree-existentials-alist-history 
+Alist mapping state numbers to old values of @samp{@code{proof-tree-existentials-alist}}.@*
+Needed for undo.
+@end defvar
+
+
+In Prooftree the separation between generic and proof-assistant
+specific code is less obvious. The Coq specific code is in the
+file @code{coq.ml}. All the remaining code is generic. 
+
+Prooftree opens for each proof a separate window. It reconstructs
+the proof tree and orders the existential variables in a
+dependency hierarchy. It stores a complete history of previous
+states to support arbitrary undo operations. Under normal
+circumstances one starts just one Prooftree process that keeps
+running for the remainder of the Proof General session,
+regardless of how many proof-tree windows are displayed.
+
+A fair amount of the Prooftree code is documented with
+@code{ocamldoc} documentation comments. With @code{make doc} they
+can be converted into a set of html pages in the @code{doc}
+subdirectory.
+
+
+@node Communication
+@subsection Communication
+
+Prooftree is a standard Emacs subprocess that reads goals and
+other proof status messages from its standard input. The
+communication between Proof General and Prooftree is almost one
+way only. Proof General sends proof status messages to Prooftree,
+from which Prooftree reconstructs the current proof status and
+the complete proof tree. Prooftree never requests additional
+information from Proof General. The only message that is sent
+from Prooftree to Proof General is a @code{stop-displaying}
+command, when the user closes the proof-tree display of the
+current proof.
+
+The communication protocol is completely described in the
+@code{ocamldoc} documentation of @code{input.ml} in the Prooftree
+sources. All messages consist of UTF-8 encoded human-readable
+strings. The strings have either a fixed length or their byte-length
+is encoded in the message before the string itself. 
+
+For debugging purposes Prooftree can save all input in a file.
+This feature can be turned on in the @code{Debug} tab of the
+Prooftree configuration dialog or with option @code{-tee}.
+
+
+@node Guards
+@subsection Guards
+
+The proof-tree display code inside Proof General uses two guard
+variables. 
+
+@c TEXI DOCSTRING MAGIC: proof-tree-configured
+@defvar proof-tree-configured 
+Whether external proof-tree display is configured.@*
+This boolean enables the proof-tree menu entry and the function
+that starts external proof-tree display.
+@end defvar
+
+@c TEXI DOCSTRING MAGIC: proof-tree-external-display
+@defvar proof-tree-external-display 
+Display proof trees in external prooftree windows if t.@*
+Actually, if this variable is t then the user requested an
+external proof-tree display. If there was no unfinished proof
+when proof-tree display was requested and if no proof has been
+started since then, then there is obviously no proof-tree
+display. In this case, this variable stays t and the proof-tree
+display will be started for the next proof.
+
+Controlled by @samp{@code{proof-tree-external-display-toggle}}.
+@end defvar
+
+In Proof General, the code for the external proof-tree display is
+called from the proof-shell filter function in
+@code{proof-shell-exec-loop} and
+@code{proof-shell-filter-manage-output}, @pxref{Proof shell
+mode}. The variable @code{proof-tree-external-display} is a guard
+for these calls, to ensure that the proof-tree specific code is
+only called if the user requested a proof-tree display.
+
+The whole proof-tree package contains only one function that can
+be called interactively:
+@code{proof-tree-external-display-toggle}, which switches
+@code{proof-tree-external-display} on and off. When
+@code{proof-tree-configured} is @code{nil},
+@code{proof-tree-external-display-toggle} aborts with an error
+message. 
+
+@c TEXI DOCSTRING MAGIC: proof-tree-external-display-toggle
+@deffn Command proof-tree-external-display-toggle 
+Toggle the external proof-tree display.@*
+When called outside a proof the external proof-tree display will
+be enabled for the next proof. When called inside a proof the
+proof display will be created for the current proof. If the
+external proof-tree display is currently on, then this toggle
+will switch it off. At the end of the proof the proof-tree
+display is switched off.
+@end deffn
+
+
+@node Urgent and Delayed Actions
+@subsection Urgent and Delayed Actions
+
+The proof-shell filter functions contains two calls to proof-tree
+specific code. One for urgent actions and one for all remaining
+actions, that can be delayed.
+
+Urgent actions are those that must be executed before
+@code{proof-shell-exec-loop} sends the next item from
+@code{proof-action-list} to the proof assistant. For execution
+speed, the amount of urgent code should be kept small.
+
+@c TEXI DOCSTRING MAGIC: proof-tree-urgent-action
+@defun proof-tree-urgent-action flags
+Handle urgent points before the next item is sent to the proof assistant.@*
+Schedule goal updates when existential variables have changed and
+call @samp{@code{proof-tree-urgent-action-hook}}. All this is only done if
+the current output does not come from a command (with the
+@code{'proof-tree-show-subgoal} flag) that this package inserted itself.
+
+Urgent actions are only needed if the external proof display is
+currently running. Therefore this function should not be called
+when @samp{@code{proof-tree-external-display}} is nil. 
+
+This function assumes that the prover output is not suppressed.
+Therefore, @samp{@code{proof-tree-external-display}} being t is actually a
+necessary precondition.
+
+The not yet delayed output is in the region
+[@code{proof-shell-delayed-output-start}, @code{proof-shell-delayed-output-end}].
+@end defun
+
+
+The function @code{proof-tree-urgent-action} is called at a point
+where it is save to manipulate @code{proof-action-list}. This is
+essential, because @code{proof-tree-urgent-action} inserts goal
+display commands into @code{proof-action-list} when existential
+variables got instantiated and when the sequent text from newly
+created subgoals is missing.
+
+
+Most of the proof-tree specific code runs when the proof
+assistant is already busy with the next item from
+@code{proof-action-list}. 
+
+@c TEXI DOCSTRING MAGIC: proof-tree-handle-delayed-output
+@defun proof-tree-handle-delayed-output cmd flags span
+Process delayed output for prooftree.@*
+This function is the main entry point of the Proof General
+prooftree support. It examines the delayed output in order to
+take appropriate actions and maintains the internal state.
+
+All arguments are (former) fields of the @samp{@code{proof-action-list}}
+entry that is now finally retired. @var{cmd} is the command, @var{flags} are
+the flags and @var{span} is the span.
+@end defun
+
+The function @code{proof-tree-handle-delayed-output} does all the
+communication with Prooftree. 
+
+
+@node Full Annotation
+@subsection Full Annotation
+
+In the default configuration Proof General switches the proof
+assistant into quiet mode if there are more than
+@code{proof-shell-silent-threshold} items in
+@code{proof-action-list}, see Section @i{Document centred
+working} (in Chapter @i{Advanced Script Management and Editing})
+in the @i{Proof General} users manual. The proof-tree display
+needs of course the full output from the proof assistant.
+Therefore @code{proof-shell-should-be-silent} keeps the proof
+assistant noisy when the proof-tree display is switched on.
+
+
+@node Configuring Prooftree for a New Proof Assistant
+@section Configuring Prooftree for a New Proof Assistant
+
+To get the proof-tree display running for a new proof assistant
+one has to configure the proof-tree Elisp code and adapt the
+Prooftree program.
+
+@menu
+* Proof Tree Elisp configuration::
+* Prooftree Adaption::
+@end menu
+
+@node Proof Tree Elisp configuration
+@subsection Proof Tree Elisp configuration
+
+All variables that need to be configured are in the customization
+group @code{proof-tree-internals}. Most of these variables are
+regular expressions for extracting various parts from the proof
+assistant output. However, some are functions that need to be
+implemented as prover specific part of the proof display code.
+
+The variables @code{proof-tree-configured},
+@code{proof-tree-get-proof-info} and
+@code{proof-tree-find-begin-of-unfinished-proof} might be used
+before the proof assistant is running inside a proof shell. They
+must therefore be configured as part of the proof assistant
+editing mode. 
+
+The other variables are only used when the proof shell is
+running. They can therefore be configured with the
+proof-assistent proof-shell mode.
+
+
+@node Prooftree Adaption
+@subsection Prooftree Adaption
+
+To make the new proof assistant known to Prooftree, the match in
+function @code{configure_prooftree} in @code{input.ml} must be
+extended. If the new proof assistant does not support existential
+variables adding a line
+@example
+  | "new-pa-name" -> ()
+@end example
+suffices.
+
+If the new prover supports existential variables, Prooftree must
+be extended with a parser for the existential variable
+information printout of the proof assistant. The parser for Coq
+is contained in the file @code{coq.ml}. Then the function
+@code{configure_prooftree} must assign this new parser to the
+reference @code{parse_existential_info}.
+
+
 @node Writing More Lisp Code
 @chapter Writing More Lisp Code
 
@@ -3354,20 +3757,22 @@ is a space.
 processed by the prover. For normal scripting items it is
 @samp{@code{proof-done-advancing}}, for retract items
 @samp{@code{proof-done-retracting}}, but there are more possibilities (e.g.
-@samp{@code{proof-done-invisible}}, @samp{@code{proof-shell-set-silent}} and
-@samp{@code{proof-shell-clear-silent}}).
+@samp{@code{proof-done-invisible}}, @samp{@code{proof-shell-set-silent}},
+@samp{@code{proof-shell-clear-silent}} and @samp{@code{proof-tree-show-goal-callback}}).
 
 The @var{displayflags} are set
 for non-scripting commands or for when scripting should not
 bother the user.  They may include
 @lisp
-  @code{'invisible}             non-script command (@samp{@code{proof-shell-invisible-command}})
-  @code{'no-response-display}   do not display messages in @strong{response} buffer
-  @code{'no-error-display}      do not display errors/take error action
-  @code{'no-goals-display}      do not goals in @strong{goals} buffer
+  @code{'invisible}                non-script command (@samp{@code{proof-shell-invisible-command}})
+  @code{'no-response-display}      do not display messages in @strong{response} buffer
+  @code{'no-error-display}         do not display errors/take error action
+  @code{'no-goals-display}         do not goals in @strong{goals} buffer
+  @code{'proof-tree-show-subgoal}  item inserted by the proof-tree package
 @end lisp
-If flags are non-empty, interactive cues will be surpressed.
-(E.g., printing hints).
+Note that @code{'invisible} does not imply any of the others. If flags
+are non-empty, interactive cues will be surpressed. (E.g.,
+printing hints).
 
 See the functions @samp{@code{proof-start-queue}} and @samp{@code{proof-shell-exec-loop}}.
 @end defvar
@@ -3500,7 +3905,8 @@ If a there is a next command after that, send it to the process.
 If the action list becomes empty, unlock the process and remove
 the queue region.
 
-The return value is non-nil if the action list is now empty.
+The return value is non-nil if the action list is now empty or
+contains only invisible elements for Prooftree synchronization.
 @end defun
 
 Input is actually inserted into the shell buffer and sent to the process
@@ -3510,10 +3916,13 @@ by the low-level function @code{proof-shell-insert}.
 @defun proof-shell-insert strings action &optional scriptspan
 Insert @var{strings} at the end of the proof shell, call @samp{@code{scomint-send-input}}.
 
+@var{strings} is a list of strings (which will be concatenated), or a
+single string.
+
 The @var{action} argument is a symbol which is typically the name of a
-callback for when @var{string} has been processed.
+callback for when each string has been processed.
 
-First we call @samp{@code{proof-shell-insert-hook}}.  The arguments @samp{action} and
+This calls @samp{@code{proof-shell-insert-hook}}.  The arguments @samp{action} and
 @samp{scriptspan} may be examined by the hook to determine how to modify
 the @samp{string} variable (exploiting dynamic scoping) which will be
 the command actually sent to the shell.
@@ -3521,7 +3930,7 @@ the command actually sent to the shell.
 Note that the hook is not called for the empty (null) string
 or a carriage return.
 
-Then we strip @var{string} of carriage returns before inserting it
+We strip the string of carriage returns before inserting it
 and updating @samp{@code{proof-marker}} to point to the end of the newly
 inserted text.
 
@@ -3736,8 +4145,9 @@ Marker in proof shell buffer pointing to end of last urgent message.
 @defun proof-shell-process-urgent-message start end
 Analyse urgent message between @var{start} and @var{end} for various cases.
 
-Cases are: included file, retracted file, cleared response buffer,
-variable setting, @var{pgip} response, or theorem dependency list.
+Cases are: @strong{trace} output, included/retracted files, cleared 
+goals/response buffer, variable setting, xml-encoded @var{pgip} response, 
+theorem dependency message or interactive output indicator.
 
 If none of these apply, display the text between @var{start} and @var{end}.
 
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 6f04c513..daa90e5d 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -161,6 +161,7 @@ provided for several other provers.
 * Unicode symbols and special layout support::
 * Support for other Packages::  
 * Subterm Activation and Proof by Pointing::
+* Graphical Proof-Tree Visualization::
 * Customizing Proof General::   
 * Hints and Tips::
 * LEGO Proof General::          
@@ -514,7 +515,8 @@ Proof General is designed to be useful for novices and expert users
 alike.  It will be useful to you if you use a proof assistant, and you'd
 like an interface with the following features: simplified interaction,
 script management, multiple file scripting, a script editing mode, proof
-by pointing, toolbar and menus, syntax highlighting, real symbols,
+by pointing, proof-tree visualization,
+toolbar and menus, syntax highlighting, real symbols,
 functions menu, tags, and finally, adaptability.
 
 Here is an outline of some of these features.   Look in the contents
@@ -554,6 +556,7 @@ regions.
 For more details, @pxref{Basic Script Management},
 @ref{Script processing commands},
 and @ref{Advanced Script Management and Editing}.
+
 @item @i{Script editing mode}@*
 Proof General provides useful facilities for editing proof scripts,
 including syntax hilighting and a menu to jump to particular goals,
@@ -563,6 +566,21 @@ assistant, or undo previous proof steps.
 
 For more details, @pxref{Script editing commands},
 and @ref{Script processing commands}.
+
+@item @i{Proof-tree visualization}@*
+In cooperation with the external program Prooftree
+(available from the @uref{http://askra.de/software/prooftree/,
+Prooftree website}), Proof General can display proof trees
+graphically and provide visual information about the proof status
+of different branches in a proof. The proof-tree display provides
+additional means for inspecting the proof tree and thus helps
+against loosing track in proofs.
+
+The graphical proof-tree visualization is currently only
+supported for Coq. For more details, @pxref{Graphical Proof-Tree
+Visualization}. 
+
+
 @item @i{Toolbar and menus}@*
 A script buffer has a toolbar with navigation buttons for processing
 parts of the proof script.  A menu provides further functions for
@@ -3035,6 +3053,113 @@ Query the prover about the identifier near mouse click @var{event}.
 @c
 @c CHAPTER
 @c
+@node Graphical Proof-Tree Visualization
+@chapter Graphical Proof-Tree Visualization
+@cindex proof-tree visualization
+
+Since version 4.2, Proof General supports proof-tree
+visualization on graphical desktops via the additional program
+Prooftree. Currently, proof-tree visualization is only supported
+for the Coq proof assistant. For installation instructions and
+more detailed information about Prooftree, please refer to the
+@uref{http://askra.de/software/prooftree/, Prooftree website} and
+the @uref{http://askra.de/software/prooftree/prooftree.man.html,
+Prooftree man page}. For information about how to support
+proof-tree visualization for a different proof assistant, see
+Section @i{Configuring Proof-Tree Visualization} in the
+@i{Adapting Proof General} manual.
+
+@menu
+* Starting and Stopping Proof-Tree Visualization::
+* Features of Prooftree::
+* Prooftree Customization::
+@end menu
+
+
+@node Starting and Stopping Proof-Tree Visualization
+@section Starting and Stopping Proof-Tree Visualization
+
+When proof-tree visualization is supported (currently only for
+the Coq proof assistant), you can start the visualization via the
+proof-tree button in the tool-bar, via the menu 
+@lisp
+   Proof-General -> Start/Stop Prooftree
+@end lisp
+or via the keyboard shortcut @kbd{C-c C-d}, all of which invoke
+@code{proof-tree-external-display-toggle}.
+
+If you are inside a proof, the graphical display is started
+immediately for your current proof. Otherwise the display starts
+as soon as you start the next proof. Starting the proof-tree
+display in the middle of a proof involves an automatic
+reexecution of your current proof script in the locked region,
+which should be almost unnoticeable, except for the time it
+takes.
+
+The proof-tree display stops at the end of the proof or when you
+invoke @code{proof-tree-external-display-toggle} by one of the
+three indicated means again. Alternatively you can also close the
+proof-tree window. 
+
+Proof General launches only one instance of Prooftree,
+which can manage an arbitrary amount of proof-tree windows. 
+
+@node Features of Prooftree
+@section Features of Prooftree
+
+The proof-tree window provides visual information about the
+status of the different branches in your proof (by coloring
+completely proved branches in green, for example) and means for
+inspecting previous proof states without the need to retract
+parts of your proof script. Currently, Prooftree provides
+the following features:
+
+@itemize @bullet
+@item Navigation in the proof tree and display of all previous
+proof states and proof commands.
+@item Display branches of the proof in different colors according to
+their proof state, distinguishing branches with open, partially
+or fully instantiated existential variables as well as branches
+that have been finished by a cheating command such as
+@code{admit}.
+@item Display the status of existential variables and their
+dependencies.
+@item Mark proof commands that introduce or instantiate a
+given existential variable.
+@item Snapshots of proof trees for reference when you retract
+your proof to try an different approach.
+@end itemize
+
+For a more elaborated description please consult the help dialog
+of Prooftree or the
+@uref{http://askra.de/software/prooftree/prooftree.man.html,
+Prooftree man page}.
+
+
+@node Prooftree Customization
+@section Prooftree Customization
+
+The location of the Prooftree program and command line
+arguments can be configured in the customization group
+@code{proof-tree}. You can visit this customization group inside
+a running instance of Proof General by typing @code{M-x
+customize-group <RET> proof-tree <RET>}.
+
+The graphical aspects of the proof-tree rendering, fonts and
+colors can be changed inside Prooftree by invoking the
+@code{Configuration} item of the main menu.
+
+Prover specific parts such as the regular expressions for
+recognizing subgoals, existential variables and navigation and
+cheating commands are in the customization group
+@code{proof-tree-internals}. Under normal circumstances there
+should be no need to change one of these internal settings. 
+
+
+@c =================================================================
+@c
+@c CHAPTER
+@c
 @node Customizing Proof General
 @chapter Customizing Proof General
 @cindex Customization
@@ -4033,6 +4158,7 @@ assistant.  It supports most of the generic features of Proof General.
 * Editing multiple proofs::
 * User-loaded tactics::
 * Holes feature::
+* Proof-Tree Visualization::
 @end menu
 
 
@@ -4608,6 +4734,14 @@ select the file named @code{coq-abbrev.el} in the
 you want to save abbrevs; answer yes.
 
 
+@node Proof-Tree Visualization
+@section Proof-Tree Visualization
+
+Starting with Proof General version 4.2 and Coq version 8.4, Coq
+Proof General has full support for proof-tree visualization, 
+@pxref{Graphical Proof-Tree Visualization}.
+
+
 @c =================================================================
 @c
 @c  CHAPTER: Isabelle Proof General
diff --git a/generic/pg-custom.el b/generic/pg-custom.el
index 8f20bf69..efbc8a76 100644
--- a/generic/pg-custom.el
+++ b/generic/pg-custom.el
@@ -56,6 +56,7 @@
   (find      "Find Theorems"	  "Find theorems" t proof-find-theorems-command)
   (info      "Identifier Info"    "Information about identifier" t proof-query-identifier-command)
   (command   "Issue Command"	  "Issue a non-scripting command" t t)
+  (prooftree "Start/Stop Prooftree" "Start/Stop external proof-tree display" t proof-tree-configured)
   (interrupt "Interrupt Prover"   "Interrupt the proof assistant" t t)
   (restart   "Restart Scripting"  "Restart scripting (clear all locked regions)" t t)
   (visibility "Toggle Visibility" "Show or hide hidden proofs" nil t)
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 40c463a0..49f3a1c6 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -213,6 +213,12 @@ conversion, etc.  (No changes are done if nil)."
   :type '(choice string (const nil))
   :group 'prover-config)
 
+(defcustom proof-tree-configured nil
+  "Whether external proof-tree display is configured.
+This boolean enables the proof-tree menu entry and the function
+that starts external proof-tree display."
+  :type 'boolean
+  :group 'proof-tree-internals)
 
 
 ;;
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index b4ac2bf9..472f2f9e 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -104,6 +104,7 @@ without adjusting window layout."
   (define-key map [(control meta e)] 'proof-goto-command-end)
   (define-key map [(control c) (control b)] 'proof-process-buffer)
   ;; C-c C-c is proof-interrupt-process in universal-keys
+  (define-key map [(control c) (control d)] 'proof-tree-external-display-toggle)
   ;; C-c C-f is proof-find-theorems in universal-keys
   (define-key map [(control c) (control H)] 'proof-help)
   ;; C-c C-l is proof-layout-windows in universal-keys
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index a2402013..ab0d2d05 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -15,7 +15,7 @@
 
 ;;; Code:
 
-(require 'cl)				; set-difference
+(require 'cl)				; set-difference, every
 
 (eval-when-compile
   (require 'span)
@@ -25,6 +25,7 @@
 (require 'pg-response)
 (require 'pg-goals)
 (require 'pg-user)			; proof-script, new-command-advance
+(require 'proof-tree)
 
 
 ;;
@@ -57,20 +58,22 @@ ACTION is the callback to be invoked when this item has been
 processed by the prover. For normal scripting items it is
 `proof-done-advancing', for retract items
 `proof-done-retracting', but there are more possibilities (e.g.
-`proof-done-invisible', `proof-shell-set-silent' and
-`proof-shell-clear-silent').
+`proof-done-invisible', `proof-shell-set-silent',
+`proof-shell-clear-silent' and `proof-tree-show-goal-callback').
 
 The DISPLAYFLAGS are set
 for non-scripting commands or for when scripting should not
 bother the user.  They may include
 
-  'invisible		 non-script command (`proof-shell-invisible-command')
-  'no-response-display   do not display messages in *response* buffer
-  'no-error-display      do not display errors/take error action
-  'no-goals-display      do not goals in *goals* buffer
+  'invisible		    non-script command (`proof-shell-invisible-command')
+  'no-response-display      do not display messages in *response* buffer
+  'no-error-display         do not display errors/take error action
+  'no-goals-display         do not goals in *goals* buffer
+  'proof-tree-show-subgoal  item inserted by the proof-tree package
 
-If flags are non-empty, interactive cues will be surpressed.
-\(E.g., printing hints).
+Note that 'invisible does not imply any of the others. If flags
+are non-empty, interactive cues will be surpressed. (E.g.,
+printing hints).
 
 See the functions `proof-start-queue' and `proof-shell-exec-loop'.")
 
@@ -885,6 +888,7 @@ track what happens in the proof queue."
   "Non-nil if we should switch to silent mode based on size of queue."
   (if (and proof-shell-start-silent-cmd ; configured
 	   (not proof-full-annotation)  ; always noisy
+	   (not proof-tree-external-display) ; no proof-tree display 
 	   (not proof-shell-silent))	; already silent
 	  ;; NB: to be more accurate we should only count number
 	  ;; of scripting items in the list (not e.g. invisibles).
@@ -1006,14 +1010,15 @@ If a there is a next command after that, send it to the process.
 If the action list becomes empty, unlock the process and remove
 the queue region.
 
-The return value is non-nil if the action list is now empty."
+The return value is non-nil if the action list is now empty or
+contains only invisible elements for Prooftree synchronization."
   (unless (null proof-action-list)
     (save-excursion
       (if proof-script-buffer		      ; switch to active script
 	  (set-buffer proof-script-buffer))
 
       (let* ((item    (car proof-action-list))
-	     (flags   (nth 3 (car proof-action-list)))
+	     (flags   (nth 3 item))
 	     cbitems)
 
 	;; now we should invoke callback on just processed command,
@@ -1025,6 +1030,16 @@ The return value is non-nil if the action list is now empty."
 	(setq cbitems (cons item
 			    (proof-shell-slurp-comments)))
 
+	;; This is the point where old items have been removed from
+	;; proof-action-list and where the next item has not yet been
+	;; sent to the proof assistent. This is therefore one of the
+	;; few points where it is safe to manipulate
+	;; proof-action-list. The urgent proof-tree display actions
+	;; must therefore be called here, because they might add some
+	;; Show actions at the front of proof-action-list.
+	(if proof-tree-external-display
+	    (proof-tree-urgent-action flags))
+
 	;; if action list is (nearly) empty, ensure prover is noisy.
 	(if (and proof-shell-silent
 		 (not (eq (nth 2 item) 'proof-shell-clear-silent))
@@ -1055,7 +1070,10 @@ The return value is non-nil if the action list is now empty."
 	    (pg-processing-complete-hint))
 	  (pg-finish-tracing-display))
 
-	(null proof-action-list)))))
+	(or (null proof-action-list)
+	    (every
+	     (lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item)))
+	     proof-action-list))))))
 
 
 (defun proof-shell-insert-loopback-cmd  (cmd)
@@ -1423,7 +1441,8 @@ output that slows down processing.
 
 After processing the current output, the last step undertaken
 by the filter is to send the next command from the queue."
-  (let ((cmd   (nth 1 (car proof-action-list)))
+  (let ((span  (caar proof-action-list))
+	(cmd   (nth 1 (car proof-action-list)))
 	(flags (nth 3 (car proof-action-list))))
 
     ;; A copy of the last message, verbatim, never modified.
@@ -1440,7 +1459,10 @@ by the filter is to send the next command from the queue."
       (if (proof-shell-exec-loop)
 	  (setq proof-shell-last-output-kind
 		;; only display result for last output
-		(proof-shell-handle-delayed-output))))))
+		(proof-shell-handle-delayed-output)))
+      ;; send output to the proof tree visualizer
+      (if proof-tree-external-display
+	  (proof-tree-handle-delayed-output cmd flags span)))))
 
 
 (defsubst proof-shell-display-output-as-response (flags str)
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index 7bf5dd26..2b23053c 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -198,6 +198,10 @@ back the default toolbar."
 (defalias 'proof-toolbar-use 'proof-process-buffer)
 (defalias 'proof-toolbar-use-enable-p 'proof-toolbar-next-enable-p)
 
+;; Prooftree
+
+(defalias 'proof-toolbar-prooftree 'proof-tree-external-display-toggle)
+
 ;; Restart
 
 (defalias 'proof-toolbar-restart 'proof-shell-restart)
diff --git a/generic/proof-tree.el b/generic/proof-tree.el
new file mode 100644
index 00000000..d877b332
--- /dev/null
+++ b/generic/proof-tree.el
@@ -0,0 +1,1118 @@
+;;; tree-tree.el --- Proof General prooftree communication.
+;;
+;; Copyright (C) 2012 Hendrik Tews
+;; Authors:   Hendrik Tews
+;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
+;;
+;; $Id$
+;;
+;;; Commentary:
+;;
+;; Generic code for the communication with prooftree. Prooftree
+;; is an ocaml-gtk program that displays proof trees.
+;;
+;; The main problem with proof tree visualization is that Coq (and
+;; probably other proof assistants as well) does not provide any
+;; information about which subgoals are new and have been created by
+;; the last proof command and which subgoals stem from older proof
+;; commands.
+;;
+;; To solve this problem prooftree relies on unique identification
+;; strings of goals, which are called goal or sequent ID's in the
+;; code. With these ID's it is easy to keep track which goals are new.
+;;
+;; A second problem is that, for an undo command, Coq (and probably
+;; other proof assistants as well) does not tell which subgoals and
+;; which finished branches must be deleted. Therefore prooftree needs
+;; a continuously increasing proof state number and keeps a complete
+;; undo history for every proof.
+;;
+;; A third problem is that Coq (and probably other proof assistants as
+;; well) is not able to generate the information for a proof tree in
+;; the middle of a proof. Therefore, if the user wants to start the
+;; proof-tree display in the middle of the proof, it is necessary to
+;; retract to the start of the proof and then to reassert to the
+;; previous end of the locked region. To achieve this one has to call
+;; `accept-process-output' at suitable points to let Proof General
+;; process the `proof-action-list'.
+;; 
+;; A fourth problem is that proof-tree display can only work when the
+;; prover output is not suppressed (via `proof-full-annotation').
+;; `proof-shell-should-be-silent' takes care of that.
+;; 
+;; The design of Prooftree, of the glue code inside Proof General
+;; (mostly in this file) and of the communication protocol tries to
+;; achieve the following two goals:
+;;
+;;   * Functionality is preferably transferred into prooftree, to
+;;     enlarge Proof General not unnecessarily.
+;;
+;;   * To avoid synchronization trouble the communication between
+;;     Proof General and prooftree is almost one way only: Only Proof
+;;     General sends display or undo commands to Prooftree. Prooftree
+;;     never requests any proof-state information from Proof General.
+;;     Prooftree only sends a quit message to Proof General when the
+;;     user closes the proof-tree display of the current proof. This
+;;     goal requires that some of the heuristics, which decide which
+;;     subgoals are new and which have to be refreshed, have to be
+;;     implemented here.
+;;
+;; In general the glue code here works on the delayed output. That is,
+;; the glue code here runs when the next proof command has already
+;; been sent to the proof assistant. The glue code makes a light
+;; analysis on the output of the proof assistant, extracts the
+;; necessary parts with regular expressions and sends appropriate
+;; commands to prooftree. This is achieved by calling the main entry
+;; here, the function `proof-tree-handle-delayed-output' from the
+;; proof shell filter function after `proof-shell-exec-loop' has
+;; finished.
+;;
+;; However, some aspects can not be delayed. Those are treated by
+;; `proof-tree-urgent-action'. Its primary use is for inserting
+;; special goal-displaying commands into `proof-action-list' before
+;; the next real proof command runs. For Coq this needs to be done for
+;; newly generated subgoals and for goals that contain an existential
+;; variable that got instantiated in the last proof step.
+
+
+;;; Code:
+
+(require 'cl)
+
+(eval-when (compile)
+  (require 'proof-shell))
+
+
+;;
+;; User options
+;;
+
+(defgroup proof-tree ()
+  "Customization for the proof tree visualizer"
+  :group 'proof-general
+  :package-version '(ProofGeneral . "4.2"))
+
+(defcustom proof-tree-program (proof-locate-executable "prooftree" t nil)
+  "Command to invoke prooftree."
+  :type 'string
+  :group 'proof-tree)
+
+(defcustom proof-tree-arguments ()
+  "Command line arguments for prooftree."
+  :type '(repeat string)
+  :group 'proof-tree)
+
+
+;;
+;; Proof assistant options
+;;
+
+(defgroup proof-tree-internals ()
+  "Proof assistant specific customization of prooftree."
+  :group 'proof-general-internals
+  :package-version '(ProofGeneral . "4.2"))
+
+;; defcustom proof-tree-configured is in proof-config.el, because it is
+;; needed in pg-custom.el
+
+(defcustom proof-tree-ignored-commands-regexp nil
+  "Commands that should be ignored for the prooftree display.
+The output of commands matching this regular expression is not
+send to prooftree. It should match commands that display
+additional information but do not make any proof progress. Leave
+at nil to act on all commands."
+  :type '(choice regexp (const nil))
+  :group 'proof-tree-internals)
+
+(defcustom proof-tree-navigation-command-regexp nil
+  "Regexp to match a navigation command.
+A navigation command typically focusses on a different open goal
+without changing any of the open goals. Leave at nil if there are
+no navigation commands."
+  :type '(choice regexp (const nil))
+  :group 'proof-tree-internals)
+
+(defcustom proof-tree-cheating-regexp nil
+  "Regexp to match cheating proofer commands.
+A cheating command finishes the current goal without proving it
+to permit the user to first focus on other parts of the
+development. Examples are \"sorry\" in Isabelle and \"admit\" in
+Coq. Leave at nil if there are no cheating commands."
+  :type '(choice regexp (const nil))
+  :group 'proof-tree-internals)
+
+(defcustom proof-tree-current-goal-regexp nil
+  "Regexp to match the current goal and its ID.
+The regexp is matched against the output of the proof assistant
+to extract the current goal with its ID. The regexp must have 2
+grouping constructs, the first one matches just the ID, the
+second one the complete sequent text that is to be sent to
+prooftree."
+  :type 'regexp
+  :group 'proof-tree-internals)
+
+(defcustom proof-tree-update-goal-regexp nil
+  "Regexp to match a goal and its ID.
+The regexp is matched against the output of additional show-goal
+commands inserted by Proof General with a command returned by
+`proof-tree-show-sequent-command'. Proof General inserts such
+commands to update the goal text in prooftree. This is necessary,
+for instance, when existential variables get instantiated. This
+regexp must have 2 grouping constructs, the first matching the ID
+of the goal, the second the complete sequent text."
+  :type 'regexp
+  :group 'proof-tree-internals)
+
+(defcustom proof-tree-additional-subgoal-ID-regexp nil
+  "Regular expression to match ID's of additional subgoals.
+This regexp is used to extract the ID's of all additionally open
+goals. The regexp is used in a while loop and must match one
+subgoal ID with subgroup 1."
+  :type 'regexp
+  :group 'proof-tree-internals)
+
+(defcustom proof-tree-existential-regexp nil
+  "Regexp to match existential variables.
+Existential variables exist for instance in Isabelle/Hol and in
+Coq. They are placeholders for terms that might (for Coq they
+must) get instantiated in a later stage of the proof. This regexp
+should match one existential variable in subgroup 1. It is used
+inside a while loop to extract all existential variables from the
+goal text or from a list of existential variables.
+
+Leave this variable at nil for proof assistants that do not have
+existential variables."
+  :type '(choice regexp (const nil))
+  :group 'proof-tree-internals)
+
+(defcustom proof-tree-existentials-state-start-regexp nil
+  "Regexp to match the start of the state display of existential variables.
+Together with `proof-tree-existentials-state-end-regexp', this
+regular expression is used to determine the state display of
+existential variables, which contains information about which
+existentials are still uninstantiated and about dependencies of
+instantiated existential variables. Leave this variable nil, if
+there is no such state display."
+  :type '(choice regexp (const nil))
+  :group 'proof-tree-internals)
+
+(defcustom proof-tree-existentials-state-end-regexp nil
+  "Regexp to match the end of the state display of existential variables.
+Together with `proof-tree-existentials-state-start-regexp', this
+regular expression is used to determine the state display of
+existential variables, which contains information about which
+existentials are still uninstantiated and about dependencies of
+instantiated existential variables. If this variable is nil (and
+if `proof-tree-existentials-state-start-regexp' is non-nil), then
+the state display expands to the end of the prover output."
+  :type '(choice regexp (const nil))
+  :group 'proof-tree-internals)
+
+(defcustom proof-tree-proof-completed-regexp nil
+  "Regexp to match the proof-is-complete message."
+  :type 'regexp
+  :group 'proof-tree-internals)
+
+(defcustom proof-tree-get-proof-info nil
+  "Proof assistant specific function for information about the current proof.
+This function takes no arguments. It must return a list, which
+contains, in the following order:
+
+* the current state number (as positive integer)
+* the name of the current proof (as string) or nil
+
+The state number is used to implement undo in prooftree. The
+proof name is used to distinguish different proofs inside
+prooftree.
+
+The state number is interpreted as the state that has been
+reached after the last command has been processed. It must be
+consistent in the following sense. Firstly, it must be strictly
+increasing for successive commands that can be individually
+retracted. Secondly, the state number reported after some command
+X has been processed must be strictly greater than the state
+reported when X is retracted. Finally, state numbers of commands
+preceding X must be less than or equal the state reported when X
+is retracted (but no stuff before X)."
+  :type 'function
+  :group 'proof-tree-internals)
+
+(defcustom proof-tree-extract-instantiated-existentials nil
+  "Proof assistant specific function for instantiated existential variables.
+This function must only be defined if the prover has existential
+variables, that is, if `proof-tree-existential-regexp' is
+non-nil.
+
+If defined, this function should return the list of currently
+instantiated existential variables as a list of strings. The
+function is called with `proof-shell-buffer' as current
+buffer and with two arguments start and stop, which designate the
+region containing the last output from the proof assistant.
+
+`proof-tree-extract-list' might be useful for writing this
+function."
+  :type '(choice function (const nil))
+  :group 'proof-tree-internals)
+
+(defcustom proof-tree-show-sequent-command nil
+  "Proof assistant specific function for a show-goal command.
+This function is applied to an ID of a goal and should return a
+command (as string) that will display the complete sequent with
+that ID. The regexp `proof-tree-update-goal-regexp' should match
+the output of the proof assistant for the returned command, such
+that `proof-tree-update-sequent' will update the sequent ID
+inside prooftree.
+
+If the proof assistant is unable to redisplay sequent ID the
+function should return nil and prooftree will not get updated."
+  :type 'function
+  :group 'proof-tree-internals)
+
+(defcustom proof-tree-find-begin-of-unfinished-proof nil
+  "Proof assistant specific function for the start of the current proof.
+This function is called with no argument when the user switches
+the external proof-tree display on. Then, this function must
+determin if there is a currently unfinished proof for which the
+proof-tree display should be started. If yes this function must
+return the starting position of the command that started this
+proof. If there is no such proof, this function must return nil."
+  :type 'function
+  :group 'proof-tree-internals)
+
+(defcustom proof-tree-urgent-action-hook ()
+  "Normal hook for prooftree actions that cannot be delayed.
+This hook is called (indirectly) from inside
+`proof-shell-exec-loop' after the preceeding command and any
+comments that follow have been choped off `proof-action-list' and
+before the next command is sent to the proof assistant. This hook
+can therefore be used to insert additional commands into
+`proof-action-list' that must be executed before the next real
+proof command.
+
+Functions in this hook can rely on `proof-info' being bound to
+the result of `proof-tree-get-proof-info'.
+
+This hook is used, for instance, for Coq to insert Show commands
+for newly generated subgoals. (The normal Coq output does not
+contain the complete sequent text of newly generated subgoals.)"
+  :type 'hook
+  :group 'proof-tree-internals)
+
+
+;;
+;; Internal variables
+;;
+
+(defvar proof-tree-external-display nil
+  "Display proof trees in external prooftree windows if t.
+Actually, if this variable is t then the user requested an
+external proof-tree display. If there was no unfinished proof
+when proof-tree display was requested and if no proof has been
+started since then, then there is obviously no proof-tree
+display. In this case, this variable stays t and the proof-tree
+display will be started for the next proof.
+
+Controlled by `proof-tree-external-display-toggle'.")
+
+(defvar proof-tree-process nil
+  "Emacs lisp process object of the prooftree process.")
+
+(defconst proof-tree-process-name "proof-tree"
+  "Name of the prooftree process for Emacs lisp.")
+
+(defconst proof-tree-process-buffer
+  (concat "*" proof-tree-process-name "*")
+  "Buffer for stdout and stderr of the prooftree process.")
+
+(defconst proof-tree-emacs-exec-regexp
+  "\nemacs exec: \\([-a-z]+\\) *\\([^\n]*\\)\n"
+  "Regular expression to match callback commands from the prooftree process.")
+
+(defvar proof-tree-last-state 0
+  "Last state of the proof assistant.
+Used for undoing in prooftree.")
+
+(defvar proof-tree-current-proof nil
+  "Name of the current proof or nil if there is none.
+This variable is only maintained and meaningful if
+`proof-tree-external-display' is t.")
+
+(defvar proof-tree-sequent-hash nil
+  "Hash table to remember sequent ID's.
+Needed because some proof assistants do not distinguish between
+new subgoals, which have been created by the last proof command,
+and older, currently unfocussed subgoals. If Proof General meets
+a goal, it is treated as new subgoal if it is not in this hash yet.
+
+The hash is mostly used as a set of sequent ID's. However, for
+undo operations it is necessary to delete all those sequents from
+the hash that have been created in a state later than the undo
+state. For this purpose this hash maps sequent ID's to the state
+number in which the sequent has been created.
+
+The hash table is initialized in `proof-tree-start-process'.")
+
+(defvar proof-tree-existentials-alist nil
+  "Alist mapping existential variables to sequent ID's.
+Used to remember which goals need a refresh when an existential
+variable gets instantiated. To support undo commands the old
+contents of this list must be stored in
+`proof-tree-existentials-alist-history'. To ensure undo is
+properly working, this variable should only be changed by using
+`proof-tree-delete-existential-assoc',
+`proof-tree-add-existential-assoc' or
+`proof-tree-reset-existentials'.")
+
+(defvar proof-tree-existentials-alist-history nil
+  "Alist mapping state numbers to old values of `proof-tree-existentials-alist'.
+Needed for undo.")
+  
+
+;;
+;; process filter function that receives prooftree output
+;;
+
+(defun proof-tree-stop-external-display ()
+  "Prooftree callback for the command \"stop-displaying\"."
+  (if proof-tree-current-proof
+      (message "External proof-tree display switched off"))
+  (proof-tree-quit-proof)
+  (setq proof-tree-external-display nil))
+
+
+(defun proof-tree-insert-output (string)
+  "Insert output or a message into the prooftree process buffer."
+  (with-current-buffer (get-buffer-create proof-tree-process-buffer)
+    (let ((moving (= (point) (point-max))))
+      (save-excursion
+	;; Insert the text, advancing the process marker.
+	(goto-char (point-max))
+	(insert string))
+      (if moving (goto-char (point-max))))))
+
+
+(defun proof-tree-process-filter (proc string)
+  "Output filter for prooftree.
+Records the output in the prooftree process buffer and checks for
+callback function requests."
+  (proof-tree-insert-output string)
+  (save-excursion
+    (let ((start 0))
+      (while (proof-string-match proof-tree-emacs-exec-regexp string start)
+	(let ((end (match-end 0))
+	      (cmd (match-string 1 string))
+	      (data (match-string 2 string)))
+	  (cond
+	   ((equal cmd "stop-displaying")
+	    (proof-tree-stop-external-display))
+	   (t
+	    (display-warning
+	     '(proof-general proof-tree)
+	     (format "Unknown prooftree command %s" cmd)
+	     :warning)))
+	  (setq start end))))))
+
+
+;;
+;; Process creation
+;;
+
+(defun proof-tree-process-sentinel (proc event)
+  "Sentinel for prooftee.
+Runs on process status changes and cleans up when prooftree dies."
+  (proof-tree-insert-output (concat "\nsubprocess status change: " event))
+  (unless (proof-tree-is-running)
+    (proof-tree-stop-external-display)
+    (setq proof-tree-process nil)))
+
+(defun proof-tree-start-process ()
+  "Start the external prooftree process.
+Does also initialize the communication channel and some internal
+variables."
+  (let ((old-proof-tree (get-process proof-tree-process-name)))
+    ;; first clean up any old processes
+    (when old-proof-tree
+      (delete-process old-proof-tree)
+      (proof-tree-insert-output "\n\nProcess terminated by Proof General\n\n"))
+    ;; now start the new process
+    (proof-tree-insert-output "\nStart new prooftree process\n\n")
+    (setq proof-tree-process
+	  (apply 'start-process
+	   proof-tree-process-name
+	   proof-tree-process-buffer
+	   proof-tree-program
+	   proof-tree-arguments))
+    (set-process-coding-system proof-tree-process 'utf-8-unix 'utf-8-unix)
+    (set-process-filter proof-tree-process 'proof-tree-process-filter)
+    (set-process-sentinel proof-tree-process 'proof-tree-process-sentinel)
+    (set-process-query-on-exit-flag proof-tree-process nil)
+    ;; other initializations
+    (setq proof-tree-sequent-hash (make-hash-table :test 'equal)
+	  proof-tree-last-state 0
+	  proof-tree-existentials-alist nil
+	  proof-tree-existentials-alist-history nil)
+    (proof-tree-send-configure)))
+
+
+(defun proof-tree-is-running ()
+  "Return t if prooftree is properly running."
+  (and proof-tree-process
+       (eq (process-status proof-tree-process) 'run)))
+
+(defun proof-tree-ensure-running ()
+  "Ensure the prooftree process is running properly."
+  (unless (proof-tree-is-running)
+    (proof-tree-start-process)))
+
+
+;;
+;; Low-level communication primitives
+;;
+
+(defconst proof-tree-protocol-version 1
+  "Version of the communication protocol between Proof General and Prooftree.
+Must be increased if one of the low-level communication
+primitives is changed.")
+
+(defun proof-tree-send-message (second-line data)
+  "Send a complete message to Prooftree.
+Send a message with command line SECOND-LINE and all strings in
+DATA as data sections to Prooftree."
+  (let ((second-line-len (string-bytes second-line)))
+    (assert (< second-line-len 999))
+    (process-send-string
+     proof-tree-process
+     (format "second line %03d\n%s\n%s%s"
+	     (1+ second-line-len)
+	     second-line
+	     (mapconcat 'identity data "\n")
+	     (if data "\n" "")))))
+
+(defun proof-tree-send-configure ()
+  "Send the configure message."
+  (proof-tree-send-message
+   (format "configure for \"%s\" and protocol version %02d"
+	   proof-assistant
+	   proof-tree-protocol-version)
+   ()))
+
+(defun proof-tree-send-goal-state (state proof-name command-string cheated-flag
+				   current-sequent-id current-sequent-text
+				   additional-sequent-ids existential-info)
+  "Send the current goal state to prooftree."
+  ;; (message "PTSGS id %s sequent %s ex-info %s"
+  ;; 	   current-sequent-id current-sequent-text existential-info)
+  (let* ((add-id-string (mapconcat 'identity additional-sequent-ids " "))
+	 (second-line
+	  (format
+	   (concat "current-goals state %d current-sequent %s %s "
+		   "proof-name-bytes %d "
+		   "command-bytes %d sequent-text-bytes %d "
+		   "additional-id-bytes %d existential-bytes %d")
+	   state
+	   current-sequent-id
+	   (if cheated-flag "cheated" "not-cheated")
+	   (1+ (string-bytes proof-name))
+	   (1+ (string-bytes command-string))
+	   (1+ (string-bytes current-sequent-text))
+	   (1+ (string-bytes add-id-string))
+	   (1+ (string-bytes existential-info)))))
+    (proof-tree-send-message
+     second-line
+     (list proof-name command-string current-sequent-text
+	   add-id-string existential-info))))
+
+(defun proof-tree-send-update-sequent (state proof-name sequent-id sequent-text)
+  "Send the updated sequent text to prooftree."
+  (let ((second-line
+	 (format
+	  (concat "update-sequent state %d sequent %s proof-name-bytes %d "
+		  "sequent-text-bytes %d")
+	  state sequent-id
+	  (1+ (string-bytes proof-name))
+	  (1+ (string-bytes sequent-text)))))
+    (proof-tree-send-message
+     second-line
+     (list proof-name sequent-text))))
+
+(defun proof-tree-send-switch-goal (proof-state proof-name current-id)
+  "Send switch-to command to prooftree."
+  (let ((second-line
+	 (format "switch-goal state %d sequent %s proof-name-bytes %d"
+		 proof-state
+		 current-id
+		 (1+ (string-bytes proof-name)))))
+    (proof-tree-send-message second-line (list proof-name))))
+
+(defun proof-tree-send-proof-completed (state proof-name
+					      cmd-string cheated-flag)
+  "Send proof completed to prooftree."
+  (let ((second-line
+	 (format
+	  "proof-complete state %d %s proof-name-bytes %d command-bytes %d"
+	  state
+	  (if cheated-flag "cheated" "not-cheated")
+	  (1+ (string-bytes proof-name))
+	  (1+ (string-bytes cmd-string)))))
+    (proof-tree-send-message
+     second-line
+     (list proof-name cmd-string))))
+
+(defun proof-tree-send-undo (proof-state)
+  "Tell prooftree to undo."
+  (let ((second-line (format "undo-to state %d" proof-state)))
+    (proof-tree-send-message second-line nil)))
+
+(defun proof-tree-send-quit-proof (proof-name)
+  "Tell prooftree to close the window for PROOF-NAME."
+  (let ((second-line (format "quit-proof proof-name-bytes %d"
+			    (1+ (string-bytes proof-name)))))
+    (proof-tree-send-message second-line (list proof-name))))
+
+
+;;
+;; proof-tree-existentials-alist manipulations and history
+;;
+
+(defun proof-tree-record-existentials-state (state &optional dont-copy)
+  "Store the current state of `proof-tree-existentials-alist' for undo.
+Usually this involves making a copy of
+`proof-tree-existentials-alist' because of the destructive
+updates used on that list. If optional argument DONT-COPY is
+non-nil no copy is done."
+  (setq proof-tree-existentials-alist-history
+	(cons (cons state
+		    (if dont-copy
+			 proof-tree-existentials-alist
+		      (copy-alist proof-tree-existentials-alist)))
+	      proof-tree-existentials-alist-history)))
+
+(defun proof-tree-undo-state-var (proof-state var-symbol history-symbol)
+  "Undo changes to VAR-SYMBOL using HISTORY-SYMBOL.
+This is a general undo function for variables that keep their
+undo information in a alist that maps state numbers to old
+values. Argument PROOF-STATE is the state to reestablish,
+VAR-SYMBOL is (the symbol of) the variable to undo and
+HISTORY-SYMBOL is (the symbol of) the undo history alist."
+  (let ((undo-not-finished t)
+	(history (symbol-value history-symbol))
+	(var (symbol-value var-symbol)))
+    (while (and undo-not-finished history)
+      (if (> (caar history) proof-state)
+	  (progn
+	    (setq var (cdr (car history)))
+	    (setq history (cdr history)))
+	(setq undo-not-finished nil)))
+    (set var-symbol var)
+    (set history-symbol history)))
+
+(defun proof-tree-undo-existentials (proof-state)
+  "Undo changes in `proof-tree-existentials-alist'.
+Change `proof-tree-existentials-alist' back to its contents in
+state PROOF-STATE."
+  (proof-tree-undo-state-var proof-state
+			     'proof-tree-existentials-alist
+			     'proof-tree-existentials-alist-history))
+
+(defun proof-tree-delete-existential-assoc (state ex-assoc)
+  "Delete mapping EX-ASSOC from 'proof-tree-existentials-alist'."
+  (proof-tree-record-existentials-state state)
+  (setq proof-tree-existentials-alist
+	(delq ex-assoc proof-tree-existentials-alist)))
+  
+(defun proof-tree-add-existential-assoc (state ex-var sequent-id)
+  "Add the mapping EX-VAR -> SEQUENT-ID to 'proof-tree-existentials-alist'.
+Do nothing if this mapping does already exist."
+  (let ((ex-var-assoc (assoc ex-var proof-tree-existentials-alist)))
+    (if ex-var-assoc
+	(unless (member sequent-id (cdr ex-var-assoc))
+	  (proof-tree-record-existentials-state state)
+	  (setcdr ex-var-assoc (cons sequent-id (cdr ex-var-assoc))))
+      (proof-tree-record-existentials-state state)
+      (setq proof-tree-existentials-alist
+	    (cons (cons ex-var (list sequent-id))
+		  proof-tree-existentials-alist)))))
+
+(defun proof-tree-reset-existentials (proof-state)
+  "Clear the mapping in `proof-tree-existentials-alist'."
+  (proof-tree-record-existentials-state proof-state 'dont-copy)
+  (setq proof-tree-existentials-alist nil))
+
+
+;;
+;; Process urgent output from the proof assistant
+;;
+
+(defun proof-tree-show-goal-callback (state)
+  "Callback for display-goal commands inserted by this package.
+Update the sequent and run hooks in `proof-state-change-hook'.
+Argument STATE is the state number (i.e., an integer) with which
+the update sequent command should be associated.
+
+The STATE is necessary, because a comment following a branching
+command cat get retired together with the branching command
+before the show-goal commands that update sequents are processed.
+The effect of the sequent update would therefore be undone when
+the comment alone is retracted.
+
+You CANNOT put this function directly as callback into
+`proof-action-list' because callbacks receive the span as
+argument and this function expects an integer! Rather you should
+call `proof-tree-make-show-goal-callback', which evaluates to a
+lambda expressions that you can put into `proof-action-list'."
+  ;;(message "PTSGC %s" state)
+  (proof-tree-update-sequent state)
+  (run-hooks 'proof-state-change-hook))
+
+(defun proof-tree-make-show-goal-callback (state)
+  "Create the callback for display-goal commands."
+  `(lambda (span) (proof-tree-show-goal-callback ,state)))
+
+(defun proof-tree-urgent-action (flags)
+  "Handle urgent points before the next item is sent to the proof assistant.
+Schedule goal updates when existential variables have changed and
+call `proof-tree-urgent-action-hook'. All this is only done if
+the current output does not come from a command (with the
+'proof-tree-show-subgoal flag) that this package inserted itself.
+
+Urgent actions are only needed if the external proof display is
+currently running. Therefore this function should not be called
+when `proof-tree-external-display' is nil. 
+
+This function assumes that the prover output is not suppressed.
+Therefore, `proof-tree-external-display' being t is actually a
+necessary precondition.
+
+The not yet delayed output is in the region
+\[proof-shell-delayed-output-start, proof-shell-delayed-output-end]."
+  ;; (message "PTUA flags %s start %s end %s pal %s ptea %s"
+  ;; 	   flags
+  ;; 	   proof-shell-delayed-output-start
+  ;; 	   proof-shell-delayed-output-end
+  ;; 	   proof-action-list
+  ;; 	   proof-tree-existentials-alist)
+  (let* ((proof-info (funcall proof-tree-get-proof-info))
+	 (state (car proof-info))
+	 (start proof-shell-delayed-output-start)
+	 (end proof-shell-delayed-output-end)
+	 inst-ex-vars)
+    (when (and (not (memq 'proof-tree-show-subgoal flags))
+	       (> state proof-tree-last-state))
+      ;; Only deal with existentials if the proof assistant has them
+      ;; (i.e., proof-tree-existential-regexp is set) and if there are some
+      ;; goals with existentials.
+      (when (and proof-tree-existential-regexp
+		 proof-tree-existentials-alist)
+	(setq inst-ex-vars
+	      (with-current-buffer proof-shell-buffer
+		(funcall proof-tree-extract-instantiated-existentials
+			 start end)))
+	(dolist (ex-var inst-ex-vars)
+	  (let ((var-goal-assoc (assoc ex-var proof-tree-existentials-alist)))
+	    (when var-goal-assoc
+	      (dolist (sequent-id (cdr var-goal-assoc))
+		(let ((show-cmd
+		       (funcall proof-tree-show-sequent-command sequent-id)))
+		  (if show-cmd
+		      (setq proof-action-list
+			    (cons (proof-shell-action-list-item
+				   show-cmd
+				   (proof-tree-make-show-goal-callback state)
+				   '(no-goals-display no-response-display
+				     proof-tree-show-subgoal))
+				  proof-action-list)))))
+	      (proof-tree-delete-existential-assoc state var-goal-assoc)))))
+      (run-hooks 'proof-tree-urgent-action-hook))
+    ;; (message "PTUA END pal %s ptea %s"
+    ;; 	   proof-action-list
+    ;; 	   proof-tree-existentials-alist)
+  ))
+
+
+;;
+;; Process output from the proof assistant
+;;
+
+(defun proof-tree-quit-proof ()
+  "Reset internal state when there is no current proof any more.
+Because currently it is not possible to undo into the middle of a
+proof, we can safely flush the `proof-tree-sequent-hash' and
+`proof-tree-existentials-alist-history' when the current proof is
+finished or quit."
+  (clrhash proof-tree-sequent-hash)
+  (setq proof-tree-existentials-alist-history nil)
+  (setq proof-tree-current-proof nil))
+
+(defun proof-tree-register-existentials (current-state sequent-id sequent-text)
+  "Register existential variables that appear in SEQUENT-TEXT.
+If SEQUENT-TEXT contains existential variables, then SEQUENT-ID
+is stored in `proof-tree-existentials-alist'."
+  (if proof-tree-existential-regexp
+      (let ((start 0))
+	(while (proof-string-match proof-tree-existential-regexp
+				   sequent-text start)
+	  (setq start (match-end 0))
+	  (proof-tree-add-existential-assoc current-state
+					    (match-string 1 sequent-text)
+					    sequent-id)))))
+
+(defun proof-tree-extract-goals (start end)
+  "Extract the current goal state information from the delayed output.
+If there is a current goal, return a list containing (in
+this order) the ID of the current sequent, the text of the
+current sequent and the list of ID's of additionally open goals.
+The delayed output is expected between START and END in the
+current buffer."
+  (goto-char start)
+  (if (proof-re-search-forward proof-tree-current-goal-regexp end t)
+      (let ((sequent-id (match-string-no-properties 1))
+	    (sequent-text (match-string-no-properties 2))
+	    additional-goal-ids)
+	(goto-char start)
+	(while (proof-re-search-forward proof-tree-additional-subgoal-ID-regexp
+					end t)
+	  (let ((other-id (match-string-no-properties 1)))
+	    (setq additional-goal-ids (cons other-id additional-goal-ids))))
+	(setq additional-goal-ids (nreverse additional-goal-ids))
+	(list sequent-id sequent-text additional-goal-ids))
+    nil))
+
+
+(defun proof-tree-extract-list (start end start-regexp end-regexp item-regexp)
+  "Extract items between START-REGEXP and END-REGEXP.
+In the region given by START and END, determine the subregion
+between START-REGEXP and END-REGEXP and return the list of all
+items in the subregion. An item is a match of subgroub 1 of
+ITEM-REGEXP. The items in the returned list have the same order
+as in the text.
+
+Return nil if START-REGEXP or ITEM-REGEXP is nil. The subregion
+extends up to END if END-REGEXP is nil."
+  (let (result)
+    (when (and start-regexp item-regexp)
+      (goto-char start)
+      (when (proof-re-search-forward start-regexp end t)
+	(setq start (point))
+	(if (and end-regexp (proof-re-search-forward end-regexp end t))
+	    (setq end (match-beginning 0)))
+	(goto-char start)
+        (while (proof-re-search-forward item-regexp end t)
+          (setq result (cons (match-string-no-properties 1)
+                             result)))))
+    (nreverse result)))
+
+(defun proof-tree-extract-existential-info (start end)
+  "Extract the information display of existential variables.
+This function cuts out the text between
+`proof-tree-existentials-state-start-regexp' and
+`proof-tree-existentials-state-end-regexp' from the prover
+output, including the matches of these regular expressions. If
+the start regexp is nil, the empty string is returned. If the end
+regexp is nil, the match expands to the end of the prover output."
+  (if (and proof-tree-existentials-state-start-regexp
+	   (proof-re-search-forward proof-tree-existentials-state-start-regexp
+				    end t))
+      (progn
+	(setq start (match-beginning 0))
+	(when (and proof-tree-existentials-state-end-regexp
+		   (proof-re-search-forward
+		    proof-tree-existentials-state-end-regexp end t))
+	  (setq end (match-end 0)))
+	(buffer-substring-no-properties start end))
+    ""))
+
+(defun proof-tree-handle-proof-progress (cmd-string proof-info)
+  "Send CMD-STRING and goals in delayed output to prooftree.
+This function is called if there is some real progress in a
+proof. This function sends the current state, the current goal
+and the list of additional open subgoals to prooftree. Prooftree
+will sort out the rest.
+
+The delayed output is in the region
+\[proof-shell-delayed-output-start, proof-shell-delayed-output-end]."
+  ;; (message "PTHPO cmd |%s| info %s flags %s start %s end %s"
+  ;; 	   cmd proof-info flags
+  ;; 	   proof-shell-delayed-output-start
+  ;; 	   proof-shell-delayed-output-end)
+  (let* ((start proof-shell-delayed-output-start)
+	 (end   proof-shell-delayed-output-end)
+	 (proof-state (car proof-info))
+	 (proof-name (cadr proof-info))
+	 (cheated-flag
+	  (and proof-tree-cheating-regexp
+	       (proof-string-match proof-tree-cheating-regexp cmd-string)))
+	 (current-goals (proof-tree-extract-goals start end)))
+    (if current-goals
+	(let ((current-sequent-id (car current-goals))
+	      (current-sequent-text (nth 1 current-goals))
+	      ;; nth 2 current-goals  contains the  additional ID's
+	      (existential-info
+	       (proof-tree-extract-existential-info start end)))
+	  ;; send all to prooftree
+	  (proof-tree-send-goal-state
+	   proof-state proof-name cmd-string
+	   cheated-flag
+	   current-sequent-id
+	   current-sequent-text
+	   (nth 2 current-goals)
+	   existential-info)
+	  ;; put current sequent into hash (if it is not there yet)
+	  (unless (gethash current-sequent-id proof-tree-sequent-hash)
+	    (puthash current-sequent-id proof-state proof-tree-sequent-hash))
+	  (proof-tree-register-existentials proof-state
+					    current-sequent-id
+					    current-sequent-text))
+      
+      ;; no current goal found, maybe the proof has been completed?
+      (goto-char start)
+      (if (proof-re-search-forward proof-tree-proof-completed-regexp end t)
+	  (progn
+	    (proof-tree-send-proof-completed proof-state proof-name
+					     cmd-string cheated-flag)
+	    (proof-tree-reset-existentials proof-state))))))
+
+(defun proof-tree-handle-navigation (proof-info)
+  "Handle a navigation command.
+This function is called if there was a navigation command, which
+results in a different goal being current now.
+
+The delayed output of the navigation command is in the region
+\[proof-shell-delayed-output-start, proof-shell-delayed-output-end]."
+  (let ((start proof-shell-delayed-output-start)
+	(end   proof-shell-delayed-output-end)
+	(proof-state (car proof-info))
+	(proof-name (cadr proof-info)))
+    (goto-char start)
+    (if (proof-re-search-forward proof-tree-current-goal-regexp end t)
+	(let ((current-id (match-string-no-properties 1)))
+	  ;; send all to prooftree
+	  (proof-tree-send-switch-goal proof-state proof-name current-id)))))
+
+
+(defun proof-tree-handle-proof-command (cmd proof-info)
+  "Display current goal in prooftree unless CMD should be ignored."
+  ;; (message "PTHPC")
+  (let ((proof-state (car proof-info))
+	(cmd-string (mapconcat 'identity cmd " ")))
+    (unless (and proof-tree-ignored-commands-regexp
+		 (proof-string-match proof-tree-ignored-commands-regexp
+				     cmd-string))
+      (if (and proof-tree-navigation-command-regexp
+	       (proof-string-match proof-tree-navigation-command-regexp
+				   cmd-string))
+	  (proof-tree-handle-navigation proof-info)
+	(proof-tree-handle-proof-progress cmd-string proof-info)))
+    (setq proof-tree-last-state (car proof-info))))
+    
+(defun proof-tree-handle-undo (proof-info)
+  "Undo prooftree to current state.
+Send the undo command to prooftree and undo changes to the
+internal state of this package. The latter involves currently two
+points:
+* delete those goals from `proof-tree-sequent-hash' that have
+  been generated after the state to which we undo now
+* change proof-tree-existentials-alist back to its previous content"
+  ;; (message "PTHU info %s" proof-info)
+  (let ((proof-state (car proof-info)))
+    ;; delete sequents from the hash
+    (maphash
+     (lambda (sequent-id state)
+       (if (> state proof-state)
+	   (remhash sequent-id proof-tree-sequent-hash)))
+     proof-tree-sequent-hash)
+    ;; undo changes in other state vars
+    (proof-tree-undo-existentials proof-state)
+    (unless (equal (cadr proof-info) proof-tree-current-proof)
+      ;; went back to a point before the start of the proof that we
+      ;; are displaying;
+      ;; or we have not started to display something
+      (proof-tree-quit-proof))
+    ;; disable proof tree display when undoing to a point outside a proof
+    (unless proof-tree-current-proof
+      (setq proof-tree-external-display nil))
+    ;; send undo
+    (if (proof-tree-is-running)
+	(proof-tree-send-undo proof-state))
+    (setq proof-tree-last-state (- proof-state 1))))
+
+
+(defun proof-tree-update-sequent (proof-state)
+  "Prepare an update-sequent command for prooftree.
+This function processes delayed output that the proof assistant
+generated in response to commands that Proof General inserted in
+order to keep prooftree up-to-date. Such commands are tagged with
+a 'proof-tree-show-subgoal flag.
+
+This function uses `proof-tree-update-goal-regexp' to find a
+sequent and its ID in the delayed output. If something is found
+an appropriate update-sequent command is sent to prooftree.
+
+The update-sequent command is associated with state PROOF-STATE
+for proper undo effects, see also the comments for
+`proof-tree-show-goal-callback'.
+
+The delayed output is in the region
+\[proof-shell-delayed-output-start, proof-shell-delayed-output-end]."
+  ;; (message "PTUS buf %s output %d-%d state %s"
+  ;; 	   (current-buffer)
+  ;; 	   proof-shell-delayed-output-start proof-shell-delayed-output-end
+  ;; 	   proof-state)
+  (if (proof-tree-is-running)
+      (with-current-buffer proof-shell-buffer
+	(let* ((start proof-shell-delayed-output-start)
+	       (end   proof-shell-delayed-output-end)
+	       (proof-info (funcall proof-tree-get-proof-info))
+	       (proof-name (cadr proof-info)))
+	  (goto-char start)
+	  (if (proof-re-search-forward proof-tree-update-goal-regexp end t)
+	      (let ((sequent-id (match-string-no-properties 1))
+		    (sequent-text (match-string-no-properties 2)))
+		(proof-tree-send-update-sequent
+		 proof-state proof-name sequent-id sequent-text)
+		;; put current sequent into hash (if it is not there yet)
+		(unless (gethash sequent-id proof-tree-sequent-hash)
+		  (puthash sequent-id proof-state proof-tree-sequent-hash))
+		(proof-tree-register-existentials proof-state
+						  sequent-id
+						  sequent-text)))))))
+
+
+(defun proof-tree-handle-delayed-output (cmd flags span)
+  "Process delayed output for prooftree.
+This function is the main entry point of the Proof General
+prooftree support. It examines the delayed output in order to
+take appropriate actions and maintains the internal state.
+
+All arguments are (former) fields of the `proof-action-list'
+entry that is now finally retired. CMD is the command, FLAGS are
+the flags and SPAN is the span."
+  ;; (message "PTHDO cmd %s flags %s span %s-%s" cmd flags
+  ;; 	   (if span (span-start span)) (if span (span-end span)))
+  (assert proof-tree-external-display)
+  (unless (or (memq 'invisible flags) (memq 'proof-tree-show-subgoal flags))
+    (let* ((proof-info (funcall proof-tree-get-proof-info))
+	   (current-proof-name (cadr proof-info)))
+      (save-excursion
+	(if (<= (car proof-info) proof-tree-last-state)
+	    ;; went back to some old state: there must have been an undo command
+	    (proof-tree-handle-undo proof-info)
+
+	  ;; else -- no undo command
+	  ;; first maintain proof-tree-current-proof
+	  (cond
+	   ((and (null proof-tree-current-proof) current-proof-name)
+	    ;; started a new proof
+	    (setq proof-tree-current-proof current-proof-name))
+	   ((and proof-tree-current-proof (null current-proof-name))
+	    ;; finished the current proof
+	    (proof-tree-quit-proof)
+	    (setq proof-tree-external-display nil))
+	   ((and proof-tree-current-proof current-proof-name
+		 (not (equal proof-tree-current-proof current-proof-name)))
+	    ;; new proof before old was finished?
+	    (display-warning
+	     '(proof-general proof-tree)
+	     "Nested proofs are not supported in prooftree display"
+	     :warning)
+	    ;; try to keep consistency nevertheless
+	    (setq proof-tree-current-proof current-proof-name)))
+
+	  ;; send stuff to prooftree now
+	  (when current-proof-name
+	    ;; we are inside a proof: display something
+	    (proof-tree-ensure-running)
+	    (proof-tree-handle-proof-command cmd proof-info)))))))
+
+
+;;
+;; Send undo command when leaving a buffer
+;;
+
+(defun proof-tree-leave-buffer ()
+  "Send an undo command to prooftree when leaving a buffer."
+  (if (and proof-tree-configured (proof-tree-is-running))
+      (proof-tree-send-undo 0)))
+
+(add-hook 'proof-deactivate-scripting-hook 'proof-tree-leave-buffer)
+
+
+;;
+;; User interface
+;;
+
+(defun proof-tree-display-current-proof (proof-start)
+  "Start an external proof-tree display for the current proof.
+Coq (and probably other proof assistants as well) does not
+support outputing the current proof tree. Therefore this function
+retracts to the start of the current proof, switches the
+proof-tree display on, and reasserts then until the former end of
+the locked region. Argument PROOF-START must contain the start
+position of the current proof."
+  ;;(message "PTDCP %s" proof-tree-external-display)
+  (unless (and proof-script-buffer
+	       (equal proof-script-buffer (current-buffer)))
+    (error
+     "Enabling prooftree inside a proof outside the current scripting buffer"))
+  (proof-shell-ready-prover)
+  (assert proof-locked-span)
+  (message "Start proof-tree display for current proof")
+  (save-excursion
+    (save-window-excursion
+      (let ((locked-end (span-end proof-locked-span)))
+	(goto-char proof-start)
+	;; enable external display to make sure the undo command is send
+	(setq proof-tree-external-display t)
+	(proof-retract-until-point)
+	(while (consp proof-action-list)
+	  (accept-process-output))
+	;; undo switched external display off; switch on again
+	(setq proof-tree-external-display t)
+	(goto-char locked-end)
+	(proof-assert-until-point)
+	(while (consp proof-action-list)
+	  (accept-process-output))))))
+
+(defun proof-tree-external-display-toggle ()
+  "Toggle the external proof-tree display.
+When called outside a proof the external proof-tree display will
+be enabled for the next proof. When called inside a proof the
+proof display will be created for the current proof. If the
+external proof-tree display is currently on, then this toggle
+will switch it off. At the end of the proof the proof-tree
+display is switched off."
+  (interactive)
+  (unless proof-tree-configured
+    (error "External proof-tree display not configured for %s" proof-assistant))
+  (cond
+   (proof-tree-external-display
+    ;; Currently on -> switch off
+    (setq proof-tree-external-display nil)
+    (when proof-tree-current-proof
+      (proof-tree-send-quit-proof proof-tree-current-proof)
+      (proof-tree-quit-proof))
+    (message "External proof-tree display switched off"))
+   (t
+    ;; Currently off
+    (let ((proof-start (funcall proof-tree-find-begin-of-unfinished-proof)))
+      ;; ensure internal variables are initialized, because otherwise
+      ;; we cannot process undo's after this
+      (proof-tree-ensure-running)
+      (setq proof-tree-current-proof nil)
+      (setq proof-tree-last-state (car (funcall proof-tree-get-proof-info)))
+      (if proof-start
+	  ;; inside an unfinished proof -> start for this proof
+	  (proof-tree-display-current-proof proof-start)
+	;; outside a proof -> wait for the next proof
+	(setq proof-tree-external-display t)
+	(proof-tree-send-undo proof-tree-last-state)
+	(message
+	 "External proof-tree display switched on for the next proof"))))))
+    
+
+;;
+;; Trailer
+;; 
+
+(provide 'proof-tree)
+
+;;; tree-tree.el ends here
diff --git a/generic/proof.el b/generic/proof.el
index 794f5445..1acfae71 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -34,6 +34,7 @@
 (require 'proof-config)			; configuration variables
 (require 'proof-auxmodes)		; auxmode functions
 (require 'proof-script)			; script mode
+(require 'proof-tree)			; proof tree visualization with prooftree
 (require 'proof-shell)			; shell mode
 
 (provide 'proof)
diff --git a/images/epg-prooftree.png b/images/epg-prooftree.png
new file mode 100644
index 00000000..0de55213
--- /dev/null
+++ b/images/epg-prooftree.png
diff --git a/images/epg-prooftree.xpm b/images/epg-prooftree.xpm
new file mode 100644
index 00000000..3fd2ecf2
--- /dev/null
+++ b/images/epg-prooftree.xpm
@@ -0,0 +1,30 @@
+/* XPM */
+static char * epg_prooftree_xpm[] = {
+"24 24 3 1",
+" 	c None",
+".	c #A52A2A",
+"+	c #0000FF",
+"                        ",
+"                        ",
+"          .             ",
+"          .             ",
+"          .             ",
+"          .....         ",
+"          .             ",
+"          .             ",
+"          .             ",
+"                        ",
+"          ++ ..         ",
+"          +   ..        ",
+"         +     ..       ",
+"        +       ..      ",
+"       +         ..     ",
+"  +              .      ",
+"  +              .      ",
+"  +              .      ",
+"  +++++          .....  ",
+"  +              .      ",
+"  +              .      ",
+"  +              .      ",
+"                        ",
+"                        "};