Update magic

2 files changed, 6 insertions, 3 deletions

diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index ee3a75c7..c12a95c2 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -3438,6 +3438,7 @@ Insert @var{string} at the end of the proof shell, call @samp{@code{comint-send-
 
 First call @samp{@code{proof-shell-insert-hook}}.  The argument @var{action} may be
 examined by the hook to determine how to process the @var{string} variable.
+NB: the hook is not called for the empty (null) string.
 
 Then strip @var{string} of carriage returns before inserting it and updating
 @samp{@code{proof-marker}} to point to the end of the newly inserted text.
@@ -3508,7 +3509,7 @@ if you don't need it (slight speed penalty).
 
 @c TEXI DOCSTRING MAGIC: proof-shell-last-prompt
 @defvar proof-shell-last-prompt 
-A record of the last prompt seen from the proof system.@*
+A raw record of the last prompt seen from the proof system.@*
 This is the string matched by @samp{@code{proof-shell-annotated-prompt-regexp}}.
 @end defvar
 
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 1ec274d8..3dc7cf1e 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -2415,11 +2415,13 @@ character is inserted without the prompt.
 @end deffn
 @c TEXI DOCSTRING MAGIC: unicode-tokens-rotate-glyph-forward
 @deffn Command unicode-tokens-rotate-glyph-forward &optional n
-Not documented.
+Rotate the character before point in the current code page, by @var{n} steps.@*
+If no character is found at the new codepoint, no change is made.
 @end deffn
 @c TEXI DOCSTRING MAGIC: unicode-tokens-rotate-glyph-backward
 @deffn Command unicode-tokens-rotate-glyph-backward &optional n
-Not documented.
+Rotate the character before point in the current code page, by -N steps.@*
+If no character is found at the new codepoint, no change is made.
 @end deffn
 Unfortunately, the precise set of symbol glyphs that are available to
 you will depend in complicated ways on your operating system, Emacs