HOL Emacs Mode

The HOL and SML distributions come with emacs modes that make using the command-line interface of HOL a little easier. Even if you are not a regular emacs user, you may find this helpful. Here's how to set it up for use on the watform servers and where to find out more information about it.

1. In the .emacs file in your home directory add the following lines,

   (setq load-path
     (cons "/watform/pkg/mosml/utility/sml-mode-3.3b/" load-path)
   )
   
   
   (load "/watform/pkg/hol/tools/hol98-mode.el")
   (load "/watform/pkg/mosml/utility/sml-mode-3.3b/sml-mosml.el")
   
   (autoload 'sml-mosml "sml-mosml" "Set up and run Moscow ML." t)
   
   (setq sml-mode-hook
         '(lambda() "SML mode defaults to Moscow ML"
        (define-key  sml-mode-map "\C-cp" 'sml-mosml)))
   
   ;; assumes hol.unquote is in your path
   (setq sml-program-name "hol.unquote")
   
   (define-key          sml-mode-map "\C-c\C-f" 'sml-send-function)
   
   (setq inferior-sml-load-hook
      '(lambda() "Set global defaults for inferior-sml-mode"
          (define-key inferior-sml-mode-map "\C-cd"    'sml-cd)
          (define-key          sml-mode-map "\C-cd"    'sml-cd)
          (setq
            sml-temp-threshold       0 ; safe: always use tmp file
            comint-scroll-show-maximum-output t
            comint-scroll-to-bottom-on-output t
            comint-input-autoexpand           nil
          )
   ))
   
   (setq auto-mode-alist
     (append '(
               ("\\.sml$" . sml-mode)
              )
     )
   )
   

2. Now, when you are in emacs and you load a file with the .sml extension, it will automatically put you in SML mode. You can tell this by seeing the "(SML)" in the bar on the bottom of your screen.
3. I find the most useful command is to send a paragraph to a hol session running in another emacs buffer. With the cursor on the first character of the paragraph you wish to send, type "C-c C-f". The first time you do this, it will ask you what hol executable to run and provide the appropriate default, and then ask you if there are any arguments for the executable, and you can just hit Enter.
4. You probably want to split your emacs screen and show the hol session in the upper or lower partition and the editing window in the other one. "C-x 2" splits the screen. "C-x o" moves you to the next partition. Using the "buffers" menu you can choose which emacs buffer to display in that partition.
5. Another useful command is to send a larger region of commands to a hol session. At the beginning of the region, type "C-space", and at the end of the region type "C-c C-r".
6. More information (and the complete list of commands) is available at: http://hol.sourceforge.net/hol-mode.html