From 4d923ab403743c3c091ba3feec10757fae3b2fec Mon Sep 17 00:00:00 2001
From: Hendrik Tews
Date: Wed, 26 Jan 2011 15:50:40 +0000
Subject: - more info on the elements of proof-action-list; the COMMANDS   list
 in it should be concatenated with (mapconcat 'identity   COMMANDS " "), which
 is not the case proof-shell-insert.

---
 generic/proof-shell.el | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

(limited to 'generic')

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 302b8400..02b024a0 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -40,7 +40,25 @@ The value is a list of lists of the form
 
    (SPAN COMMANDS ACTION [DISPLAYFLAGS])
 
-which is the queue of things to do.  The display flags are set
+which is the queue of things to do.
+
+SPAN is a region in the sources, where COMMANDS come from. Often,
+additional properties are recorded as properties of SPAN.
+
+COMMANDS is a list of strings, holding the text to be send to the
+prover. It might be the empty list is nothing needs to be sent to
+the prover, such as, for instance, for comments. Usually COMMANDS
+contains just 1 string, but it might also contains more elements.
+The text should be obtained with
+`(mapconcat 'identity COMMANDS \" \")', where the last argument
+is a space.
+
+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.
+
+The DISPLAYFLAGS are set
 for non-scripting commands or for when scripting should not
 bother the user.  They may include
 
-- 
cgit v1.2.3