diff options
Diffstat (limited to 'doc/sphinx/practical-tools/coqide.rst')
| -rw-r--r-- | doc/sphinx/practical-tools/coqide.rst | 20 |
1 files changed, 9 insertions, 11 deletions
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 1fcfc665b..f9903e610 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -10,7 +10,7 @@ used as a user-friendly replacement to `coqtop`. Its main purpose is to allow the user to navigate forward and backward into a Coq vernacular file, executing corresponding commands or undoing them respectively. -CoqIDE is run by typing the command `coqide` on the command line. +|CoqIDE| is run by typing the command `coqide` on the command line. Without argument, the main screen is displayed with an “unnamed buffer”, and with a file name as argument, another buffer displaying the contents of that file. Additionally, `coqide` accepts the same @@ -43,7 +43,7 @@ is the one where Coq commands are currently executed. Buffers may be edited as in any text editor, and classical basic editing commands (Copy/Paste, …) are available in the *Edit* menu. -CoqIDE offers only basic editing commands, so if you need more complex +|CoqIDE| offers only basic editing commands, so if you need more complex editing commands, you may launch your favorite text editor on the current buffer, using the *Edit/External Editor* menu. @@ -75,7 +75,7 @@ There are two additional buttons for navigation within the running buffer. The "down" button with a line goes directly to the end; the "up" button with a line goes back to the beginning. The handling of errors when using the go-to-the-end button depends on whether |Coq| is running in asynchronous mode or not (see -Chapter :ref:`Asyncprocessing`). If it is not running in that mode, execution +Chapter :ref:`asynchronousandparallelproofprocessing`). If it is not running in that mode, execution stops as soon as an error is found. Otherwise, execution continues, and the error is marked with an underline in the error foreground color, with a background in the error background color (pink by default). The same @@ -86,14 +86,14 @@ If you ever try to execute a command which happens to run during a long time, and would like to abort it before its termination, you may use the interrupt button (the white cross on a red circle). -There are other buttons on the CoqIDE toolbar: a button to save the running +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); an "information" button; and a "gears" button. -The "information" button is described in Section :ref:`sec:trytactics`. +The "information" button is described in Section :ref:`try-tactics-automatically`. The "gears" button submits proof terms to the |Coq| kernel for type-checking. -When |Coq| uses asynchronous processing (see Chapter :ref:`Asyncprocessing`), +When |Coq| uses asynchronous processing (see Chapter :ref:`asynchronousandparallelproofprocessing`), proofs may have been completed without kernel-checking of generated proof terms. The presence of unchecked proof terms is indicated by ``Qed`` statements that have a subdued *being-processed* color (light blue by default), rather than the @@ -150,18 +150,16 @@ arguments. Queries ------------ -.. _coqide_queryselected: - .. image:: ../_static/coqide-queries.png :alt: |CoqIDE| queries We call *query* any vernacular command that does not change the current state, such as ``Check``, ``Search``, etc. To run such commands interactively, without -writing them in scripts, CoqIDE offers a *query pane*. The query pane can be +writing them in scripts, |CoqIDE| offers a *query pane*. The query pane can be displayed on demand by using the ``View`` menu, or using the shortcut ``F1``. Queries can also be performed by selecting a particular phrase, then choosing an item from the ``Queries`` menu. The response then appears in the message window. -Figure :ref:`fig:queryselected` shows the result after selecting of the phrase +The image above shows the result after selecting of the phrase ``Nat.mul`` in the script window, and choosing ``Print`` from the ``Queries`` menu. @@ -221,7 +219,7 @@ still edit this configuration file by hand, but this is more involved. Using Unicode symbols -------------------------- -CoqIDE is based on GTK+ and inherits from it support for Unicode in +|CoqIDE| is based on GTK+ and inherits from it support for Unicode in its text windows. Consequently a large set of symbols is available for notations. |