Hello. Thanks for your reply. On 2017-08-20 16:31 +0200 "Chun Tian (binghe)" <binghe.l...@gmail.com> wrote: >in which the two appearances of “DIVIDES_0” are perfectly aligned, so >that if I wrongly used different names, I can find out this mistake >immediately. The 2nd argument (the theorem statement) of store_thm, if >it’s not short, I will put it into separated line.
I see your point, but I think that this is an inelegant and unreliable approach. My suggestion would be to write some Elisp code that checks for this, and reports mismatches in an appropriate way. >But what’s more important, is to disable the auto-indentation of SML >mode, once I have adjusted my personal-style indentation and hit the RET >key to go to next line. To completely disable SML mode’s auto-indentaion >on RET, as suggested in official HOL emacs manual (originally found by >myself), you should put the following lines into your Emacs >configuration: (if you haven’t done this) Please note that my query (as I wrote in the original message) is for a way to have reasonable automatic indentation support for HOL proof scripts, not to disable automatic indentation entirely, or for workaround. The workaround suggested in the HOL Emacs documentation has the shortcoming that <RET> no longer indents, and <TAB> will indent according to the SML mode seemingly arbitrary rules. For lack of a better solution, I have been using the following workaround which is _slightly_ better: (defun sml-mode-sane-indent () (setq-local tab-width 4) (setq-local indent-line-function 'indent-relative-maybe)) (add-hook 'sml-mode-hook 'sml-mode-sane-indent) <TAB> indents to the indentation level of the previous line, or adds a TAB (or the equivalent in spaces if intent-tabs-mode is nil) if already indented. If called over a top-level statement, M-x indent-region (or <TAB> with active region) will unindent completely. Thus this is a very poor solution. Most major modes (e.g.: C mode) do the *appropriate* indentation in all of these cases. *Is there some solution that gives C-like automatic indentation* (without having to hack SML mode)? Regards.
pgp_5l9fk09WH.pgp
Description: OpenPGP digital signature
------------------------------------------------------------------------------ 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
