Review #2

doc/sphinx/addendum/parallel-proof-processing.rst

@@ -66,11 +66,11 @@ to modify the proof script accordingly.
 Proof blocks and error resilience
 --------------------------------------
 
-Coq 8.6 introduced a mechanism for error resilience: in interactive
+In interactive
 mode Coq is able to completely check a document containing errors
 instead of bailing out at the first failure.
 
-Two kind of errors are supported: errors occurring in
+Two kind of errors are handled: errors occurring in
 commands and errors occurring in proofs.
 
 To properly recover from a failing tactic, Coq needs to recognize the
@@ -112,21 +112,21 @@ Valid proof block types are: “curly”, “par”, “indent”, and “bullet
 Interactive mode
 ---------------------
 
-.. todo: How about PG and coqtail?  Trim this back a bit, some of the info is now
-   in the CoqIDE chapter.
+.. todo: How about PG and coqtail?
 
 CoqIDE and vsCoq support asynchronous proof processing.
 
-When CoqIDE is started, two Coq processes are created. The master one
+When CoqIDE is started and async mode is enabled, two or more Coq processes
+are created. The master one
 follows the user, giving feedback as soon as possible by skipping
-proofs, which are delegated to the worker process. The worker process,
-whose state can be seen by clicking on the button in the lower right
-corner of the main CoqIDE window, asynchronously processes the proofs.
-If a proof contains an error, it is reported in red in the label of
+proofs, which are delegated to the worker processes. The worker processes
+asynchronously processes the proofs.  The *Jobs panel* in the main CoqIDE
+window shows the status of each worker process.
+If a proof contains an error, it's reported in red in the label of
 the very same button, that can also be used to see the list of errors
 and jump to the corresponding line.
 
-If a proof is processed asynchronously the corresponding Qed command
+If a proof is processed asynchronously the corresponding :cmd:`Qed` command
 is colored using a lighter color than usual. This signals that the
 proof has been delegated to a worker process (or will be processed
 lazily if the ``-async-proofs lazy`` option is used). Once finished, the

doc/sphinx/practical-tools/coqide.rst

@@ -49,8 +49,11 @@ launch your favorite text editor on the current buffer, using the
 *Edit/External Editor* menu. When you're done editing, you must currently must
 reopen the file to see your changes.  Also note:
 
-- Undo is also available as Ctrl-Z.  Redo is Ctrl-Shift-Z.
-- Select all is Ctrl-A.
+- Undo is also available as Ctrl-Z (Command-Z on macOS).  Redo is Ctrl-Shift-Z
+  (Shift-Command-Z on macOS).
+- Select all is Ctrl-A (Command-A on macOS).
+- Ctrl-Delete deletes a word of text after the cursor
+- Ctrl-Backspace deletes a word of text before the cursor
 - Commenting and uncommenting the current line or selected text is available in
   the *Tools* menu.  If some text is selected, exactly that text is commented out;
   otherwise the line containing the cursor is commented out.  To uncomment, position
@@ -110,9 +113,15 @@ everything after that point is undone.  Unlike `coqtop`, you should not use
 
 .. todo drop next para, mention left and right with search
 
-There are other buttons on the CoqIDE toolbar: a button to save the running
-buffer; a button to close the current buffer (an "X"); buttons to switch among
-buffers (left and right arrows); and a "gears" button.
+The other buttons on the toolbar do the following:
+
+- Save the current buffer (down arrow icon)
+- Close the current buffer ("X" icon)
+- Fully check the document (gears icon) - for async mode
+- Previous occurrence (left arrow icon) - find the previous occurrence
+  of the current word (The current word is determined by the cursor position.)
+- Next occurrence (right arrow icon) - find the next occurrence
+  of the current word
 
 .. _asyncmode:
 
@@ -168,7 +177,7 @@ The image above shows the result after selecting
 ``Nat.mul`` in the bottom line of the script panel, then choosing ``Print``
 from the ``Queries`` menu.
 
