lxndrcx/prooftheoryhol

Equivalence of natural deduction and sequent calculus in HOL4

prooftheoryhol's Issues

Weird error in emacs hol

I get his in the emacs hol session when I interrupt:

>  C-c C-cVimhol's tail gave eof
Compilation interrupted

> 

Why is Vimhol doing something when I start this session in emacs? I cleaned and rebuilt hol and the issue remains. Is my config donked up somewhere?

Emacs annoying indentation

Emacs is doing annoying indentation. I have tried changing settings for sml mode with no success. the most annoying thing is when I type a pipe | emacs moves it to a new line and indents it. How do I make this better, other than by disabling sml mode completely?

my emacs config includes:

(defun my-sml-mode-hook () "Local defaults for SML mode"
         (setq words-include-escape t)    ; \ loses word break status
         (setq sml-electric-pipe-mode nil)
         (setq sml-program-name 'poly)
         (setq electric-indent-chars '())
         )
  (add-hook 'sml-mode-hook 'my-sml-mode-hook)
  (setq electric-indent-chars nil)