On 27 January 2017 at 09:12, Thomas Tuerk <[email protected]> wrote: > Hello, > > many thanks. That does the trick and is much nicer than my hack. > > @Magnus Myreen: Do you think this is worth adding to the HOL Interaction > manual?
Definitely! I've updated the HOL Interaction manual: https://hol-theorem-prover.org/HOL-interaction.pdf Cheers, Magnus > On 26.01.2017 22:25, Chun Tian (binghe) wrote: > > I took a look into sml-mode.el and the documentation [1], it seems that the > following Emacs configuration could disable the auto-indent triggered by > return key: > > (defun my-sml-mode-hook () > "Local defaults for SML mode" > (setq electric-indent-chars '())) > > (add-hook 'sml-mode-hook 'my-sml-mode-hook) > > P. S. You can only see the effect for newly opened SML code files. (or just > restart Emacs) > > [1] http://www.smlnj.org/doc/Emacs/sml-mode.html > > Il giorno 26 gen 2017, alle ore 09:43, Heiko Becker > <[email protected]> ha scritto: > > Hello everyone, > > I am currently running into some technical "difficulties" with using HOL4: > > I found that the emacs sml-mode binds the return key to > "newline-and-indent" and I cannot find a way to remove this binding. > Problem being that emacs keeps indenting my tactic proofs totally weird, > so I would favour being able to indent only on my own. > > So far, I tried deactivating it similar to what worked for removing > tab-indentation > > (setq default-tab-width 4) > (setq-default indent-tabs-mode nil) > (global-set-key (kbd "TAB") 'self-insert-command) > > by setting > > (global-set-key (kbd "RET") 'newline) > > > Unfortunately this does not work. Can someone help me with this issue > with some elisp? > > > Thanks in advance. > > Best regards, > > Heiko > > > ------------------------------------------------------------------------------ > Check out the vibrant tech community on one of the world's most > engaging tech sites, SlashDot.org! http://sdm.link/slashdot > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info > > > > ------------------------------------------------------------------------------ > Check out the vibrant tech community on one of the world's most > engaging tech sites, SlashDot.org! http://sdm.link/slashdot > > > > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info > > ------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, SlashDot.org! http://sdm.link/slashdot _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
