diff options
| author |  monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-10 19:16:28 +0000 |
|---|---|---|
| committer | monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-10 19:16:28 +0000 |
| commit | 64f0fe542c3871d76eddf520b307ecd0a0634e89 (patch) | |
| tree | b304e651555b45b708a5d954c1c65adec5be988a /ide | |
| parent | fbfc1ff19252520da7700341ba67a75b2e113746 (diff) | |
coqide: maj des bindings
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3752 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/.coqiderc | 3 | ||||
| -rw-r--r-- | ide/FAQ | 23 | ||||
| -rw-r--r-- | ide/coqide.ml | 2 |
3 files changed, 25 insertions, 3 deletions
diff --git a/ide/.coqiderc b/ide/.coqiderc index 65a6085d9..89967ce36 100644 --- a/ide/.coqiderc +++ b/ide/.coqiderc @@ -4,6 +4,7 @@ binding "text" { "cut-clipboard" () } bind "<ctrl>x" { } + bind "F13" {"insert-at-cursor" ("∀")} } class "GtkTextView" binding "text" @@ -25,5 +26,3 @@ font_name = "Serif 10" class "GtkLabel" style "menu" gtk-key-theme-name = "Emacs" -gtk-can-change-accels = 1 - @@ -17,3 +17,26 @@ R2) Insert Q3) How to enable antialiased fonts? R3) Set the GDK_USE_XFT variable to 1. + +Q4) How can use Forall and Exists pretty symbols ? +R4) Thanks to the Notation features in Coq, you just need to paste these + lines in your Coq Buffer : +====================================================================== +Notation "∀ x : t | P" := (x:t)P (at level 1, x,t,P at level 10). +Notation "~ x : t | P" := (EXT x:t|P) (at level 1, x,t,P at level 10). +====================================================================== +Then you need an input method for these symbols. +-First solution : type "<CONTROL>2200" to enter a forall. 2200 is the + hexadecimal code for forall in unicode charts. + 2203 is for exists. See http://www.unicode.org for more. + +-Second solution : rebind "<AltGr>a" to forall. Under X11, you need to + use + xmodmap -e "keycode 24 = a A F13 F13" + and then to add + bind "F13" {"insert-at-cursor" ("∀")} + to your "binding "text"" section in .coqiderc. + The strange ("∀") argument is the UTF-8 encoding for + 0x2200. It is computed by lablgtk2 by + Glib.Utf8.from_unichar 0x2200;; + Further symbols can be found on higher Fxx key symbols. diff --git a/ide/coqide.ml b/ide/coqide.ml index 15b34b8dc..f1ef1b450 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1832,7 +1832,7 @@ let start () = with Not_found -> ()); ignore (GtkMain.Main.init ()); GtkData.AccelGroup.set_default_mod_mask - (Some [`CONTROL;`SHIFT;`MOD1;`MOD4]); + (Some [`CONTROL;`SHIFT;`MOD1;`MOD3;`MOD4]); cb_ := Some (GtkBase.Clipboard.get Gdk.Atom.primary); Glib.Message.set_log_handler ~domain:"Gtk" ~levels:[`ERROR;`FLAG_FATAL; `WARNING;`CRITICAL] |