diff options
Diffstat (limited to 'ide/FAQ')
-rw-r--r-- | ide/FAQ | 25 |
1 files changed, 6 insertions, 19 deletions
@@ -6,8 +6,8 @@ R0: A powerfull graphical interface for Coq. See http://coq.inria.fr. for more i Q1) How to enable Emacs keybindings? R1: Insert gtk-key-theme-name = "Emacs" - in your "coqide-gtk2rc" file. It should be in $XDG_CONFIG_DIRS/coq dir. - This is done by default. +in your gtkrc file. The location of this file is system-dependent. If you're running +Gnome, you may use the graphical configuration tools. Q2) How to enable antialiased fonts? R2) Set the GDK_USE_XFT variable to 1. This is by default with Gtk >= 2.2. @@ -34,27 +34,14 @@ R5)-First solution : type "<CONTROL><SHIFT>2200" to enter a forall in the script 2200 is the hexadecimal code for forall in unicode charts and is encoded as "∀" in UTF-8. 2203 is for exists. See http://www.unicode.org for more codes. --Second solution : rebind "<AltGr>a" to forall and "<AltGr>e" to exists. - Under X11, you need to use something like - xmodmap -e "keycode 24 = a A F13 F13" - xmodmap -e "keycode 26 = e E F14 F14" - and then to add - bind "F13" {"insert-at-cursor" ("∀")} - bind "F14" {"insert-at-cursor" ("∃")} - to your "binding "text"" section in coqiderc-gtk2rc. - The strange ("∀") argument is the UTF-8 encoding for - 0x2200. - You can compute these encodings using the lablgtk2 toplevel with - Glib.Utf8.from_unichar 0x2200;; - Further symbols can be bound on higher Fxx keys or on even on other keys you - do not need . +-Second solution : Use an input method editor, such as SCIM or iBus. The latter offers +a module for LaTeX-like inputting. Q6) How to customize the shortcuts for menus? R6) Two solutions are offered: - Edit $XDG_CONFIG_HOME/coq/coqide.keys by hand or - - Add "gtk-can-change-accels = 1" in your coqide-gtk2rc file. Then - from CoqIde, you may select a menu entry and press the desired - shortcut. + - If your system allows it, from CoqIde, you may select a menu entry and press the + desired shortcut. Q7) What encoding should I use? What is this \x{iiii} in my file? R7) The encoding option is related to the way files are saved. |