Re: custom keybindings [Re: html_mode vs _Jed_Emulation]

["John E. Davis" <davis>]

Tomasz Sienicki <tsca@xxxxxx> wrote:
> Do I understand correctly that using the _Jed_Emulation/keybindings_hook
> mechanism is the right way of customising the keybindings now (instead of
> putting setkey definitions directly in .jedrc)? Seems a little bit
> complicated... I feel like I'm missing something.

The preferred way is to use either "require" or "evalfile" to load the
desired keybinding file.  Then use "setkey" to tweak those if you
want.  

The "keybindings_hook" was added to support the "-e emulation"
command line parameter and to allow the administrator to setup
a default emulation for all users by adding the appropriate lines to,
e.g., /etc/jed.conf.  For example, in my /etc/jed.conf, I have:

  switch (path_basename (__argv[0]))
  { case "ide": _Jed_Default_Emulation = "ide";}
  { case "emacs": _Jed_Default_Emulation = "emacs";}
  { case "edt": _Jed_Default_Emulation = "edt";}
  { case "brief": _Jed_Default_Emulation = "brief";}
  { _Jed_Default_Emulation = "jed"; } % default

where /usr/bin/ide, /usr/bin/emacs, etc. are symlinked to
/usr/bin/jed.  Hence, if one runs jed via the "ide" symlink, then jed
will use "ide" bindings as long as the user does not explicitly load
bindings in the .jedrc file.

In addition, suppose that the administrator wants to provide the users
with a binding to the extremely useful "double_line" function.  The
best way to accomplish this is via a keybindings_hook in jed.conf:

   define keybindings_hook (emulation)
   {
      switch (emulation)
      {
         case "emacs": setkey ("double_line", "^Xl");
      }
      {
         case "ide": setkey ("double_line", "^K^L");
      }
         .
	 .
   }
   

The old mechanism required required the administrator to put such
tweaks into $JED_ROOT/jed/jed.rc, which was overwritten with each
upgrade.

I hope this clarifies the role of _Jed_Default_Emulation and the
keybindings_hook hook.

Thanks,
--John

--------------------------
To unsubscribe send email to <jed-users-request@xxxxxxxxxxx> with
the word "unsubscribe" in the message body.
Need help? Email <jed-users-owner@xxxxxxxxxxx>.