From 35dae9b203b0fc918e56deb9926b44d19042ed9d Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 7 Aug 2002 13:55:58 +0000 Subject: Doc proof-shell-strip-crs-from-output; update magic --- doc/PG-adapting.texi | 25 +++++++++++++++++-------- doc/ProofGeneral.texi | 2 +- 2 files changed, 18 insertions(+), 9 deletions(-) (limited to 'doc') diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 89313ce4..7b4d06da 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -640,7 +640,7 @@ development distribution includes a button blank and some notes in @c TEXI DOCSTRING MAGIC: proof-toolbar-entries-default @defvar proof-toolbar-entries-default -Example value for proof-toolbar-entries. Also used to define Scripting menu.@* +Example value for proof-toolbar-entries. Also used to define scripting menu.@* This gives a bare toolbar that works for any prover, providing the appropriate configuration variables are set. To add/remove prover specific buttons, adjust the @samp{-toolbar-entries} @@ -1249,7 +1249,7 @@ List of identifiers to use for completion for this proof assistant.@* Completion is activated with C-return. If this table is empty or needs adjusting, please make changes using -@samp{@code{customize-variable}} and send suggestions to proofgen@@dcs.ed.ac.uk. +@samp{@code{customize-variable}} and send suggestions to support@@proofgeneral.org @end defvar @c TEXI DOCSTRING MAGIC: proof-add-completions @@ -1922,13 +1922,11 @@ Command to change to the goal @samp{%s} @end defvar @c TEXI DOCSTRING MAGIC: pbp-goal-command @defvar pbp-goal-command -Command informing the prover that @samp{@code{pg-goals-button-action}} has been@* -requested on a goal. +Command sent when @samp{@code{pg-goals-button-action}} is requested on a goal. @end defvar @c TEXI DOCSTRING MAGIC: pbp-hyp-command @defvar pbp-hyp-command -Command informing the prover that @samp{@code{pg-goals-button-action}} has been@* -requested on an assumption. +Command sent when @samp{@code{pg-goals-button-action}} is requested on an assumption. @end defvar @c TEXI DOCSTRING MAGIC: pg-goals-error-regexp @defvar pg-goals-error-regexp @@ -3291,7 +3289,10 @@ urgent message will be a candidate for the goal or response buffer. The internal variable @code{proof-shell-urgent-message-marker} tracks the last urgent message seen. -When output is grabbed from the prover process, it is stored into +When output is grabbed from the prover process, the first action +is to strip spurious carriage return characters from the end of +lines, if @code{proof-shell-strip-crs-from-output} requires it. +Then the output is stored into @code{proof-shell-last-output}, and its type is stored in @code{proof-shell-last-output-kind}. Output which is deferred or possibly discarded until the queue is empty is copied into @@ -3301,12 +3302,20 @@ seen from the prover process is also kept, in @code{proof-shell-last-prompt}. -@c TEXI DOCSTRING MAGIC: proof-shell-last-prompt +@c TEXI DOCSTRING MAGIC: proof-shell-strip-crs-from-output + +@defvar proof-shell-strip-crs-from-output +If non-nil, remove carriage returns (^M) at the end of lines from output.@* +This is enabled for cygwin32 systems by default. You should turn it off +if you don't need it (slight speed penalty). +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-last-prompt @defvar proof-shell-last-prompt A record of the last prompt seen from the proof system.@* This is the string matched by @code{proof-shell-annotated-prompt-regexp}. @end defvar + @c TEXI DOCSTRING MAGIC: proof-shell-last-output @defvar proof-shell-last-output A record of the last string seen from the proof system. diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index bf155222..98a0f4cc 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -2145,7 +2145,7 @@ List of identifiers to use for completion for this proof assistant.@* Completion is activated with C-return. If this table is empty or needs adjusting, please make changes using -@samp{@code{customize-variable}} and send suggestions to proofgen@@dcs.ed.ac.uk. +@samp{@code{customize-variable}} and send suggestions to support@@proofgeneral.org @end defvar The completion facility uses a library @file{completion.el} which -- cgit v1.2.3