| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The goals buffer settings allow configuration of Proof General for proof by pointing or similar features. See the Proof General documentation web page for a link to the technical report ECS-LFCS-97-368 which hints at how to use these settings.
Command to change to the goal ‘%s’.
Command sent when ‘pg-goals-button-action’ is requested on a goal.
Command sent when ‘pg-goals-button-action’ is requested on an assumption.
Regexp indicating that the proof process has identified an error.
Regexp matching start of an output from the prover after pbp commands.
In particular, after a ‘pbp-goal-command’ or a ‘pbp-hyp-command’.
Regexp matching end of output from the prover after pbp commands.
In particular, after a ‘pbp-goal-command’ or a ‘pbp-hyp-command’.
Opening special character for subterm markup.
Subsequent special characters with values below
‘pg-subterm-first-special-char’ are assumed to be subterm position
indicators. Annotations should be finished with ‘pg-subterm-sep-char’;
the end of the concrete syntax is indicated by ‘pg-subterm-end-char’.
If ‘pg-subterm-start-char’ is nil, subterm markup is disabled.
Finishing special for a subterm markup.
See doc of ‘pg-subterm-start-char’.
Annotation regexp that indicates the beginning of a "top" element.
A "top" element may be a sub-goal to be proved or a named hypothesis,
for example. It could also be a literal command to insert and
send back to the prover.
The function ‘pg-topterm-goalhyplit-fn’ examines text following this
special character, to determine what kind of top element it is.
This setting is also used to see if proof-by-pointing features are configured. If it is unset, some of the code for parsing the prover output is disabled.
Closing special character for subterm markup.
See ‘pg-subterm-start-char’.
| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This document was generated on July 22, 2013 using texi2html 5.0.