further documentation of LEGO specific bug

2 files changed, 17 insertions, 6 deletions

diff --git a/BUGS b/BUGS
index 5585ca68..c3cce6ba 100644
--- a/BUGS
+++ b/BUGS
@@ -69,7 +69,7 @@ LEGO Proof General Bugs
 
 * If LEGO attempts to write a (object) file in a non-writable
   directory, it forgets the protocol mechanism on how to interact with 
-  Proof General and gets stuck. Workaround: directly enter "Configure
+  Proof General and gets stuck. Workaround: Directly enter "Configure
   AnnotateOn" in the Proof Shell to recover.
 
 * After a `Discharge', retraction ought to only be possible back to the
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 85516dc3..cf942022 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -113,7 +113,6 @@ Version control stamp: @code{@value{rcsid}}
 
 @page
 
-
 @ifinfo
 @node Top
 @top Proof General
@@ -1058,16 +1057,18 @@ If inside a comment, just process until the start of the comment.
 @end deffn
 
 @c TEXI DOCSTRING MAGIC: proof-undo-last-successful-command-interactive
-@deffn Command proof-undo-last-successful-command-interactive 
+@deffn Command proof-undo-last-successful-command-interactive delete
 Undo last successful command at end of locked region.
-The text is also deleted from the proof script.
+If optional @var{delete} argument is set (called with a prefix argument), 
+the text is also deleted from the proof script.
 @end deffn
 
 @c TEXI DOCSTRING MAGIC: proof-retract-until-point-interactive
-@deffn Command proof-retract-until-point-interactive 
+@deffn Command proof-retract-until-point-interactive delete-region
 Tell the proof process to retract until point.
 If invoked outside a locked region, undo the last successfully processed
-command.
+command.  If called with a prefix argument (@var{delete-region} non-nil), also
+delete the retracted region from the proof-script.
 @end deffn
 
 @c TEXI DOCSTRING MAGIC: proof-process-buffer
@@ -3775,6 +3776,7 @@ the system.
 @menu
 * Retraction and Discharge::    
 * Retraction and proving::      
+* Non writable directories::    
 @end menu
 
 @node Retraction and Discharge
@@ -3817,6 +3819,15 @@ proper @samp{Save} command.
 a proof. If you forget one, you should retract to a point before the
 offending proof development.
 
+@node Non writable directories
+@subsection Non-writable directories
+
+If LEGO 1.3.1 attempts to write a (object) file in a non-writable
+directory, it forgets the protocol mechanism on how to interact with 
+Proof General and gets stuck. 
+
+@strong{Workaround:} Directly enter @kbd{Configure AnnotateOn;} in the Proof Shell to recover.
+
 @node Bugs specific to Coq Proof General
 @section Bugs specific to Coq Proof General