From f9fc09abc97576f0e1a54439b921a9e97a7f73f8 Mon Sep 17 00:00:00 2001
From: Hendrik Tews <hendrik@askra.de>
Date: Sun, 7 Jan 2024 18:19:57 +0100
Subject: [PATCH] prooftree: polish

This commit addresses all the points that have only been marked in the
previous prooftree related commits.
---
 coq/coq.el             |  9 ++++++---
 generic/proof-shell.el |  4 ----
 generic/proof-tree.el  | 15 ++++++++++-----
 3 files changed, 16 insertions(+), 12 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index 6bea247fa..11b5edc38 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1930,7 +1930,7 @@ at `proof-assistant-settings-cmds' evaluation time.")
 
   ;; prooftree config
   (setq
-   proof-tree-configured t
+   proof-tree-configured (coq--post-v810)
    proof-tree-get-proof-info 'coq-proof-tree-get-proof-info
    proof-tree-find-begin-of-unfinished-proof
      'coq-find-begin-of-unfinished-proof)
@@ -2237,7 +2237,9 @@ This is the Coq incarnation of `proof-tree-find-undo-position'."
    (list 'invisible 'no-response-display)))
 
 (defun coq-proof-tree-enable-evars ()
-  "Enable the evar status line for Coq >= 8.6."
+  "Enable the evar status line."
+  ;; The evar status can be switched on and off since 8.6. However, prooftree
+  ;; is only supported for 8.10 or later.
   (when (and (coq--post-v86) coq-proof-tree-manage-dependent-evar-line)
     (proof-shell-ready-prover)
     (proof-add-to-priority-queue (coq-proof-tree-evar-command "Set"))))
@@ -2247,7 +2249,8 @@ This is the Coq incarnation of `proof-tree-find-undo-position'."
 (defun coq-proof-tree-disable-evars ()
   "Return action list item to disable evar printing.
 Function for `proof-tree-display-stop-command'."
-  ;; XXX disable proof tree completely for < 8.10
+  ;; The evar status can be switched on and off since 8.6. However, prooftree
+  ;; is only supported for 8.10 or later.
   (when (and (coq--post-v86) coq-proof-tree-manage-dependent-evar-line)
     (coq-proof-tree-evar-command "Unset")))
 
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index ecce5a4ce..52defb6b6 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1335,10 +1335,6 @@ ends with text matching `proof-shell-eager-annotation-end'."
    ((proof-looking-at-safe proof-shell-theorem-dependency-list-regexp)
     (proof-shell-process-urgent-message-thmdeps))
 
-   ;;XXX duplication?
-   ((proof-looking-at-safe proof-shell-theorem-dependency-list-regexp)
-    (proof-shell-process-urgent-message-thmdeps))
-
    ((proof-looking-at-safe proof-shell-interactive-prompt-regexp)
     (proof-shell-process-interactive-prompt-regexp))
 
diff --git a/generic/proof-tree.el b/generic/proof-tree.el
index ab90917aa..f256b8523 100644
--- a/generic/proof-tree.el
+++ b/generic/proof-tree.el
@@ -338,8 +338,13 @@ instantiated. When a proof finishes with proof-tree display,
 prooftree may request a number of show goal commands after the
 proof has been finished in the proof assistant. This function
 must return an action item that can be inserted as last command
-in `proof-action-list' after all these show goal commands. An
-action item is a list `(SPAN COMMANDS ACTION [DISPLAYFLAGS])',
+in `proof-action-list' after all these show goal commands.
+
+For Coq this is used to disable the dependent evar line. But also
+other proof assistants that enable the proof tree display must
+set this function.
+
+An action item is a list `(SPAN COMMANDS ACTION [DISPLAYFLAGS])',
 see `proof-action-list'. The action item must not be recognized
 as comment by `proof-shell-slurp-comments', that is COMMANDS must
 be a nonempty list of strings. The generic prooftree glue code
@@ -516,7 +521,6 @@ Add command `proof-tree-display-stop-command' with
 `proof-tree-check-proof-finish' eventually sees this last command
 and switches the proof-tree display processing off."
   (if (string-match proof-tree--confirm-complete-regexp data)
-      ;; XXX assert proof-tree-display-stop-command when proof-tree is started
       (let ((stop-cmd (funcall proof-tree-display-stop-command)))
         ;; an action list item is a list (span commands action [displayflags])
         (proof-add-to-priority-queue
@@ -1174,8 +1178,9 @@ 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))
+  (unless (and proof-tree-configured proof-tree-display-stop-command)
+    (error "External proof-tree display not or not correctly configured for %s"
+           proof-assistant))
   (cond
    (proof-tree-external-display
     ;; Currently on -> switch off