On 2017-08-21 02:31 +0000 <michael.norr...@data61.csiro.au> wrote: >> *Is there some solution that gives C-like automatic indentation* >> (without having to hack SML mode)? > >Short answer: no.
Thanks for your honest answer.
>If I run my cursor down column 0 and hit TAB at each point, the string and
>quotation both move inwards to column 6, and the tactic lines move across
>to column 7, creating:
I see.
For manually indenting several lines at once, the “indent-rigidly” command
(M-x TAB) is more convenient. The amount of space that it adds when using
shift is given by “tab-width” (even when “indent-tabs-mode” is nil).
>and I have no idea why there is a difference in the handling of the
>tactic line. Luckily, tactics will typically indent correctly after the
>first line has been put to the right level. I think the relevant parts
>of my .emacs config are:
What do you think about replacing the SML mode indentation function with
“indent-relative-maybe” as I mentioned in my previous message?
(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)
Then auto-indentation after <RET> works reasonably, so it needs not be
disabled with “(setq electric-indent-chars nil)”. Moreover, M-x
indent-region will do a good enough job for many cases if one line before
the region is intended to what one.
For example, consider this trivial example:
val DIVIDES_0 = store_thm(
"DIVIDES_0",
“!x. x divides 0”,
metis_tac [divides_def, MULT_CLAUSES]);
Then I go to the beginning of the second line and press TAB.
val DIVIDES_0 = store_thm(
"DIVIDES_0",
“!x. x divides 0”,
metis_tac [divides_def, MULT_CLAUSES]);
Then I mark the other 2 lines and press TAB again once:
val DIVIDES_0 = store_thm(
"DIVIDES_0",
“!x. x divides 0”,
metis_tac [divides_def, MULT_CLAUSES]);
Done.
>Pull requests from capable emacs hackers would be gratefully received.
>Unfortunately, I am not a particularly capable emacs hacker, and I don’t
>have a great deal of time to spend on it at the moment.
Unfortunately I am no Emacs expert either. I have been using it for years
but I have only recently started to try to learn to use it properly.
I am also still learning HOL4. I do not know if I will stay with it or move
to a different proof assistant, since I am new to proof assistants overall
and I have yet to try the alternatives. However, if I become a regular
user, I will probably try to write a “HOL4-script-mode”.
Regards and thanks.
--
Do not eat animals, respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
signature.asc
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
