diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/PG-adapting.texi | 10 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 2 |
2 files changed, 8 insertions, 4 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index a23a91e7..67248cb4 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -2740,10 +2740,12 @@ 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. +information from Proof General. + +There are only a few messages that Prooftree sends to Proof +General. These messages communicate user requests to Proof +General, for instance, when the user selects the undo menu item, +or when he closes the Prooftree window. The communication protocol is completely described in the @code{ocamldoc} documentation of @code{input.ml} in the Prooftree diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 628fae0f..30e19cfc 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -3158,6 +3158,8 @@ dependencies. given existential variable. @item Snapshots of proof trees for reference when you retract your proof to try a different approach. +@item Trigger a retract (undo) operation with a selected sequent +as target. @end itemize For a more elaborated description please consult the help dialog |