Update documenation of mouse bindings.

Clean up documentation of holes a bit.
Remove some dead comments.

1 files changed, 79 insertions, 77 deletions

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 6ec9d037..477b33ce 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -1839,21 +1839,23 @@ Enabling
 Proof General -> Quick Options -> Processing -> Process Automatically
 @end lisp
 
-Causes Proof General to start processing text when Emacs is idle for
-a while.  You can choose either to send just the next command, or
-the whole buffer.  See 
+Causes Proof General to start processing text when Emacs is idle for a
+while.  You can choose either to send just the next command beyond the
+point, or the whole buffer.  See
 @lisp
 Proof General -> Quick Options -> Processing -> Automatic Processing Mode
 @end lisp
 for the choices.
 
-The text will be sent in a fast loop that processes more
-quickly than @kbd{C-c C-b} (i.e., @code{proof-process-buffer},
-the down toolbar button), but ignores user input and doesn't update
-the display.  
+The text will be sent in a fast loop that processes more quickly than
+@kbd{C-c C-b} (i.e., @code{proof-process-buffer}, the down toolbar
+button), but ignores user input and doesn't update the display.  But the
+feature tries to be non-intrusive to the user: if you start to type
+something or use the mouse, the fast loop will be interrupted and revert
+to a slower interactive loop with display updates.
 
-This feature tries to be non-intrusive to the user: if you start to type
-something or use the mouse, the fast loop will be interrupted.
+In the check next command mode, the successfully checked region will
+briefly flash up as green to indicate it is okay.
 
 You can use @kbd{C-c C-.} (@code{proof-goto-end-of-locked}) to find
 out where processing got to, as usual.  Text is only sent if the last
@@ -2855,10 +2857,11 @@ Add completions from the current tags table.
 This chapter describes what you can do from inside the goals buffer,
 providing support for these features exists for your proof assistant.
 
-As of Proof General 4.0, this support only exists for LEGO.  
-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!
+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!
 
 @menu
 * Goals buffer commands::
@@ -2868,36 +2871,43 @@ proof assistant to provide it!
 @section Goals buffer commands
 
 When you are developing a proof, the input focus (Emacs cursor) is
-usually on the script buffer.  Therefore Proof General binds mouse
+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.
 
 The mouse bindings are these:
 
 @table @kbd
-@c @item button2
-@c FIXME: @code{pg-goals-button-action}
-@item C-M-mouse-3
+@item mouse-1
+@code{pg-goals-button-action}
+@item C-mouse-3
 @code{proof-undo-and-delete-last-successful-command}
-@item mouse-3
-@code{pg-goals-yank-subterm}
+@c @item mouse-3
+@c @code{pg-goals-yank-subterm}
+@item C-S-mouse-1
+@code{pg-identifier-under-mouse-query}
 @end table
 
-Where @kbd{button2} indicates the middle mouse button, and @kbd{button3}
-indicates the right hand mouse button.
+Where @kbd{mouse-1} indicates the left mouse button, and @kbd{mouse-3}
+indicates the right hand mouse button.  The functions available provide
+a way to construct commands automatically (@code{pg-goals-button-action})
+and to inspect identifiers (@code{pg-identifier-under-mouse-query}) as
+the Info toolbar button does.
 
-The idea is that you can automatically construct parts of a proof by
-clicking.  Using the middle mouse button asks the proof assistant to try
-to do a step in the proof, based on where you click.  If you don't like
-the command which was inserted into the script, you can use the control
-key with the middle button to undo the step, and delete it from your
-script.
+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'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}).
 
-Note that 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.
+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.
+
+The main function for proof-by-pointing is @code{pg-goals-button-action}.
 
 @c TEXI FIXME DOCSTRING MAGIC: pg-goals-button-action
 @deffn Command pg-goals-button-action event
@@ -2921,25 +2931,29 @@ 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.
 
-The right-hand mouse button provides this convenient way to copy
-subterms from the goals buffer, using the function
-@code{pg-goals-yank-subterm}.
+@c The right-hand mouse button provides this convenient way to copy
+@c subterms from the goals buffer, using the function
+@c @code{pg-goals-yank-subterm}.
 
 @c TEXI FIXME DOCSTRING MAGIC: pg-goals-yank-subterm
