This commit is contained in:
Basile Burg 2017-01-26 00:47:26 +01:00
parent 3273f26bb5
commit 9a1dcffb54
No known key found for this signature in database
GPG Key ID: 1868039F415CB8CF
4 changed files with 20 additions and 0 deletions

Binary file not shown.

After

Width:  |  Height:  |  Size: 58 KiB

View File

@ -39,6 +39,7 @@ _Full description of Coedit options. May redirect to a specific widget page._
* [Code metrics](options_code_metrics) * [Code metrics](options_code_metrics)
* [Compiler paths](options_compilers_paths) * [Compiler paths](options_compilers_paths)
* [DUB build](options_dub_build) * [DUB build](options_dub_build)
* [Editor pages](options_editor_pages)
* [Messages](widgets_messages) * [Messages](widgets_messages)
* [Mini explorer](widgets_mini_explorer) * [Mini explorer](widgets_mini_explorer)
* [Runnable modules](features_runnables) * [Runnable modules](features_runnables)

View File

@ -2,6 +2,8 @@
title: Widgets - application options title: Widgets - application options
--- ---
#### Application
{% include xstyle.css %} {% include xstyle.css %}
The page exposes unsorted options. In the future some of them might be moved to their own category. The page exposes unsorted options. In the future some of them might be moved to their own category.

View File

@ -0,0 +1,17 @@
---
title: Options - DUB build
---
#### Editor pages
This category exposes the options of the page control used to host the code editors.
![](img/options_editor_pages.png)
- **detectModuleName**: If sets then a module is lexed in order to find its module name. Can be deactivated on slowest machines.
- **moveLeft**: Sets the shortcut used to move a page to left.
- **moveRight**: Sets the shortcut used to move a page to right.
- **nextPage**: Sets the shortcut used to select the next page.
- **pageButtons**: Defines which buttons are visible in the toolbar.
- **pagesOptions**: Miscellaneous options. __poPageHistory__ means the creation order is saved and used to select a particular page when another is closed.
- **previousPage**: Sets the shortcut used to select the previous page.