-.. todo PR: should names of menus be *Menu* or `Menu` or ??  not consistent
+.. todo: should names of menus be *Menu* or `Menu` or ??  not consistent
 
 
 Compilation
@@ -184,6 +193,9 @@ The `Compile` menu offers direct commands to:
 Customizations
 --------------
 
+Preferences
+~~~~~~~~~~~
+
 You may customize your environment with the *Preferences* dialog, which
 *Edit/Preferences* on the menu. There are several sections:
 
@@ -227,14 +239,55 @@ Notice that these settings are saved in the file ``coqiderc`` in the
 is the value of ``$XDG_CONFIG_HOME`` if this environment variable is
 set and which otherwise is ``$HOME/.config/``.
 
+Key bindings
+~~~~~~~~~~~~
+
+Each menu item in the GUI shows its key binding, if one has been defined,
+on the right-hand side.  Typing the key binding is equivalent to selecting
+the associated item from the menu.
 A GTK+ accelerator keymap is saved under the name ``coqide.keys`` in
-the same ``coq`` subdirectory of the user configuration directory. It
-is not recommended to edit this file manually: to modify a given menu
-shortcut, go to the corresponding menu item without releasing the
-mouse button, press the key you want for the new shortcut, and release
-the mouse button afterwards. If your system does not allow it, you may
-still edit this configuration file by hand, but this is more involved.
+the ``coq`` subdirectory of the user configuration directory,
+e.g. in `~/.config/coq/` on Linux and `C:\Users\<USERNAME>\AppData\Local\coq`
+on Windows. On some systems (not Linux or Windows),
+you can modify the key binding ("accelerator") for a menu entry by
+going to the corresponding menu item without releasing the
+mouse button, pressing the keys you want for the new binding and then releasing
+the mouse button.
+
+Alternatively, you can edit the file directly.  Make sure there are no
+CoqIDE processes running while you edit the file.  (CoqIDE creates or
+overwrites the file when it terminates, which may reorder the lines).
+
+The file contains lines such as:
+
+   ::
+
+     ; (gtk_accel_path "<Actions>/Queries/About" "<Primary><Shift>a")
+     ; (gtk_accel_path "<Actions>/Export/Export to" "")
+     (gtk_accel_path "<Actions>/Edit/Find Next" "F4")
+
+The first line corresponds to the menu item for the Queries/About menu item,
+which was bound by default to Shift-Ctrl-A.  "<Primary>" indicates Ctrl.
+The second line is for a menu item that has no key binding.
+
+Lines that begin with semicolons are comments create by CoqIDE.  CoqIDE uses
+the default binding
+for these items.  To change a key binding, remove the semicolon and set the third item
+in the list as desired, such as in the third line.  Avoid assigning the same binding
+to multiple items.
+
+If the same menu item name appears on multiple lines in the file, the value from the
+last line is used.  This is convenient for copying a group of changes from elsewhere--just
+insert the changes at the end of the file.  The next time CoqIDE terminates, it will
+usually reorder the items.
+
+Some menu entries can be changed as a group from the Edit/Preferences/Shortcuts panel.
+Key bindings that don't appear in the file such as Ctrl-A (Select All) can't be
+changed with this mechanism.
+
+.. todo: list common rebindings?
 
+.. todo: microPG mode?
 
 Using Unicode symbols
 ---------------------
@@ -261,10 +314,9 @@ mathematical symbols ∀ and ∃, you may define:
      (at level 200, x binder, y binder, right associativity)
      : type_scope.
 
-There exists a small set of such notations already defined, in the
-file `utf8.v` of Coq library, so you may enable them just by
-``Require Import Unicode.Utf8`` inside CoqIDE, or equivalently,
-by starting CoqIDE with ``coqide -l utf8``.
+A small set of such notations are already defined in the Coq library
+which you can enable with ``Require Import Unicode.Utf8`` inside CoqIDE,
+or equivalently, by starting CoqIDE with ``coqide -l utf8``.
 
 However, there are some issues when using such Unicode symbols: you of
 course need to use a character font which supports them. In the Fonts