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?
Thank you,
Thomas Tuerk
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
>> <s9hhb...@stud.uni-saarland.de> 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
>> hol-info@lists.sourceforge.net
>> 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
> hol-info@lists.sourceforge.net
> 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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