-@deffn Command pg-goals-yank-subterm event
-Copy the subterm indicated by the mouse-click @var{event}.@*
-This function should be bound to a mouse button in the Proof General
-goals buffer.
-
-The @var{event} is used to find the smallest subterm around a point.  The
-subterm is copied to the @samp{@code{kill-ring}}, and immediately yanked (copied)
-into the current buffer at the current cursor position.
+@c @deffn Command pg-goals-yank-subterm event
+@c Copy the subterm indicated by the mouse-click @var{event}.@*
+@c This function should be bound to a mouse button in the Proof General
+@c goals buffer.
+
+@c The @var{event} is used to find the smallest subterm around a point.  The
+@c subterm is copied to the @samp{@code{kill-ring}}, and immediately yanked (copied)
+@c into the current buffer at the current cursor position.
+
+@c In case the current buffer is the goals buffer itself, the yank
+@c is not performed.  Then the subterm can be retrieved later by an
+@c explicit yank.
+@c @end deffn
 
-In case the current buffer is the goals buffer itself, the yank
-is not performed.  Then the subterm can be retrieved later by an
-explicit yank.
+@c TEXI DOCSTRING MAGIC: pg-identifier-under-mouse-query
+@deffn Command pg-identifier-under-mouse-query event
+Query the prover about the identifier near mouse click @var{event}.
 @end deffn
-
 @c Proof General expects to parse
 @c term-structure annotations on the output syntax of the prover.
 @c It uses these to construct a message to the prover indicating
@@ -4019,24 +4033,26 @@ recording it in the script.
 @node Holes feature
 @section Holes feature
 
-@emph{Holes} are an experimental feature for complex expression
-editing. It is inspired from other tools, like Pcoq
-(@uref{http://www-sop.inria.fr/lemme/pcoq/index.html}). The principle is
-simple, holes are pieces of text that can be "filled" by different
-means. The new coq command insertion menu system makes use of the holes
-system. Almost all holes operations are available in the Coq/holes menu.
+@emph{Holes} are an experimental feature for complex expression editing
+by filling in templates. It is inspired from other tools, like Pcoq
+(@uref{http://www-sop.inria.fr/lemme/pcoq/index.html}).  The principle
+is simple, holes are pieces of text that can be "filled" by various
+means. The Coq command insertion menu system makes use of the holes
+system.  Almost all holes operations are available in the Holes menu.
 
-@b{Note:} Holes make use of the Emacs abbreviation mechanism, it will
+@b{Notes:} Holes make use of the Emacs abbreviation mechanism, it will
 work without problem if you don't have an abbrev table defined for Coq
-in your config files (@code{C-h v abbrev-file-name} to see the name of
-the abbreviation file). If you already have such a table it won't be
-automatically overwritten (so that you keep your own abbreviations). But
-you must read the abbrev file given in PG/Coq sources to be able to use
-the command insertion menus. You can do the following to merge your
-abbreviations with ProofGeneral's abbreviations: @code{M-x
-read-abbrev-file}, then select the file named @code{coq-abbrev.el} in
-the ProofGeneral/coq directory. At Emacs exit you will be asked if you
-want to save abbrevs; answer yes.
+in your config files.  Use @code{C-h v abbrev-file-name} to see the name
+of the abbreviation file. 
+
+If you already have such a table it won't be automatically overwritten
+(so that you keep your own abbreviations).  But you must read the abbrev
+file given in the Proof General sources to be able to use the command
+insertion menus.  You can do the following to merge your abbreviations
+with ProofGeneral's abbreviations: @code{M-x read-abbrev-file}, then
+select the file named @code{coq-abbrev.el} in the
+@code{ProofGeneral/coq} directory. At Emacs exit you will be asked if
+you want to save abbrevs; answer yes.
 
 
 @c =================================================================
@@ -4952,25 +4968,11 @@ Mode (for multiple modes in one buffer) are bundled with Proof General.
 An experimental Unicode Tokens package has been added which will replace
 X-Symbol.
 
-@c The display handling functions have been improved to be more user
-@c friendly and the display in multiple-window mode is trimmed to
-@c allow more text space for display.  
-
-@c Proof General 3.7 is available in RPM package format which includes
-@c pre-compiled code for GNU Emacs and 
-@c desktop integration on freedesktop.org compliant desktops (including,
-@c for example, many recent Linux distributions).
-
-@c Other stuff pending:
-@c Support for *thms* buffer??
-
 See the @file{CHANGES} file in the distribution for more complete
 details of changes since version 3.5, and the appendix
 @ref{History of Proof General} for old news.
 
 
-
-
 @node Function Index
 @unnumbered Function and Command Index
 @printindex fn