/usr/share/doc/proofgeneral-doc/html/Subterm-Activation-and-Proof-by-Pointing.html

<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<html>
<!-- Created by GNU Texinfo 5.2, http://www.gnu.org/software/texinfo/ -->
<head>
<title>Proof General: Subterm Activation and Proof by Pointing</title>

<meta name="description" content="Proof General: Subterm Activation and Proof by Pointing">
<meta name="keywords" content="Proof General: Subterm Activation and Proof by Pointing">
<meta name="resource-type" content="document">
<meta name="distribution" content="global">
<meta name="Generator" content="makeinfo">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<link href="index.html#Top" rel="start" title="Top">
<link href="Function-Index.html#Function-Index" rel="index" title="Function Index">
<link href="Concept-Index.html#SEC_Contents" rel="contents" title="Table of Contents">
<link href="index.html#Top" rel="up" title="Top">
<link href="Graphical-Proof_002dTree-Visualization.html#Graphical-Proof_002dTree-Visualization" rel="next" title="Graphical Proof-Tree Visualization">
<link href="Support-for-other-Packages.html#Support-for-tags" rel="prev" title="Support for tags">
<style type="text/css">
<!--
/* Style sheet for the Proof General web pages. 
 * David Aspinall, June 1999.
 * proofgen.css,v 4.0 2000/03/13 07:36:57 da Exp
 */


a.summary-letter {text-decoration: none}
blockquote.smallquotation {font-size: smaller}
div.display {margin-left: 3.2em}
div.example {margin-left: 3.2em}
div.indentedblock {margin-left: 3.2em}
div.lisp {margin-left: 3.2em}
div.smalldisplay {margin-left: 3.2em}
div.smallexample {margin-left: 3.2em}
div.smallindentedblock {margin-left: 3.2em; font-size: smaller}
div.smalllisp {margin-left: 3.2em}
kbd {font-style:oblique}
pre.display {font-family: inherit}
pre.format {font-family: inherit}
pre.menu-comment {font-family: serif}
pre.menu-preformatted {font-family: serif}
pre.smalldisplay {font-family: inherit; font-size: smaller}
pre.smallexample {font-size: smaller}
pre.smallformat {font-family: inherit; font-size: smaller}
pre.smalllisp {font-size: smaller}
span.nocodebreak {white-space:nowrap}
span.nolinebreak {white-space:nowrap}
span.roman {font-family:serif; font-weight:normal}
span.sansserif {font-family:sans-serif; font-weight:normal}
ul.no-bullet {list-style: none}
body{
 font-family: Verdana, Arial, sans-serif;
 background: #2D1D03;  /* background brown */
 background-attachment: fixed;
 color: #FFFFFF;
}

p{
 max-width: 1024px;
 font-family: Verdana, Arial, sans-serif;
 color: #FFFFFF;
}
pre{
 color: #FFFFFF;
}
h1{
 color: #FFFFFF;
 font-size: large;
 font-weight: bold;
}
h2{
 font-size: medium;
 font-weight: bold;
 color: #FFFFD0;
 padding: 2px 4px 4px 8px;
 background: #5D2D13;
}
h3{
 font-size: medium;
 padding: 2px 2px 2px 8px;
 margin-right: 50%;
 background: #4D1D23;
 color: #FFFFD0;
}
h4{
 font-size: medium;
 color: #FFD0D0;
 padding: 2px 2px 2px 8px;
}
blockquote,form,input,select{
 color: #FFFFFF;
}
address{
 font-size: small;
 color: #FFFFFF;
}
select {
 font-size: 100%;
 background: #2D1D03;
 color: #FFFFFF;
}
textarea,input {
 font-size: 100%;
 background: #4D2D23;
 color: #FFFFFF;
}
input[type=submit],input[type=reset],input[type=Submit] {
 font-size: 80%;
 padding-top: 0px;
 padding-bottom: 0px;
 background: #401010;
}
#button:active{
 background: #402020;
}

dl,ul,dir,li{
 color: #FFFFFF;
 max-width: 1024px;
}

dt{ font-style: italic; 
    padding: 2px 2px 2px 8px;
    margin-left: 20px;
    margin-right: 20px;
    background: #4D1D23; 
}

table{
 font-family: Verdana, Arial, sans-serif;	
 color: #FFFFFF;
}

table.menubar{
 font-family: Verdana, Arial, sans-serif;	
 font-size: smaller;
 color: #FFFFFF;
}

td,tr{
 color: #FFFFFF;
}

a:link,a:visited{
 font-family: Verdana, Arial, sans-serif;	
 text-decoration: none;
 color: #E0D020;
}

a:active,a:hover{
 font-family: Verdana, Arial, sans-serif;	
 text-decoration: underline;
 color: #E8D830;
}

pre{
 background: #2D1D03;
}

/* Specifics */

p.nb{
 font-size: smaller;
 font-style: italic;
}

/* These bits for Mailman pages for mailing lists */
TD.head1old {
 font-family: Verdana, Arial, sans-serif;
  text-align: center;
  color: #FFFFFF;
  font-weight: bold;
  font-size: 110%;
}
td.head1{
 font-family: Verdana, Arial, sans-serif;
 font-weight: bold;
 font-size: 110%;
 text-align: center;
 color: #FFFFFF;
}
td.head2{
 font-family: Verdana, Arial, sans-serif;
 font-size: 100%;
 font-weight: bold;
 color: #FFFFD0;
 padding: 2px 4px 4px 4px;
 background: #7D4D33;
}
td.head3{
 font-family: Verdana, Arial, sans-serif;	
 padding: 2px 2px 2px 2px;
 margin-right: 10%;
 background: #6D3D43;
 font-size: 80%;
 color: #FFFFD0;
}
td.head4{
 font-family: Verdana, Arial, sans-serif;	
 font-size: 100%;
 font-weight: bold;
 color: #FFD0D0;
}

