- 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.

1 files changed, 19 insertions, 1 deletions

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