From ea789fb00cecbb720702940d4752e991bbcc2054 Mon Sep 17 00:00:00 2001 From: charguer Date: Tue, 13 Nov 2018 11:04:00 +0100 Subject: documentation for unicode bindings --- doc/sphinx/practical-tools/coqide.rst | 76 +++++++++++++++++++++++------------ 1 file changed, 51 insertions(+), 25 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 8b7fe20191..ab7fe2ac08 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -218,7 +218,8 @@ Using Unicode symbols |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. +notations. Furthermore, |CoqIDE| conveniently provides a simple way to +input Unicode characters. Displaying Unicode symbols @@ -254,37 +255,62 @@ use antialiased fonts or not, by setting the environment variable Defining an input method for non-ASCII symbols ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -To input a Unicode symbol, a general method provided by GTK+ is to -simultaneously press the Control, Shift and “u” keys, release, then -type the hexadecimal code of the symbol required, for example `2200` -for the ∀ symbol. A list of symbol codes is available at -`http://www.unicode.org`. +CoqIDE supports a builtin mechanism to input non-ASCII symbols. +For example, to input ``π``, it suffices to type ``\pi`` then press the +combination of key ``Shift+Space`` (default key binding). Often, it +suffices to type a prefix of the latex token, e.g. typing ``\p`` +then ``Shift+Space`` suffices to insert a ``π``. -An alternative method which does not require to know the hexadecimal -code of the character is to use an Input Method Editor. On POSIX -systems (Linux distributions, BSD variants and MacOS X), you can -use `uim` version 1.6 or later which provides a LaTeX-style input -method. +For several symbols, ASCII art is also recognized, e.g. ``\->`` for a +right arrow, or ``\>=`` for a greater than or equal sign. -To configure uim, execute uim-pref-gtk as your regular user. In the -"Global Settings" group set the default Input Method to "ELatin" -(don’t forget to tick the checkbox "Specify default IM"). In the -"ELatin" group set the layout to "TeX", and remember the content of -the "[ELatin] on" field (by default Control-\\). You can now execute -|CoqIDE| with the following commands (assuming you use a Bourne-style -shell): +A larger number of latex tokens are supported by default. The full list +is available here: +https://github.com/coq/coq/blob/master/ide/default_bindings_src.ml -:: +Custom bindings may be added, as explained further on. - $ export GTK_IM_MODULE=uim - $ coqide +Remark: it remains possible to input non-ASCII symbols using system-wide +approaches independent of |CoqIDE|. -Activate the ELatin Input Method with Control-\\, then type the -sequence `\\Gamma`. You will see the sequence being replaced by Γ as -soon as you type the second "a". +Adding custom bindings +~~~~~~~~~~~~~~~~~~~~~~ + +To extend the default set of bindings, create a file named `coqide.bindings` +and place it in the same folder as `coqide.keys`. On Linux, this would be +the folder ``~/.config/coq``. The file `coqide.bindings` should contain one +binding per line, in the form ``\key value``, followed by an optional priority +integer. (The key and value should not contain any space character.) +Here is an example configuration file: + +``` +\par || +\pi π 1 +\le ≤ 1 +\lambda λ 2 +\lambdas λs +``` + +Above, the priority number 1 on ``\pi`` indicates that the prefix ``\p`` +should resolve to ``\pi``, and not to something else (e.g. ``\par``). +Similarly, the above settings ensure than ``\l`` resolves to ``\le``, +and that ``\la`` resolves to ``\lambda``. + +It can be useful to work with per-project binding files. For this purpose +|CoqIDE| accepts a command line argument of the form +``-unicode-bindings file1,file2,...,fileN``. +Each of the file tokens provided may consists of one of: + + - a path to a custom bindings file, + - the token ``default``, which resolves to the default bindings file, + - the token ``local``, which resolves to the `coqide.bindings` file + stored in the user configuration directory. + +Remark: if two bindings for a same token both have the same priority value +(or both have no priority value set), then the binding considered is the +one from the file that comes first on the command line. -.. _character-encoding-saved-files: Character encoding for saved files ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -- cgit v1.2.3 From 8d93141a931a4007feb8f28df2cd61c7b1c1b61e Mon Sep 17 00:00:00 2001 From: charguer Date: Wed, 14 Nov 2018 12:53:38 +0100 Subject: final polishing for coqide bindings --- doc/sphinx/practical-tools/coqide.rst | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'doc/sphinx') diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index ab7fe2ac08..44955412ce 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -307,6 +307,11 @@ Each of the file tokens provided may consists of one of: - the token ``local``, which resolves to the `coqide.bindings` file stored in the user configuration directory. +Remark: if a filename other than the first one includes a "~" to refer +to the home directory, it won't be expanded properly. To work around that +issue, one should not use comas but instead repeat the flag, in the form: +``-unicode-bindings file1 .. -unicode-bindings fileN``. + Remark: if two bindings for a same token both have the same priority value (or both have no priority value set), then the binding considered is the one from the file that comes first on the command line. -- cgit v1.2.3 From 8ca754b1737adb4700609d43ef434a6d06c54ffe Mon Sep 17 00:00:00 2001 From: charguer Date: Wed, 28 Nov 2018 11:23:31 +0100 Subject: polishing documentation for coqide bindings, following @Zimmi48 comments --- doc/sphinx/practical-tools/coqide.rst | 36 +++++++++++++++++++++-------------- 1 file changed, 22 insertions(+), 14 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 44955412ce..6f48daf208 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -223,7 +223,7 @@ input Unicode characters. Displaying Unicode symbols -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +~~~~~~~~~~~~~~~~~~~~~~~~~~ You just need to define suitable notations as described in the chapter :ref:`syntaxextensionsandinterpretationscopes`. For example, to use the @@ -252,8 +252,8 @@ use antialiased fonts or not, by setting the environment variable `GDK_USE_XFT` to 1 or 0 respectively. -Defining an input method for non-ASCII symbols -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Bindings for input of Unicode symbols +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ CoqIDE supports a builtin mechanism to input non-ASCII symbols. For example, to input ``π``, it suffices to type ``\pi`` then press the @@ -270,15 +270,17 @@ https://github.com/coq/coq/blob/master/ide/default_bindings_src.ml Custom bindings may be added, as explained further on. -Remark: it remains possible to input non-ASCII symbols using system-wide -approaches independent of |CoqIDE|. +.. note:: + + It remains possible to input non-ASCII symbols using system-wide + approaches independent of |CoqIDE|. Adding custom bindings ~~~~~~~~~~~~~~~~~~~~~~ -To extend the default set of bindings, create a file named `coqide.bindings` -and place it in the same folder as `coqide.keys`. On Linux, this would be +To extend the default set of bindings, create a file named ``coqide.bindings`` +and place it in the same folder as ``coqide.keys``. On Linux, this would be the folder ``~/.config/coq``. The file `coqide.bindings` should contain one binding per line, in the form ``\key value``, followed by an optional priority integer. (The key and value should not contain any space character.) @@ -307,15 +309,21 @@ Each of the file tokens provided may consists of one of: - the token ``local``, which resolves to the `coqide.bindings` file stored in the user configuration directory. -Remark: if a filename other than the first one includes a "~" to refer -to the home directory, it won't be expanded properly. To work around that -issue, one should not use comas but instead repeat the flag, in the form: -``-unicode-bindings file1 .. -unicode-bindings fileN``. +.. remark:: + + If a filename other than the first one includes a "~" to refer + to the home directory, it won't be expanded properly. To work around that + issue, one should not use comas but instead repeat the flag, in the form: + ``-unicode-bindings file1 .. -unicode-bindings fileN``. + +.. note:: + + If two bindings for a same token both have the same priority value + (or both have no priority value set), then the binding considered is + the one from the file that comes first on the command line. -Remark: if two bindings for a same token both have the same priority value -(or both have no priority value set), then the binding considered is the -one from the file that comes first on the command line. +.. _character-encoding-saved-files: Character encoding for saved files ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -- cgit v1.2.3 From 67847789beede10420ab631d5d0f9c2cfe9db72d Mon Sep 17 00:00:00 2001 From: charguer Date: Mon, 11 Feb 2019 14:47:44 +0100 Subject: fix documentation issues, and add entry to change log --- doc/sphinx/practical-tools/coqide.rst | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 6f48daf208..97d86943fb 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -284,15 +284,18 @@ and place it in the same folder as ``coqide.keys``. On Linux, this would be the folder ``~/.config/coq``. The file `coqide.bindings` should contain one binding per line, in the form ``\key value``, followed by an optional priority integer. (The key and value should not contain any space character.) -Here is an example configuration file: -``` -\par || -\pi π 1 -\le ≤ 1 -\lambda λ 2 -\lambdas λs -``` +.. example:: + + Here is an example configuration file: + + :: + + \par || + \pi π 1 + \le ≤ 1 + \lambda λ 2 + \lambdas λs Above, the priority number 1 on ``\pi`` indicates that the prefix ``\p`` should resolve to ``\pi``, and not to something else (e.g. ``\par``). @@ -309,7 +312,7 @@ Each of the file tokens provided may consists of one of: - the token ``local``, which resolves to the `coqide.bindings` file stored in the user configuration directory. -.. remark:: +.. warning:: If a filename other than the first one includes a "~" to refer to the home directory, it won't be expanded properly. To work around that -- cgit v1.2.3