> *Is there some solution that gives C-like automatic indentation* (without
> having to hack SML mode)?
Short answer: no.
The situation with the emacs mode is clearly far from ideal. I have long since
trained myself to use the automatic indentation facilities when I know they
will get me roughly the effect I want, to manually correct the occasional
anomaly, and to indent manually when necessary. I agree that it would be nice
if the automatic tools did Just Work.
For example, I write goals+tactics in this style:
val addNode_preserves_wfg = Q.store_thm(
"addNode_preserves_wfg[simp]",
‘wfg g ⇒ wfg (addNode i g)’,
simp[wfg_def, addNode_def] >>
dsimp[wfAdjacency_def, lookup_insert, cond_eq] >> metis_tac[]);
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:
val addNode_preserves_wfg = Q.store_thm(
"addNode_preserves_wfg[simp]",
‘wfg g ⇒ wfg (addNode i g)’,
simp[wfg_def, addNode_def] >>
dsimp[wfAdjacency_def, lookup_insert, cond_eq] >> metis_tac[]);
This isn’t so bad, but it’s not what I want. The behaviour is not consistent
either, because the following one-liner
val graph_size_addNode = Q.store_thm(
"graph_size_addNode[simp]",
‘wfg g ⇒ graph_size (addNode i g) = graph_size g + 1’,
simp[graph_size_def, addNode_def, size_insert, wfg_def]);
turns into
val graph_size_addNode = Q.store_thm(
"graph_size_addNode[simp]",
‘wfg g ⇒ graph_size (addNode i g) = graph_size g + 1’,
simp[graph_size_def,
addNode_def, size_insert, wfg_def]);
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:
(setq indent-tabs-mode nil)
(setq sml-type-of-indent nil)
(setq sml-nested-if-indent t)
(setq sml-indent-level 2)
(electric-indent-mode -1)
- - -
Given that script files are typically a very constrained subset of full SML, it
might make the most sense to implement a major mode for script files that was
special-cased to tactics and goals, and which could handle a standard style.
(For example, I imagine it might be possible to use regular expressions and the
font-lock engine to highlight mismatched SML-level and store_thm names.)
Note that you’d probably want the HOL text occurring within backquotes (or “..”
and ‘..’) to be handled differently: it’s a different language after all.
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.
Michael
On 21/8/17, 02:19, "Mario Castelán Castro" <marioxcc...@yandex.com> wrote:
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.
------------------------------------------------------------------------------
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