-->
</style>


</head>

<body lang="en" bgcolor="#FFFFFF" text="#000000" link="#0000FF" vlink="#800080" alink="#FF0000">
<a name="Subterm-Activation-and-Proof-by-Pointing"></a>
<div class="header">
<p>
Next: <a href="Graphical-Proof_002dTree-Visualization.html#Graphical-Proof_002dTree-Visualization" accesskey="n" rel="next">Graphical Proof-Tree Visualization</a>, Previous: <a href="Support-for-other-Packages.html#Support-for-other-Packages" accesskey="p" rel="prev">Support for other Packages</a>, Up: <a href="index.html#Top" accesskey="u" rel="up">Top</a> &nbsp; [<a href="Concept-Index.html#SEC_Contents" title="Table of contents" rel="contents">Contents</a>][<a href="Function-Index.html#Function-Index" title="Index" rel="index">Index</a>]</p>
</div>
<hr>
<a name="Subterm-Activation-and-Proof-by-Pointing-1"></a>
<h2 class="chapter">6 Subterm Activation and Proof by Pointing</h2>

<p>This chapter describes what you can do from inside the goals buffer,
providing support for these features exists for your proof assistant.
</p>
<p>As of Proof General 4.0, this support only exists for LEGO and
proof-by-pointing functionality has been temporarily removed from the
interface.  If you would like to see subterm activation support for
Proof General in another proof assistant, please petition the developers
of that proof assistant to provide it!
</p>

<hr>
<a name="Goals-buffer-commands"></a>
<a name="Goals-buffer-commands-1"></a>
<h3 class="section">6.1 Goals buffer commands</h3>

<p>When you are developing a proof, the input focus (Emacs cursor) is
usually on the script buffer.  Therefore Proof General binds some mouse
buttons for commands in the goals buffer, to avoid the need to move the
cursor between buffers.
</p>
<p>The mouse bindings are these:
</p>
<dl compact="compact">
<dt><kbd>mouse-1</kbd></dt>
<dd><p><code>pg-goals-button-action</code>
</p></dd>
<dt><kbd>C-mouse-3</kbd></dt>
<dd><p><code>proof-undo-and-delete-last-successful-command</code>
</p></dd>
<dt><kbd>C-S-mouse-1</kbd></dt>
<dd><p><code>pg-identifier-under-mouse-query</code>
</p></dd>
</dl>

<p>Where <kbd>mouse-1</kbd> indicates the left mouse button, and <kbd>mouse-3</kbd>
indicates the right hand mouse button.  The functions available provide
a way to construct commands automatically (<code>pg-goals-button-action</code>)
and to inspect identifiers (<code>pg-identifier-under-mouse-query</code>) as
the Info toolbar button does.
</p>
<p>Proof-by-pointing is a cute idea.  It lets you automatically construct
parts of a proof by clicking.  You can ask the proof assistant to try to
do a step in the proof, based on where you click.  If you don&rsquo;t like the
command which was inserted into the script, you can comment use the
control key with the right button to undo the step and delete it from
your script (<code>proof-undo-and-delete-last-successful-command</code>).
</p>
<p>Proof-by-pointing may construct several commands in one go.  These are
sent back to the proof assistant altogether and appear as a single step
in the proof script.  However, if the proof is later replayed (without
using PBP), the proof-by-pointing constructions will be considered as
separate proof commands, as usual.
</p>
<p>The main function for proof-by-pointing is <code>pg-goals-button-action</code>.
</p>
<dl>
<dt><a name="index-pg_002dgoals_002dbutton_002daction"></a>Command: <strong>pg-goals-button-action</strong> <em>event</em></dt>
<dd><p>Construct a proof-by-pointing command based on the mouse-click <var>event</var>.<br>
This function should be bound to a mouse button in the Proof General
goals buffer.
</p>
<p>The <var>event</var> is used to find the smallest subterm around a point.  A
position code for the subterm is sent to the proof assistant, to ask
it to construct an appropriate proof command.  The command which is
constructed will be inserted at the end of the locked region in the
proof script buffer, and immediately sent back to the proof assistant.
If it succeeds, the locked region will be extended to cover the
proof-by-pointing command, just as for any proof command the
user types by hand.
</p></dd></dl>

<p>Proof-by-pointing uses markup describing the term structure of the
concrete syntax output by the proof assistant.  This markup is useful in
itself: it allows you to explore the structure of a term using the mouse
(the smallest subexpression that the mouse is over is highlighted), and
easily copy subterms from the output to a proof script.
</p>




<dl>
<dt><a name="index-pg_002didentifier_002dunder_002dmouse_002dquery"></a>Command: <strong>pg-identifier-under-mouse-query</strong> <em>event</em></dt>
<dd><p>Query the prover about the identifier near mouse click <var>event</var>.
</p></dd></dl>



<hr>
<div class="header">
<p>
Up: <a href="#Subterm-Activation-and-Proof-by-Pointing" accesskey="u" rel="up">Subterm Activation and Proof by Pointing</a> &nbsp; [<a href="Concept-Index.html#SEC_Contents" title="Table of contents" rel="contents">Contents</a>][<a href="Function-Index.html#Function-Index" title="Index" rel="index">Index</a>]</p>
</div>



</body>
</html>
proofgeneral-doc 4.3~pre130510-1.1 / usr / share / doc / proofgeneral-doc / html / Subterm-Activation-and-Proof-by-Pointing.html
