diff options
| author | Hugo Herbelin | 2019-04-27 12:56:30 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-04-30 12:56:55 +0200 |
| commit | 7d3e6fefd7dab20c433fb7ae1baec5fa3ff2f0d7 (patch) | |
| tree | b6c2763c0dc917e3bcd47a1a47950c872aed6153 /doc | |
| parent | bae9b53c58d995a0cce404c279c37206e5418d2f (diff) | |
CoqIDE: updating documentation of the Preference windows.
In particular, we explicitly mention the existence of an Emacs mode.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/practical-tools/coqide.rst | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 97d86943fb..d3d75dddd8 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -181,7 +181,14 @@ presented as a notebook. The first section is for selecting the text font used for scripts, goal and message windows. -The second section is devoted to file management: you may configure +The second and third sections are for controlling colors and style. + +The fourth section is for customizing the editor. It includes in +particular the ability to activate an Emacs mode named +micro-Proof-General (use the Help menu to know more about the +available bindings). + +The next section is devoted to file management: you may configure automatic saving of files, by periodically saving the contents into files named `#f#` for each opened file `f`. You may also activate the *revert* feature: in case a opened file is modified on the disk by a |