Hello. Is there some way to make the behavior of auto-indentation in GNU Emacs when writing for proof scripts more predictable? By default it uses SML mode, which is shipped with Emacs. I can not find any documentation about it other than the built-in help, which is not of much use.
I find that SML mode chooses indentation level in an unpredictable way, for
example, it intend the following code this way:
val DIVIDES_0 =
store_thm(
"DIVIDES_0",
``!x. x divides 0``,
metis_tac [divides_def,MULT_CLAUSES]);
(note the extra 2 spaces before “metis_tac”)
If I put “store_thm” in a line of its own, I get an exaggerate amount of
indentation:
val DIVIDES_0 = store_thm
("DIVIDES_0",
``!x. x divides 0``,
metis_tac [divides_def,MULT_CLAUSES]);
Disabling indentation completely (e.g.: M-x fundamental-mode) is not a
satisfactory solution. Is there some way to make Emacs perform sensible
indentation for HOL proof scripts?
Thanks in advance.
pgp4KJ7NyqMKU.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
