prooftree: fix Unshelve and delete new layer recognition

Support Unshelve after all goals have been closed, which shall create
a new layer with all the unshelved goals. Prooftree contains enough
state to determine whether or not a new layer must be created.
Therefore erase the regular expression to recognize commands that are
expected to create a new layer. Also erase the new-layer flag from the
current-goals display command.

NOTE: This commit changes the Prooftree communication protocol. Use
only with Prooftree containing a patch with the same header.

coq/coq.el

@@ -208,12 +208,6 @@ It is mostly useful in three window mode, see also
   :type 'regexp
   :group 'coq-proof-tree)
 
-(defcustom coq-proof-tree-new-layer-command-regexp
-  "^\\(\\(Proof\\)\\|\\(Grab Existential Variables\\)\\)"
-  "Regexp for `proof-tree-new-layer-command-regexp'."
-  :type 'regexp
-  :group 'coq-proof-tree)
-
 (defcustom coq-proof-tree-current-goal-regexp
   (concat "^[0-9]+ \\(?:focused \\)?\\(?:sub\\)?goal\\(?:s\\)?\\s-*"
           "\\(?:(\\(?:unfocused: [-0-9]+\\)?,?"
@@ -2022,7 +2016,6 @@ at `proof-assistant-settings-cmds' evaluation time.")
    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-new-layer-command-regexp coq-proof-tree-new-layer-command-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-existentials-state-start-regexp

doc/PG-adapting.texi

@@ -2644,17 +2644,8 @@ proof goal. The second layer contains proof trees for goals that
 have been added to the proof after the first proof tree was
 completed. And so on.
 
-To organize the layers, Prooftree must identify those proof
-commands that add new goals to a proof.
-
-@c TEXI DOCSTRING MAGIC: proof-tree-new-layer-command-regexp
-@defvar proof-tree-new-layer-command-regexp 
-Regexp to match proof commands that add new goals to a proof.@*
-This regexp must match the command that turns the proof assistant
-into prover mode, which adds the initial goal to the proof.  It
-must further match commands that add additional goals after all
-previous goals have been proved.
-@end defvar
+Prooftree assumes a new layer when it receives new goals in a state
+where the number of open goals is zero.
 
 
 @node Prerequisites

generic/proof-tree.el

@@ -184,15 +184,6 @@ Coq.  Leave at nil if there are no cheating commands."
   :type '(choice regexp (const nil))
   :group 'proof-tree-internals)
 
-(defcustom proof-tree-new-layer-command-regexp nil
-  "Regexp to match proof commands that add new goals to a proof.
-This regexp must match the command that turns the proof assistant
-into prover mode, which adds the initial goal to the proof.  It
-must further match commands that add additional goals after all
-previous goals have been proved."
-  :type 'regexp
-  :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
@@ -713,7 +704,7 @@ DATA as data sections to Prooftree."
    ()))
 
 (defun proof-tree-send-goal-state (state proof-name command-string cheated-flag
-				   layer-flag current-sequent-id
+				   current-sequent-id
 				   current-sequent-text additional-sequent-ids
 				   existential-info)
   "Send the current goal state to prooftree."
@@ -723,14 +714,13 @@ DATA as data sections to Prooftree."
   (let* ((add-id-string (mapconcat #'identity additional-sequent-ids " "))
 	 (second-line
 	  (format
-	   (concat "current-goals state %d current-sequent %s %s %s "
+	   (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")
-	   (if layer-flag "new-layer" "current-layer")
 	   (1+ (string-bytes proof-name))
 	   (1+ (string-bytes command-string))
 	   (1+ (string-bytes current-sequent-text))
@@ -931,7 +921,9 @@ regexp is nil, the match expands to the end of the prover output."
 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.
+will sort out the rest. In particular, Prooftree determines
+without input from this function, whether or not a new layer in
+the proof tree must be started.
 
 The delayed output is in the region
 \[proof-shell-delayed-output-start, proof-shell-delayed-output-end].
@@ -962,16 +954,12 @@ command was sent to the proof assistant."
       (setq current-goals (proof-tree-extract-goals start end))
       (when 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
-	      (layer-flag
-	       (and proof-tree-new-layer-command-regexp
-		    (proof-string-match proof-tree-new-layer-command-regexp
-					cmd-string))))
-	  ;; send all to prooftree
+	      (current-sequent-text (nth 1 current-goals)))
+	  ;; Note that (nth 2 current-goals) contains the  additional ID's.
+	  ;; Now send all to prooftree.
 	  (proof-tree-send-goal-state
 	   proof-state proof-name cmd-string
-	   cheated-flag layer-flag
+	   cheated-flag
 	   current-sequent-id
 	   current-sequent-text
 	   (nth 2 current-goals)