From 5fda98a3491408f43f3c2a9d8a0b1f8b42fea00d Mon Sep 17 00:00:00 2001
From: Joseph Chan <jhlchan@gmail.com>
Date: Sun, 15 Dec 2024 13:27:43 +1100
Subject: [PATCH] Update tools.

---
 tools/hol-mode.el        | 2215 ++++++++++++++++++++++++++++++++++++++
 tools/vim/filetype.vim   |    9 +
 tools/vim/hol-config.sml |    1 +
 tools/vim/hol.vim        |  374 +++++++
 tools/vim/vimhol.sml     |  120 +++
 5 files changed, 2719 insertions(+)
 create mode 100644 tools/hol-mode.el
 create mode 100644 tools/vim/filetype.vim
 create mode 100644 tools/vim/hol-config.sml
 create mode 100644 tools/vim/hol.vim
 create mode 100644 tools/vim/vimhol.sml

diff --git a/tools/hol-mode.el b/tools/hol-mode.el
new file mode 100644
index 0000000000..ebdbdeac27
--- /dev/null
+++ b/tools/hol-mode.el
@@ -0,0 +1,2215 @@
+;;; -*- emacs-lisp -*-
+;;; to use this mode, you will need to do something along the lines of
+;;; the following and have it in your .emacs file:
+;;;    (setq hol-executable "<fullpath to HOL executable>")
+;;;    (load "<fullpath to this file>")
+
+;;; The fullpath to this file can be just the name of the file, if
+;;; your elisp variable load-path includes the directory where it
+;;; lives.
+
+(require 'thingatpt)
+(require 'cl-lib)
+(require 'subr-x)
+
+(defgroup hol nil
+  "Customising the Emacs interface to the HOL4 proof assistant."
+  :group 'external)
+
+(define-prefix-command 'hol-map)
+(define-prefix-command 'hol-d-map)
+(define-prefix-command 'hol-movement-map)
+(make-variable-buffer-local 'hol-buffer-name)
+(set-default 'hol-buffer-name "*HOL*")
+
+(set-default 'hol-default-buffer nil)
+
+(defcustom hol-executable 
+  "/Users/josephchan/HOL/bin/hol"
+  "Path-name for the HOL executable."
+  :group 'hol
+  :type '(file :must-match t))
+
+(defcustom holmake-executable 
+  "/Users/josephchan/HOL/bin/Holmake"
+  "Path-name for the Holmake executable."
+  :group 'hol
+  :type '(file :must-match t))
+
+(defcustom hol-show-tooltips-in-minibuffer t
+  "Whether to additionally show tooltips in minibuffer."
+  :group 'hol
+  :type '(choice
+          (const :tag "Yes; messages appear in minibuffer" t)
+          (const :tag "No; messages only in tooltips" nil)))
+
+(defconst hol-dir
+  (file-name-directory
+   (directory-file-name (file-name-directory hol-executable))))
+(setq load-path (cons (concat hol-dir "tools/") load-path))
+(require 'holscript-mode)
+
+(defcustom hol-new-buffer-style-default 'new-frame
+  "Default style for creating new HOL buffers. Possible values are
+new-frame (create in a new-frame); horizontal (create in a new buffer
+that is horizontally adjacent and to the right); and vertical (create in
+a new buffer that is vertically adjacent and below)."
+  :group 'hol
+  :type '(choice (const new-frame :tag "new-frame")
+                 (const horizontal :tag "horizontal")
+                 (const vertical :tag "vertical")))
+
+(defun hol-set-executable (filename)
+  "*Set hol executable variable to be NAME."
+  (interactive "fHOL executable: ")
+  (setq hol-executable filename)
+  (setq hol-bare-p nil))
+
+(defun holmake-set-executable (filename)
+  "*Set holmake executable variable to be NAME."
+  (interactive "fHOL executable: ")
+  (setq holmake-executable filename))
+
+(defvar hol-mode-sml-init-command
+   "use (Globals.HOLDIR ^ \"/tools/hol-mode.sml\")"
+  "*The command to send to HOL to load the ML-part of hol-mode.")
+
+
+(defcustom hol-echo-commands-p nil
+  "Whether or not to echo the text of commands originating elsewhere."
+  :group 'hol
+  :type 'boolean)
+
+(defcustom hol-raise-on-recentre nil
+  "Controls if hol-recentre (\\[hol-recentre]) also raises the HOL frame."
+  :group 'hol
+  :type 'boolean)
+
+(defcustom hol-unicode-print-font-filename
+  "/usr/share/fonts/truetype/ttf-dejavu/DejaVuSans.ttf"
+  "File name of font to use when printing HOL output to a PDF file."
+  :group 'hol
+  :type '(file :must-match t))
+
+
+
+(defvar hol-generate-locpragma-p t
+  "*Whether or not to generate (*#loc row col *) pragmas for HOL.")
+
+(defvar hol-emit-time-elapsed-p nil
+  "*Whether or not to print time elapsed messages after causing HOL
+evaluations.")
+
+(defvar hol-auto-load-p t
+  "*Do automatic loading?")
+
+(defvar hol-bare-p nil
+  "*use hol.bare?")
+
+;;; For compatability between both Emacs and XEmacs, please use the following
+;;; two functions to determine if the mark is active, or to set it active.
+
+(defun is-region-active ()
+  (or
+    (and (fboundp 'region-active-p) (region-active-p)
+         (fboundp 'region-exists-p) (region-exists-p))
+    (and transient-mark-mode (boundp 'mark-active) mark-active)))
+
+(defun set-region-active ()
+  (or
+    (and (fboundp 'zmacs-activate-region) (zmacs-activate-region))
+    (and (boundp 'mark-active) (setq mark-active t))))
+
+(defvar-local hol-term-end-delim nil)
+(put 'hol-term 'end-op
+     (function
+      (lambda ()
+        (let ((pthm-point
+               (save-excursion
+                 (let ((ok t))
+                   (while
+                       (and ok
+                            (re-search-forward
+                             "^Proof\\|^Theorem\\|^Triviality" nil t))
+                     (let ((ppss (syntax-ppss)))
+                       (if (or (nth 3 ppss) (nth 4 ppss)) nil
+                         (setq ok nil))))
+                   (not ok)))))
+          (if (and pthm-point (equal (match-string 0) "Proof"))
+              (progn (goto-char (match-beginning 0))
+                     (setq hol-term-end-delim "Proof"))
+            (re-search-forward "[`’”]\\|^End\\|^Termination" nil t)
+            (setq hol-term-end-delim (match-string 0))
+            (goto-char (match-beginning 0)))))))
+(defvar hol-beg-pos nil) ; ugh, global, but easiest this way
+(defvar hol-name-attrs-colon-re
+  "[[:space:]]+[A-Za-z0-9'_]+\\(\\[[A-Za-z0-9_,]+\\]\\)?[[:space:]]*:")
+(defvar hol-quoted-theorem-proof-re-begin
+  (concat "\\(Theorem\\|Triviality\\)" hol-name-attrs-colon-re))
+(defvar hol-quoted-definition-re-begin
+  (concat "\\(Definition\\|\\(Co\\)?Inductive\\)" hol-name-attrs-colon-re))
+(put 'hol-term 'beginning-op
+     (function
+      (lambda ()
+        (let ((beg
+               (cond
+                ((equal hol-term-end-delim "`") "`")
+                ((equal hol-term-end-delim "’") "‘")
+                ((equal hol-term-end-delim "”") "“")
+                ((equal hol-term-end-delim "Proof")
+                 hol-quoted-theorem-proof-re-begin)
+                ((or (equal hol-term-end-delim "End")
+                     (equal hol-term-end-delim "Termination"))
+                 hol-quoted-definition-re-begin))))
+          (re-search-backward beg nil t)
+          (goto-char (match-end 0))
+          (setq hol-beg-pos (point))))))
+
+(defun hol-term-at-point ()
+  (let ((s (thing-at-point 'hol-term t)))
+    (with-hol-locpragma hol-beg-pos s)))
+
+(defun hol-buffer-ok (string)
+  "Checks a string to see if it is the name of a good HOL buffer.
+In reality this comes down to checking that a buffer-name has a live
+process in it."
+  (and string (get-buffer-process string)
+       (eq 'run
+           (process-status
+            (get-buffer-process string)))))
+
+(defun ensure-hol-buffer-ok ()
+  "Ensures by prompting that a HOL buffer name is OK, and returns it."
+  (if (hol-buffer-ok hol-buffer-name) hol-buffer-name
+    (message
+     (cond (hol-buffer-name (concat hol-buffer-name " not valid anymore."))
+           (t "Please choose a HOL to attach this buffer to.")))
+    (sleep-for 1)
+    (setq hol-buffer-name (read-buffer "HOL buffer: " hol-default-buffer t))
+    (while (not (hol-buffer-ok hol-buffer-name))
+      (ding)
+      (message "Not a valid HOL process")
+      (sleep-for 1)
+      (setq hol-buffer-name
+            (read-buffer "HOL buffer: " hol-default-buffer t)))
+    (setq hol-default-buffer hol-buffer-name)
+    hol-buffer-name))
+
+
+
+(defun with-hol-locpragma (pos s)
+  (if hol-generate-locpragma-p
+      (concat (hol-locpragma-of-position pos) s)
+      s))
+
+(defun hol-locpragma-of-position (pos)
+  "Convert Elisp position into HOL location pragma.  Not for interactive use."
+  (let ((initial-point (point)))
+    (goto-char pos)
+    (let* ((rowstart (point-at-bol))  ;; (line-beginning-position)
+           (row      (+ (count-lines 1 pos)
+                      (if (= rowstart pos) 1 0)))
+           (col      (+ (current-column) 1)))
+      (goto-char initial-point)
+      (format " (*#loc %d %d *)\n" (- row 1) col))))
+
+(defun send-raw-string-to-hol (string echoit)
+  "Sends a string in the raw to HOL.  Not for interactive use."
+  (let ((buf (ensure-hol-buffer-ok)))
+    (if echoit
+        (with-current-buffer buf
+          (goto-char (point-max))
+          (princ (concat string ";") (get-buffer buf))
+          (goto-char (point-max))
+          (comint-send-input)
+          (hol-recentre 1))
+      (comint-send-string buf (concat string ";\n")))))
+
+(defun send-timed-string-to-hol (string echo-p &optional loud-opens)
+  "Send STRING to HOL (with send-string-to-hol), and emit information about
+how long this took."
+  (interactive)
+  (send-raw-string-to-hol
+   "val hol_mode_time0 = #usr (Timer.checkCPUTimer Globals.hol_clock);" nil)
+  (send-string-to-hol string echo-p)
+  (send-raw-string-to-hol
+       "val _ = let val t = #usr (Timer.checkCPUTimer Globals.hol_clock)
+                      val elapsed = Time.-(t, hol_mode_time0)
+                in
+                      print (\"\\n*** Time taken: \"^
+                             Time.toString elapsed^\"s\\n\")
+                  end" nil))
+
+(defvar tactic-connective-regexp
+  "[[:space:]]*\\(THEN1\\|THENL\\|THEN\\|>>\\|>|\\|>-\\|>~\\|\\\\\\\\\\)[[:space:]]*[[(]?"
+  "Regular expression for strings used to put tactics together.")
+
+(defun tactic-cleanup-leading (string)
+  "Remove leading instances of tactic connectives from a string.
+A tactic connective is any one of \"THEN\", \"THENL\", \"THEN1\", \">>\", \">|\"
+or \">-\"."
+  (let* ((case-fold-search nil)
+         (pattern (concat "\\`" tactic-connective-regexp)))
+    (replace-regexp-in-string pattern "" string)))
+
+(defun tactic-cleanup-trailing (string)
+  "Remove trailing instances of tactic connectives from a string.
+A tactic connective is any one of \"THEN\", \"THENL\", \"THEN1\", \">>\", \">|\"
+or \">-\"."
+  (let* ((case-fold-search nil)
+         (pattern (concat tactic-connective-regexp "\\'")))
+    (replace-regexp-in-string pattern "" string)))
+
+(defun hol-find-eval-next-tactic (arg)
+  "Highlights the next tactic in the source and evaluates in the HOL buffer.
+With a prefix ARG, uses `expandf' rather than `e'."
+  (interactive "P")
+  (deactivate-mark)
+  (skip-syntax-forward " ")
+  (let
+      ((term (thing-at-point 'tactic-terminator))
+       (sqb (char-equal (following-char) ?\[)))
+    (while (or term sqb)
+      (cond (term (forward-tactic-terminator 1))
+            (sqb (forward-char)))
+      (skip-syntax-forward " ")
+      (setq term (thing-at-point 'tactic-terminator))
+      (setq sqb (char-equal (following-char) ?\[))))
+  (mark-hol-tactic)
+  (copy-region-as-hol-tactic (region-beginning) (region-end) arg)
+  (goto-char (region-end)))
+
+(defun copy-region-as-hol-tactic (start end arg)
+  "Send selected region to HOL process as tactic."
+  (interactive "r\nP")
+  (let*
+      ((region-string0 (buffer-substring start end))
+       (region-string1 (tactic-cleanup-leading region-string0))
+       (region-string2 (tactic-cleanup-trailing region-string1))
+       (start-offset (- (length region-string0) (length region-string1)))
+       (region-string3 (with-hol-locpragma (+ start start-offset) region-string2))
+       (ste "\"show_typecheck_errors\"")
+       (region-string (concat "let val old = Feedback.current_trace "
+                              ste
+                              " val _ = Feedback.set_trace "
+                              ste
+                              " 0 in ("
+                              region-string3
+                              ") before "
+                              "Feedback.set_trace " ste " old end"))
+       (e-string (concat "proofManagerLib." (if arg "expandf" "e")))
+       (tactic-string (format "%s (fn HOL__GOAL__foo => (%s) HOL__GOAL__foo)"
+                              e-string region-string))
+       (sender (if hol-emit-time-elapsed-p
+                   'send-timed-string-to-hol
+                 'send-string-to-hol)))
+    (funcall sender tactic-string hol-echo-commands-p)))
+
+;;; For goaltrees
+(defun copy-region-as-goaltree-tactic (start end)
+  "Send selected region to HOL process as goaltree tactic."
+  (interactive "r\nP")
+  (let* ((region-string (with-hol-locpragma start
+                          (buffer-substring-no-properties start end)))
+         (tactic-string
+           (format "proofManagerLib.expandv (%S,%s) handle e => Raise e"
+                   region-string region-string))
+         (sender (if hol-emit-time-elapsed-p
+                     'send-timed-string-to-hol
+                   'send-string-to-hol)))
+    (funcall sender tactic-string hol-echo-commands-p)))
+
+(defun send-string-as-hol-goal (s &optional attr-string)
+  (let ((goal-string
+         (if attr-string
+             (progn
+               (message (format "Using tactic-modifier %s" attr-string))
+               (format "proofManagerLib.new_goalstack ([], “%s”) \
+                         (BasicProvers.mk_tacmod %s) I" s attr-string))
+           (format  "proofManagerLib.g `%s`" s))))
+    (send-raw-string-to-hol goal-string hol-echo-commands-p)
+    (send-raw-string-to-hol "proofManagerLib.set_backup 100;" nil)))
+
+(defun count-text-match (regex string)
+  (let ((case-fold-search nil)
+        (i 0)
+        (c 0))
+    (while (string-match regex string i)
+      (progn (setq i (match-end 0))
+             (setq c (+ c 1))))
+    c))
+
+(defun hol-string-contains-term-delimiters-p (s)
+  (< 0 (count-text-match
+        (concat "^Theorem\\|^Definition\\|^Proof\\|^\\(Co\\)?Inductive\\|"
+                "^Termination\\|^End\\|[“”‘’`]\\|^Triviality")
+        s)))
+
+
+(defun hol-get-proof-attribute-string ()
+  "Get attribute string following a Proof keyword that follows point."
+  (save-mark-and-excursion
+    (let ((pos (point))
+          (proof-pos (re-search-forward "^Proof" nil t)))
+      (if proof-pos
+          (let ((prev-term (re-search-backward "[”’`]" pos t)))
+            (if prev-term nil
+              (goto-char (match-end 0))
+              (skip-chars-forward "[:space:]")
+              (if (equal (char-after) ?\[)
+                  (let ((sq-start (point)))
+                    (condition-case nil
+                        (progn
+                          (skip-chars-forward "^]")
+                          (forward-char)
+                          (buffer-substring-no-properties sq-start (point)))
+                      (error nil)))
+                nil)))
+        nil))))
+
+(defun hol-do-goal (arg)
+  "Send term around point to HOL process as goal.
+If prefix ARG is true, or if in transient mark mode, region is active and
+the region contains no term-delimiters, then send region instead."
+  (interactive "P")
+  (let ((txt (condition-case nil
+                 (with-hol-locpragma (region-beginning)
+                    (buffer-substring (region-beginning) (region-end)))
+               (error nil)))
+        (attr-string (hol-get-proof-attribute-string)))
+    (if (or (and (is-region-active)
+                 (not (hol-string-contains-term-delimiters-p txt)))
+            arg)
+      (send-string-as-hol-goal txt)
+      (let ((attr-s
+             (if attr-string
+                 (concat "\""
+                         (replace-regexp-in-string
+                          "[[:space:]\n]+" " "
+                          attr-string)
+                         "\"")
+               nil)))
+        (send-string-as-hol-goal (hol-term-at-point) attr-s)))))
+
+
+(defun send-string-as-hol-goaltree (s)
+  (let ((goal-string
+         (format  "proofManagerLib.gt `%s` handle e => Raise e" s)))
+    (send-raw-string-to-hol goal-string hol-echo-commands-p)
+    (send-raw-string-to-hol "proofManagerLib.set_backup 100;" nil)))
+
+
+(defun hol-do-goaltree (arg)
+  "Send term around point to HOL process as goaltree.
+If prefix ARG is true, or if in transient mark mode, region is active and
+the region contains no backquotes, then send region instead."
+  (interactive "P")
+  (let ((txt (condition-case nil
+                 (with-hol-locpragma (region-beginning)
+                    (buffer-substring (region-beginning) (region-end)))
+               (error nil))))
+    (if (or (and (is-region-active) (= (cl-count ?\` txt) 0))
+            arg)
+      (send-string-as-hol-goaltree txt)
+    (send-string-as-hol-goaltree (hol-term-at-point)))))
+
+(defun copy-region-as-hol-definition (start end arg &optional loud-opens0)
+  "Send selected region to HOL process as definition/expression.  With a
+prefix arg of 4 (hit control-u once), wrap what is sent so that it becomes
+( .. ) handle e => Raise e, allowing HOL_ERRs to be displayed cleanly.
+With a prefix arg of 16 (hit control-u twice), toggle `quiet-declarations'
+before and after the region is sent."
+  (interactive "r\np")
+  (let* ((buffer-string
+            (with-hol-locpragma start (buffer-substring start end)))
+         (send-string
+          (if (= arg 4)
+              (concat "(" buffer-string ") handle e => Raise e")
+            buffer-string))
+         (loud-opens (if (= arg 16) t loud-opens0))
+         (sender (if hol-emit-time-elapsed-p
+                     'send-timed-string-to-hol
+                   'send-string-to-hol)))
+    (if (= arg 16) (hol-toggle-quietdec))
+    (unwind-protect
+        (progn
+          (funcall sender send-string hol-echo-commands-p loud-opens)
+          (if (> (length send-string) 300)
+              (send-string-to-hol
+               (concat "val _ = print \"\\n*** Emacs/HOL command completed "
+                       "***\\n\\n\""))))
+      (if (= (prefix-numeric-value arg) 16) (hol-toggle-quietdec)))))
+
+
+
+(defun hol-what-was-copy-region-as-hol-definition-quietly ()
+   (interactive "")
+   (ding)
+   (message "Deprecated: use C-u C-u M-h M-r for quiet region execution instead"))
+
+
+(defun hol-name-top-theorem (string arg)
+  "Name the top theorem of the proofManagerLib.
+With prefix argument, drop the goal afterwards."
+  (interactive "sName for top theorem: \nP")
+  (if (not (string= string ""))
+      (send-raw-string-to-hol
+       (format "val %s = top_thm()" string)
+       hol-echo-commands-p))
+  (if arg
+      (send-raw-string-to-hol "proofManagerLib.drop()" hol-echo-commands-p)))
+
+(defun hol-start-termination-proof (arg)
+  "Send definition around point to HOL process as Defn.tgoal.
+If prefix ARG is true, or if in transient mark mode, region is active and
+the region contains no term delimiters, then send region instead."
+  (interactive "P")
+  (let ((txt (condition-case nil
+                 (with-hol-locpragma (region-beginning)
+                    (buffer-substring (region-beginning) (region-end)))
+               (error nil))))
+    (if (or (and (is-region-active)
+                 (not (hol-string-contains-term-delimiters-p txt)))
+            arg)
+      (hol-send-string-as-termination-proof txt)
+    (hol-send-string-as-termination-proof (hol-term-at-point)))))
+
+(defun hol-send-string-as-termination-proof (str)
+  (send-raw-string-to-hol
+   (concat "Defn.tgoal (Defn.Hol_defn \"HOLmode_defn\" `"
+           str "`) handle e => Raise e")
+   nil))
+
+(defun remove-sml-comments (end)
+  (let (done (start (point)))
+    (while (and (not done) (re-search-forward "(\\*\\|\\*)" end t))
+        (if (string= (match-string 0) "*)")
+            (progn
+              (delete-region (- start 2) (point))
+              (setq done t))
+          ;; found a comment beginning
+          (if (not (remove-sml-comments end)) (setq done t))))
+      (if (not done) (message "Incomplete comment in region given"))
+      done))
+
+(defun remove-quoted-hol-term (bq eq end-marker &optional extra)
+  (let ((start (point))
+        (bqsize (length bq))
+        (i (if extra extra 0)))
+    (if (re-search-forward eq end-marker t)
+        (delete-region (- start (- bqsize i)) (point))
+      (error
+       (format "Incomplete (%s...%s-quoted) HOL term in region given; \
+starts >%s%s<"
+               bq eq
+               bq
+               (buffer-substring (point) (+ (point) 10)))))))
+
+(defun remove-hol-string (end-marker)
+  (let ((start (point)))
+    (if (re-search-forward "\n\\|[^\\]?\"" end-marker t)
+        (if (string= (match-string 0) "\n")
+            (message "String literal terminated by newline - not allowed!")
+          (delete-region (- start 1) (point))))))
+
+
+(setq hol-open-terminator-regexp
+      (concat
+       (mapconcat (lambda (s) (concat "^" s "\\>"))
+                  '("Theorem" "Definition" "Inductive" "CoInductive"
+                    "Triviality" "Datatype" "Type" "Overload")
+                  "\\|")
+       "\\|;\\|"
+       (regexp-opt
+        '("val" "fun" "in" "infix" "infixl" "infixr" "open" "local" "type"
+          "datatype" "nonfix" "exception" "end" "structure") 'symbols)))
+
+(setq sml-struct-id-regexp "[A-Za-z][A-Za-z0-9_]*")
+
+(defun send-string-to-hol (string &optional echoit leave-loud-opens)
+  "Send a string to HOL process."
+  (let ((buf (ensure-hol-buffer-ok))
+        (old-mark-active (is-region-active)))
+    (unwind-protect
+        (with-temp-buffer
+          (holscript-mode)
+          (setq hol-buffer-name buf) ; version of this variable in tmpbuf
+          (setq case-fold-search nil) ; buffer-local version
+          (insert string)
+          (goto-char (point-min))
+          ;; first thing to do is to search through buffer looking for
+          ;; identifiers of form id.id.  When spotted such identifiers need
+          ;; to have the first component of the name loaded.
+          (let ((regexp
+                 (concat "`\\|“\\|‘\\|"
+                         hol-quoted-theorem-proof-re-begin "\\|"
+                         hol-quoted-definition-re-begin "\\|"
+                         "\\(" sml-struct-id-regexp "\\)\\.\\w+" "\\|"
+                         "\\_<open\\_>")))
+            (while (re-search-forward regexp (point-max) t)
+              (let ((pp (syntax-ppss))
+                    (ms (match-string-no-properties 0)))
+                (if (and (not (nth 3 pp)) (not (nth 4 pp)))
+                    ;; maybe looking at termish thing that needs dodging
+                    (cond
+                     ((string= ms "`")
+                      (let ((term
+                             (if (looking-at "`") ; double backtick
+                                 (progn (forward-char 1) "``") "`")))
+                        (if (not (re-search-forward term nil t))
+                            (error
+                             (concat "Unbalanced " term " in region")))))
+                     ((string= ms "“")
+                      (if (not (re-search-forward "”" nil t))
+                          (error "Unbalanced “ in region")))
+                     ((string= ms "‘")
+                      (if (not (re-search-forward "’" nil t))
+                          (error "Unbalanced ‘ in region")))
+                     ((and (or (string-prefix-p "Theorem" ms)
+                               (string-prefix-p "Triviality" ms))
+                           (char-equal (char-before) ?:))
+                      (if (not (re-search-forward "^Proof" nil t))
+                          (error "Unbalanced `Theorem/Triviality' in region")))
+                     ((and (string-prefix-p "Definition" ms)
+                           (char-equal (char-before) ?:))
+                      (if (not
+                           (re-search-forward "^Termination\\|^End" nil t))
+                          (error "Unbalanced `Definition' in region")))
+                     ((and (or (string-prefix-p "Inductive" ms)
+                               (string-prefix-p "CoInductive" ms))
+                           (char-equal (char-before) ?:))
+                      (if (not (re-search-forward "^End" nil t))
+                          (error "Unbalanced [Co]Inductive in region")))
+                     ((string= ms "open")
+                      ;; point now after an open, now search forward
+                      ;; to end of buffer or a semi-colon, or an infix
+                      ;; declaration or a val or a fun or another open
+                      ;; or whatever, (as per the regexp defined just
+                      ;; before this function definition)
+                      (let ((open-start (match-beginning 0))
+                            (start (point))
+                            (end
+                             (save-excursion
+                               (let ((case-fold-search nil)
+                                     (foundp nil)
+                                     (abortedp nil))
+                                 ;; complicated loop required to avoid being
+                                 ;; confused by input such as
+                                 ;; open listSyntax (* ; *) integerTheory;
+                                 (while (and (not foundp) (not abortedp))
+                                   (if (re-search-forward
+                                        hol-open-terminator-regexp
+                                        nil t)
+                                       (setq foundp
+                                             (let ((pp (syntax-ppss)))
+                                               (and (not (nth 3 pp))
+                                                    (not (nth 4 pp)))))
+                                     (setq abortedp t)))
+                                 (if foundp
+                                     (- (point) (length (match-string 0)))
+                                   (point-max)))))
+                            (endm (make-marker)))
+                        ; (message "Handling an open")
+                        (if hol-auto-load-p
+                            (hol-load-modules-in-region start end))
+                        (if leave-loud-opens nil
+                            ;; now bracket the open decl with quietdec toggles
+                          (set-marker endm end)
+                          (goto-char end)
+                          (insert
+                           ";val _ = HOL_Interactive.toggle_quietdec();\n")
+                          (goto-char open-start)
+                          (insert
+                           "val _ = HOL_Interactive.toggle_quietdec();\n")
+                          (goto-char endm) (set-marker endm nil))))
+                     (t
+                      ; (message "Saw \"%s\"; position = %d; loading: %s"
+                      ;           ms (point) (match-string 6))
+                      (let ((mod-name (match-string 6)))
+                        (if hol-auto-load-p
+                            ;; need to check if we're in a Proof[...] block
+                            (let
+                                ((in-proof
+                                  (save-mark-and-excursion
+                                    (skip-chars-backward "A-Za-z0-9._, =\n")
+                                    (if(equal (char-before) ?\[)
+                                        (progn
+                                          (backward-char)
+                                          (skip-chars-backward " \n")
+                                          (looking-back "Proof"
+                                                        (- (point) 6)))))))
+                              (if (not in-proof)
+                                  (hol-load-string mod-name))))))))))
+          ;; send the string
+          (goto-char (point-min))
+            (send-buffer-to-hol-maybe-via-file echoit)))
+      )
+    ;; deactivate-mark will have likely been set by all the editting actions
+    ;; in the temporary buffer.  We fix this here, thereby keeping the mark
+    ;; active, if it is active.
+    ;; if in XEmacs, use (zmacs-activate-region) instead.
+    (if (boundp 'deactivate-mark)
+        (if deactivate-mark (setq deactivate-mark nil))
+        (if (and old-mark-active (fboundp 'zmacs-activate-region))
+            (zmacs-activate-region)))))
+
+(defun interactive-send-string-to-hol (string &optional echoit)
+   "Send a string to HOL process."
+   (interactive "sString to send to HOL process: \nP")
+   (if hol-emit-time-elapsed-p
+       (send-timed-string-to-hol string echoit)
+     (send-string-to-hol string echoit)))
+
+(if (null temporary-file-directory)
+    (if (equal system-type 'windows-nt)
+        (if (not (null (getenv "TEMP")))
+            (setq temporary-file-directory (getenv "TEMP")))
+      (setq temporary-file-directory "/tmp")))
+
+(defun make-temp-file-xemacs (prefix &optional dir-flag)
+  "Create a temporary file.
+The returned file name (created by appending some random characters at the end
+of PREFIX, and expanding against `temporary-file-directory' if necessary,
+is guaranteed to point to a newly created empty file.
+You can then use `write-region' to write new data into the file.
+
+If DIR-FLAG is non-nil, create a new empty directory instead of a file."
+  (let (file)
+    (while (condition-case ()
+	       (progn
+		 (setq file
+		       (make-temp-name
+			(expand-file-name prefix temporary-file-directory)))
+		 (if dir-flag
+		     (make-directory file)
+		   (write-region "" nil file nil 'silent nil)) ;; 'excl
+		 nil)
+	    (file-already-exists t))
+      ;; the file was somehow created by someone else between
+      ;; `make-temp-name' and `write-region', let's try again.
+      nil)
+    file))
+
+(defvar hol-mode-to-delete nil
+  "String optionally containing name of last temporary file used to transmit
+HOL sources to a running session (using \"use\")")
+
+(defun send-buffer-to-hol-maybe-via-file (&optional echoit)
+  "Send the contents of current buffer to HOL, possibly putting it into a
+file to \"use\" first."
+  (if (< 500 (buffer-size))
+          (let ((fname (if (fboundp 'make-temp-file)
+                              ;; then
+                                    (make-temp-file "hol" nil "Script.sml")
+                              ;; else
+                                    (make-temp-file-xemacs "hol")
+                                 )))
+            (if (stringp hol-mode-to-delete)
+                (progn (condition-case nil
+                           (delete-file hol-mode-to-delete)
+                         (error nil))
+                       (setq hol-mode-to-delete nil)))
+            ; below, use visit parameter = 1 to stop message in mini-buffer
+            (write-region (point-min) (point-max) fname nil 1)
+            (send-raw-string-to-hol (format "use \"%s\"" fname) nil)
+            (setq hol-mode-to-delete fname))
+    (send-raw-string-to-hol (buffer-string) echoit)))
+
+
+(defun hol-backup ()
+  "Perform a HOL backup."
+  (interactive)
+  (send-raw-string-to-hol "proofManagerLib.b()" hol-echo-commands-p))
+
+(defun hol-user-backup ()
+  "Perform a HOL backup to a user-defined save-point."
+  (interactive)
+  (send-raw-string-to-hol "proofManagerLib.restore()" hol-echo-commands-p))
+
+(defun hol-print-info ()
+  "Show some information about the currently running HOL and the settings of hol-mode."
+  (interactive)
+  (send-raw-string-to-hol
+   (concat "print_current_hol_status" "\""
+           hol-executable "\" \"" holmake-executable "\" ();")
+   hol-echo-commands-p))
+
+(defun hol-user-save-backup ()
+  "Saves the current status of the proof for later backups to this point."
+  (interactive)
+  (send-raw-string-to-hol "proofManagerLib.save()" hol-echo-commands-p))
+
+(defun hol-print-goal ()
+  "Print the current HOL goal."
+  (interactive)
+  (send-raw-string-to-hol "proofManagerLib.p()" hol-echo-commands-p))
+
+(defun hol-print-all-goals ()
+  "Print all the current HOL goals."
+  (interactive)
+  (send-raw-string-to-hol "proofManagerLib.status()" hol-echo-commands-p))
+
+(defun hol-interrupt ()
+  "Perform a HOL interrupt."
+  (interactive)
+  (let ((buf (ensure-hol-buffer-ok)))
+    (interrupt-process (get-buffer-process buf))))
+
+
+(defun hol-kill ()
+  "Kill HOL process."
+  (interactive)
+  (let ((buf (ensure-hol-buffer-ok)))
+    (kill-process (get-buffer-process buf))))
+
+(defun hol-recentre (arg)
+  "Display the HOL window in such a way that it displays most text, with the
+cursor at the bottom.
+With prefix arg, instead orient the HOL window so as to put the cursor in
+the middle of the window, and keep the cursor in its current position.
+
+If the variable `hol-raise-on-recentre' is non-nil, also raise the frame
+containing the HOL window, but keep the current frame uppermost."
+  (interactive "p")
+  (let ((f (selected-frame)))
+    (if (get-buffer-window hol-buffer-name t)
+        (save-mark-and-excursion
+          (select-window (get-buffer-window hol-buffer-name t))
+          (and hol-raise-on-recentre (progn (raise-frame) (raise-frame f)))
+          (if (= arg 1) (goto-char (point-max)))
+          (recenter (if (= arg 1) -1 nil))))))
+
+(defun hol-rotate (arg)
+  "Rotate the goal stack N times.  Once by default."
+  (interactive "p")
+  (send-raw-string-to-hol (format "proofManagerLib.r %d" arg)
+                          hol-echo-commands-p))
+
+(defun hol-scroll-up (arg)
+  "Scrolls the HOL window."
+  (interactive "P")
+  (ensure-hol-buffer-ok)
+  (save-excursion
+    (select-window (get-buffer-window hol-buffer-name t))
+    (scroll-up arg)))
+
+(defun hol-scroll-down (arg)
+  "Scrolls the HOL window."
+  (interactive "P")
+  (ensure-hol-buffer-ok)
+  (save-excursion
+    (select-window (get-buffer-window hol-buffer-name t))
+    (scroll-down arg)))
+
+(defun hol-use-file (filename)
+  "Gets HOL session to \"use\" a file."
+  (interactive "fFile to use: ")
+  (send-raw-string-to-hol (concat "use \"" filename "\";")
+                          hol-echo-commands-p))
+
+(defun hol-load-string (s)
+  "Loads the ML object file NAME.uo; checking that it isn't already loaded."
+  (let* ((buf (ensure-hol-buffer-ok))
+         (mys (format "%s" s)) ;; gets rid of text properties
+         (commandstring
+          (concat "val _ = if List.exists (fn s => s = \""
+                  mys
+                  "\") (emacs_hol_mode_loaded()) then () else "
+                  "(print  \"Loading " mys
+                  "\\n\"; " "Meta.load \"" mys "\");\n")))
+    (comint-send-string buf commandstring)))
+
+(defun hol-load-modules-in-region (start end)
+  "Attempts to load all of the words in the region as modules."
+  (interactive "rP")
+  (save-excursion
+    (goto-char start)
+    (while (re-search-forward (concat "\\b" sml-struct-id-regexp "\\b") end t)
+      (let ((ppss (syntax-ppss)))
+        (if (and (not (nth 4 ppss)) (not (nth 3 ppss)))
+            (hol-load-string (match-string 0)))))))
+
+(defun hol-load-file (arg)
+  "Gets HOL session to \"load\" the file at point.
+If there is no filename at point, then prompt for file.  If the region
+is active (in transient mark mode) and it looks like it might be a
+module name or a white-space delimited list of module names, then send
+region instead. With prefix ARG prompt for a file-name to load."
+  (interactive "P")
+  (let* ((wap (word-at-point))
+         (txt (condition-case nil
+                  (buffer-substring (region-beginning) (region-end))
+                (error nil))))
+    (cond (arg (hol-load-string (read-string "Library to load: ")))
+          ((and (is-region-active)
+                (string-match (concat "^\\(\\s-*" sml-struct-id-regexp
+                                      "\\)+\\s-*$") txt))
+           (hol-load-modules-in-region (region-beginning) (region-end)))
+          ((and wap (string-match "^\\w+$" wap)) (hol-load-string wap))
+          (t (hol-load-string (read-string "Library to load: "))))))
+
+
+(defun hol-mode-init-sml ()
+   (hol-toggle-quiet-quietdec)
+   (send-raw-string-to-hol hol-mode-sml-init-command nil)
+   (hol-toggle-quiet-quietdec))
+
+(defun turn-off-hol-font-lock (oldvar)
+  (interactive)
+  (if (not oldvar)
+      (progn
+        (message "Turning on font-lock mode does nothing in HOL mode")
+        (setq font-lock-defaults nil)))
+  (setq font-lock-mode nil))
+
+(require 'term)
+(defun holmake (&optional dir)
+  (interactive "DRun Holmake in dir: ")
+  (let ((holmake-buffer
+         (let ((holmake-buffer-candidate (get-buffer-create "*Holmake*")))
+           (if (get-buffer-process holmake-buffer-candidate)
+               (generate-new-buffer "*Holmake*")
+             holmake-buffer-candidate))))
+    (set-buffer holmake-buffer)
+    (cd dir)
+    (goto-char (point-max))
+    (setq buffer-read-only nil)
+    (delete-region (point-min) (point-max))
+    (insert "Running Holmake in directory " dir "\n\n")
+    (term-ansi-make-term
+     (buffer-name)
+     holmake-executable nil "--qof" "-k")
+    (term-mode)
+    (term-char-mode)
+    (display-buffer holmake-buffer '(nil (allow-no-window . t)))))
+
+;** hol map keys and function definitions
+(defun hol-executable-with-bare ()
+  (if hol-bare-p (concat hol-executable ".bare")
+                 hol-executable))
+
+(defun hol--looks-like-root-holdir (dir)
+  (cl-every
+   (lambda (s) (file-exists-p (concat (file-name-as-directory dir) s)))
+   '("COPYRIGHT" "tools" "tools-poly" "std.prelude" "bin")))
+
+(defun hol--find-alternate-executable (dir0 original-name0)
+  (let ((dir (expand-file-name dir0))
+        (original-name (expand-file-name original-name0)))
+    ;; check for lastmaker file
+    (if-let*
+        (((file-readable-p ".HOLMK/lastmaker"))
+         ((> 500 (file-attribute-size (file-attributes ".HOLMK/lastmaker"))))
+         (lines (with-temp-buffer
+                  (insert-file-contents-literally ".HOLMK/lastmaker")
+                  (split-string (buffer-string) "\n" t)))
+         ((not (null lines)))
+         (dir1 (file-name-directory (car lines)))
+         (name (concat dir1 "hol"))
+         ((not (equal name original-name))))
+        (list (concat dir1 "hol") "(honouring last build in this directory)")
+      (while (and (not (hol--looks-like-root-holdir dir))
+                  (not (equal "/" dir)))
+        (setq dir (file-name-directory (directory-file-name dir))))
+      (if (equal "/" dir) nil
+        (let ((bindir
+               (file-name-as-directory
+                (concat (file-name-as-directory dir) "bin"))))
+          (cond
+           ((equal (file-name-directory original-name) bindir) nil)
+           ((file-exists-p (concat bindir "hol.state"))
+            (list (concat bindir "hol") "(as we are in its HOL directory)"))
+           ((file-exists-p (concat bindir "hol.state0"))
+            (list
+             (concat bindir "hol.bare")
+             "(as we are in its HOL directory and hol.state doesn't exist)"))))))))
+
+(defun hol--get-executable ()
+  (let ((first-option (hol-executable-with-bare)))
+    (or (let ((alternate
+               (hol--find-alternate-executable default-directory first-option)))
+          (if alternate
+              (progn (message "Using %s as HOL executable %s"
+                              (car alternate) (cadr alternate))
+                     (sleep-for 1 500)
+                     (car alternate))))
+        first-option)))
+
+(defun hol (&optional display-actions display-alist)
+  "Runs a HOL session in a comint window."
+  (interactive)
+  (let* ((original-buffer (current-buffer))
+         (my-dir (or (ignore-errors (file-name-directory buffer-file-name))
+                     default-directory))
+         (hol-executable (hol--get-executable)))
+    (if (not (file-executable-p hol-executable))
+        (error "Wanted to execute %s as HOL, but can not find/execute it"
+               hol-executable))
+    (if (get-buffer hol-buffer-name)
+        (progn
+          (set-buffer hol-buffer-name)
+          (if (hol-buffer-ok hol-buffer-name)
+              (progn
+                (message "Killing existing HOL process")
+                (comint-send-eof)
+                (sleep-for 0 500)))
+          (setq default-directory my-dir)
+          (make-comint-in-buffer "HOL" hol-buffer-name hol-executable))
+      (let* ((buf (make-comint "HOL" hol-executable)))
+        (setq hol-buffer-name (buffer-name buf))
+        (set-buffer hol-buffer-name)))
+
+    (setq comint-prompt-regexp "^- ")
+    ;; must go to ridiculous lengths to ensure that font-lock-mode is
+    ;; turned off and stays off
+    (font-lock-mode 0)
+    (make-local-variable 'font-lock-function)
+    (setq font-lock-function 'turn-off-hol-font-lock)
+    (make-local-variable 'comint-preoutput-filter-functions)
+    (holpp-quiet-reset)
+    (setq comint-preoutput-filter-functions '(holpp-output-filter))
+    (setq comint-scroll-show-maximum-output t)
+    (setq comint-scroll-to-bottom-on-output t)
+    (hol-mode-init-sml)
+    (send-raw-string-to-hol
+     "val _ = Parse.current_backend := PPBackEnd.emacs_terminal;" nil)
+    (if hol-show-tooltips-in-minibuffer
+       (progn (setq help-at-pt-display-when-idle t)
+              (help-at-pt-set-timer)))
+
+    (if (eq (get-buffer hol-buffer-name) original-buffer)
+        nil
+      (display-buffer hol-buffer-name
+                      (cons
+                       (append display-actions
+                               '(display-buffer-use-some-frame
+                                 display-buffer-pop-up-frame))
+                       display-alist))
+      (select-frame-set-input-focus
+       (window-frame (get-buffer-window original-buffer t))))))
+
+(defun hol-toggle-bare ()
+  "Toggles the elisp variable 'hol-bare-p."
+  (interactive)
+  (setq hol-bare-p (not hol-bare-p))
+  (concat "using " (hol-executable-with-bare)))
+
+(defun hol-display ()
+   "Attempts to bring the HOL buffer to the fore (calling `display-buffer')."
+   (interactive)
+   (display-buffer hol-buffer-name))
+
+(defun hol-vertical ()
+  "Runs a HOL session after splitting the window"
+  (interactive)
+  (hol '(display-buffer-below-selected)))
+
+(defun hol-horizontal ()
+  "Runs a HOL session after splitting the window"
+  (interactive)
+  (hol '(display-buffer-reuse-window
+         (lambda (b al)
+           (let ((split-height-threshold nil)
+                 (split-width-threshold 0))
+             (display-buffer-pop-up-window b al))))
+       '((window-width . 83) (reusable-frames . nil))))
+
+(defvar hol-new-buffer-style hol-new-buffer-style-default)
+
+(setq hol-new-buffer-style-alist
+      '((horizontal . hol-horizontal)
+        (vertical . hol-vertical)
+        (new-frame . hol)))
+
+(defun hol-with-region ()
+  "Starts a HOL session and pastes selected region into it. If there is no active region, pastes whole buffer."
+  (interactive)
+  (let* ((style-str (completing-read
+                     (concat "HOL buffer position ("
+                             (symbol-name hol-new-buffer-style)
+                             "): ")
+                     '("horizontal" "vertical" "new-frame")
+                     nil
+                     t
+                     nil
+                     nil
+                     (symbol-name hol-new-buffer-style)
+                     t))
+         (style (intern style-str))
+         (starter (cdr (assoc style hol-new-buffer-style-alist))))
+    (setq hol-new-buffer-style style)
+    (save-mark-and-excursion (funcall starter))
+    (if (region-active-p)
+        (copy-region-as-hol-definition (region-beginning) (region-end) 16 t)
+      (let ((beg (point-min))
+            (end (progn
+                   (while (looking-at "[[:space:]]*\n") (forward-line 1))
+                   (search-backward "\n\n")
+                   (while (looking-at "[[:space:]]*\n") (forward-line 1))
+                   (point))))
+        (push-mark (point-min))
+        (activate-mark t)
+        (copy-region-as-hol-definition beg end 16 t)))))
+
+(defun run-program (filename niceness)
+  "Runs a PROGRAM in a comint window, with a given (optional) NICENESS."
+  (interactive "fProgram to run: \nP")
+  (let* ((niceval (cond ((null niceness) 0)
+                        ((listp niceness) 10)
+                        (t (prefix-numeric-value niceness))))
+         (progname (format "%s(n:%d)"
+                          (file-name-nondirectory filename)
+                          niceval))
+         (buf (cond ((> niceval 0)
+                     (make-comint progname "nice" nil
+                                  (format "-%d" niceval)
+                                  (expand-file-name filename)))
+                   (t (make-comint progname
+                                   (expand-file-name filename)
+                                   nil)))))
+    (switch-to-buffer buf)))
+
+(defun hol-toggle-var (s)
+  "Toggles the boolean variable STRING."
+  (message (concat "Toggling " s))
+  (send-raw-string-to-hol
+   (format (concat "val _ = (%s := not (!%s);"
+                   "print (\"*** %s now \" ^"
+                   "Bool.toString (!%s)^\" ***\\n\"))")
+           s s s s)
+   nil))
+
+(defun hol-toggle-var-quiet (s)
+  "Toggles the boolean variable STRING."
+  (send-raw-string-to-hol
+   (format "val _ = (%s := not (!%s));" s s) nil))
+
+(defun hol-toggle-trace (s &optional arg)
+  "Toggles the trace variable STRING between zero and non-zero.  With prefix
+argument N, sets the trace to that value in particular."
+  (interactive "sTrace name: \nP")
+  (if (null arg)
+      (progn
+        (message (concat "Toggling " s))
+        (send-raw-string-to-hol
+         (format "local open Int in
+                  val _ = let val nm = \"%s\"
+                      fun findfn r = #name r = nm
+                      val old =
+                            #trace_level (valOf (List.find findfn (traces())))
+                  in
+                      print (\"** \"^nm^\" trace now \");
+                      if 0 < old then (set_trace nm 0; print \"off\\n\")
+                      else (set_trace nm 1; print \"on\\n\")
+                  end handle Option =>
+                        print \"** No such trace var: \\\"%s\\\"\\n\"
+                  end" s s)
+         nil))
+    (let ((n (prefix-numeric-value arg)))
+      (message (format "Setting %s to %d" s n))
+      (send-raw-string-to-hol
+       (format "val _ = (set_trace \"%s\" %d; print \"** %s trace now %d\\n\")
+                        handle HOL_ERR _ =>
+                           print \"** No such trace var: \\\"%s\\\"\\n\""
+               s n s n s)
+       nil))))
+
+(defun hol-toggle-unicode ()
+  "Toggles the \"Unicode\" trace."
+  (interactive)
+  (hol-toggle-trace "Unicode"))
+
+(defun hol-toggle-emacs-tooltips ()
+  "Toggles whether HOL produces tooltip information while pretty-printing."
+  (interactive)
+  (hol-toggle-trace "PPBackEnd show types"))
+
+(defun hol-toggle-pp-styles ()
+  "Toggles whether HOL produces style informations while pretty-printing."
+  (interactive)
+  (hol-toggle-trace "PPBackEnd use styles"))
+
+(defun hol-toggle-pp-cases ()
+  "Toggles the \"pp_cases\" trace."
+  (interactive)
+  (hol-toggle-trace "pp_cases")
+  (hol-toggle-trace "use pmatch_pp"))
+
+(defun hol-toggle-pp-annotations ()
+  "Toggles whether HOL produces annotations while pretty-printing."
+  (interactive)
+  (hol-toggle-trace "PPBackEnd use annotations"))
+
+(defun hol-toggle-goalstack-fvs ()
+  "Toggles the trace \"Goalstack.print_goal_fvs\"."
+  (interactive)
+  (hol-toggle-trace "Goalstack.print_goal_fvs"))
+
+(defun hol-toggle-goalstack-print-goal-at-top ()
+  "Toggles the trace \"Goalstack.print_goal_at_top\"."
+  (interactive)
+  (hol-toggle-trace "Goalstack.print_goal_at_top"))
+
+(defun hol-toggle-goalstack-num-assums (arg)
+  "Toggles the number of assumptions shown in a goal."
+  (interactive "nMax. number of visible assumptions: ")
+  (hol-toggle-trace "Goalstack.howmany_printed_assums" arg))
+
+(defun hol-toggle-goalstack-num-subgoals (arg)
+  "Toggles the number of shown subgoals."
+  (interactive "nMax. number of shown subgoals: ")
+  (hol-toggle-trace "Goalstack.howmany_printed_subgoals" arg))
+
+(defun hol-toggle-simplifier-trace (arg)
+  "Toggles the trace \"simplifier\".  With ARG sets trace to this value."
+  (interactive "P")
+  (hol-toggle-trace "simplifier" arg))
+
+(defun hol-toggle-show-types (arg)
+  "Toggles the global show_types variable. With prefix ARG sets trace to this value (setting trace to 2, is the same as setting the show_types_verbosely variable)."
+  (interactive "P")
+  (hol-toggle-trace "types" arg))
+
+(defun hol-toggle-show-types-verbosely ()
+  "Toggles the global show_types_verbosely variable."
+  (interactive)
+  (hol-toggle-var "Globals.show_types_verbosely"))
+
+(defun hol-toggle-show-numeral-types()
+  "Toggles the global show_numeral_types variable."
+  (interactive)
+  (hol-toggle-var "Globals.show_numeral_types"))
+
+(defun hol-toggle-show-assums()
+  "Toggles the global show_assums variable."
+  (interactive)
+  (hol-toggle-var "Globals.show_assums"))
+
+(defun hol-toggle-show-tags()
+  "Toggles the global show_tags variable."
+  (interactive)
+  (hol-toggle-var "Globals.show_tags"))
+
+(defun hol-toggle-show-axioms()
+  "Toggles the global show_axioms variable."
+  (interactive)
+  (hol-toggle-var "Globals.show_axioms"))
+
+(defun hol-toggle-quietdec ()
+  "Toggles quiet declarations in the interactive system."
+  (interactive)
+  (message "Toggling 'Quiet declaration'")
+  (send-raw-string-to-hol
+   (concat
+    "val _ = print (\"*** 'Quiet declaration' now \" ^"
+    "Bool.toString (HOL_Interactive.toggle_quietdec()) ^ \" ***\\n\")")
+   nil)
+  (hol-toggle-var "Globals.interactive"))
+
+(defun hol-toggle-quiet-quietdec ()
+  "Toggles quiet declarations in the interactive system."
+  (interactive)
+  (send-raw-string-to-hol "val _ = HOL_Interactive.toggle_quietdec()" nil)
+  (hol-toggle-var-quiet "Globals.interactive"))
+
+(defun hol-toggle-show-times()
+  "Toggles the elisp variable 'hol-emit-time-elapsed-p."
+  (interactive)
+  (setq hol-emit-time-elapsed-p (not hol-emit-time-elapsed-p))
+  (message (if hol-emit-time-elapsed-p "Elapsed times WILL be displayed"
+             "Elapsed times WON'T be displayed")))
+
+(defun hol-toggle-echo-commands ()
+  "Toggles the elisp variable 'hol-echo-commands-p."
+  (interactive)
+  (setq hol-echo-commands-p (not hol-echo-commands-p))
+  (message (if hol-echo-commands-p "Commands WILL be echoed"
+             "Commands WON'T be echoed")))
+
+(defun hol-toggle-auto-load ()
+  "Toggles the elisp variable 'hol-auto-load-p."
+  (interactive)
+  (setq hol-auto-load-p (not hol-auto-load-p))
+  (message (if hol-auto-load-p "automatic loading ON"
+             "automatic loading OFF")))
+
+(defun hol-toggle-ppbackend ()
+  "Toggles between using the Emacs and \"raw\" terminal pretty-printing."
+  (interactive)
+  (send-raw-string-to-hol
+   (concat
+    "val _ = if #name (#extras (!Parse.current_backend)) = \"emacs_terminal\" then"
+    "(Parse.current_backend := PPBackEnd.raw_terminal;"
+    "print \"*** PP Backend now \\\"raw\\\" ***\\n\")"
+    "else (Parse.current_backend := PPBackEnd.emacs_terminal;"
+    "print \"*** PP Backend now \\\"emacs\\\" ***\\n\")")
+   nil))
+
+(defun hol-restart-goal ()
+  "Restarts the current goal."
+  (interactive)
+  (send-raw-string-to-hol "proofManagerLib.restart()" hol-echo-commands-p))
+
+(defun hol-drop-goal ()
+  "Drops the current goal."
+  (interactive)
+  (send-raw-string-to-hol "proofManagerLib.drop()" hol-echo-commands-p))
+
+(defun hol-open-string (prefixp)
+  "Opens HOL modules, prompting for the name of the module to load.
+With prefix ARG, toggles quietdec variable before and after opening,
+potentially saving a great deal of time as tediously large modules are
+printed out.  (That's assuming that quietdec is false to start with.)"
+  (interactive "P")
+  (let* ((prompt0 "Name of module to (load and) open")
+         (prompt (concat prompt0 (if prefixp " (toggling quietness)") ": "))
+         (module-name (read-string prompt)))
+    (hol-load-string module-name)
+    (if prefixp (hol-toggle-quietdec))
+    (send-raw-string-to-hol (concat "open " module-name) hol-echo-commands-p)
+    (if prefixp (hol-toggle-quietdec))))
+
+(defun hol-db-match (tm)
+  "Does a DB.match [] on the given TERM (given as a string, without quotes) and formats the result nicely."
+  (interactive "sTerm to match on: ")
+  (send-raw-string-to-hol (format "Hol_pp.print_match [] (Term`%s`)" tm)
+                          hol-echo-commands-p))
+
+(defun hol-check-dbselector (s)
+  (if (string-prefix-p "'" s) (string-suffix-p "'" s)
+    (if (string-prefix-p "\"" s) (string-suffix-p "\"" s)
+      t)))
+
+(defun hol-make-db-select-string (args)
+  (let ((sels (mapconcat (lambda (s) (if (string-prefix-p "'" s)
+                                      (concat "DB.SelTHY \""
+                                              (substring s 1 -1) "\"")
+                                    (if (string-prefix-p "\"" s)
+                                        (concat "DB.SelNM \""
+                                                (substring s 1 -1) "\"")
+                                      (concat "DB.SelTM “" s "”"))))
+                         args ", ")))
+    (concat "DB.selectDB [" sels "]")))
+
+(defconst hol-db-select-info "('thy'; \"name\"; term pattern)" "")
+(defun hol-db-select (arg1)
+  "Calls DB.selectDB on the sequence of `selectors' provided.
+A selector is a string (as per DB.find) that matches against the name of
+the theorem, given in double quotes; a theory name, given in single quotes,
+or a term pattern, given without delimiters."
+  (interactive "sFirst selector pattern('thy'; \"name\"; term pattern): ")
+  (or (string-equal arg1 "")
+      (and (not (hol-check-dbselector arg1))
+           (error "Malformed DB selector: %s" arg1))
+      (let ((args (list arg1)) next-arg)
+        (while (and (setq next-arg
+                          (read-string (concat "Next DB selector"
+                                               hol-db-select-info
+                                               ": ")))
+                    (not (string-equal next-arg "")))
+          (if (hol-check-dbselector next-arg)
+              (setq args (cons next-arg args))
+            (error "Malformed DB selector: %s" next-arg)))
+        (send-string-to-hol (hol-make-db-select-string args)))))
+
+(defun hol-db-find (tm)
+  "Does a DB.find on the given string and formats the result nicely."
+  (interactive "sTheorem name part: ")
+  (send-raw-string-to-hol (format "Hol_pp.print_find \"%s\"" tm)
+                          hol-echo-commands-p))
+
+(defun hol-db-check (ty)
+  "Does a sanity check on the current theory."
+  (interactive "sTheory name: ")
+  (send-raw-string-to-hol (format "Sanity.sanity_check_theory \"%s\"" ty)
+                          hol-echo-commands-p))
+
+(defun hol-db-check-current ()
+  "Does a sanity check on the current theory."
+  (interactive)
+  (send-raw-string-to-hol "Sanity.sanity_check()" hol-echo-commands-p))
+
+(defun hol-db-find-consts (ty)
+  "Does bossLib.find_consts on a given type and prints the result."
+  (interactive "sType of constant: ")
+  (send-raw-string-to-hol (format "bossLib.find_consts ``%s``" ty)
+                          hol-echo-commands-p))
+
+(defun hol-drop-all-goals ()
+  "Drops all HOL goals from the current proofs object."
+  (interactive)
+  (send-raw-string-to-hol "proofManagerLib.drop_all()" hol-echo-commands-p))
+
+(defun hol-subgoal-tactic (p)
+  "Without a prefix argument, sends term at point (delimited by backquote
+characters) as a subgoal to prove.  Will usually create at least two sub-
+goals; one will be the term just sent, and the others will be the term sent
+STRIP_ASSUME'd onto the assumption list of the old goal.  This mimicks what
+happens with the \"by\" command.
+
+With a prefix argument, sends the delimited term as if the
+argument of a \"suffices_by\" command, making two new goals: the
+first is to show that the new term implies the old goal, and the
+second is to show the new term.
+
+(Loads the BasicProvers module if not already loaded.)"
+  (interactive "P")
+  (let ((tactic (if p "Tactical.Q_TAC Tactic.SUFF_TAC"
+                      "(fn q => BasicProvers.byA(q,ALL_TAC))")))
+    (send-string-to-hol
+     (format "proofManagerLib.e (%s `%s`)"
+             tactic
+             (hol-term-at-point)))))
+
+
+;; (defun hol-return-key ()
+;;   "Run comint-send-input, but only if both: the user is editting the
+;; last command in the buffer, and that command ends with a semicolon.
+;; Otherwise, insert a newline at point."
+;;   (interactive)
+;;   (let ((comand-finished
+;;          (let ((process (get-buffer-process (current-buffer))))
+;;            (and (not (null process))
+;;                 (let ((pmarkpos (marker-position
+;;                                  (process-mark process))))
+;;                   (and (< (point) pmarkpos)
+;;                        (string-match ";[ \t\n\r]*$"
+;;                                      (buffer-substring pmarkpos
+;;                                                        (point-max)))))))))
+;;     (if command-finished
+;;         (progn
+;;           (goto-char (point-max))
+;;           (comint-send-input))
+;;       (insert "\n"))))
+
+;; (define-key comint-mode-map "\r" 'hol-return-key)
+
+(defun hol-overload-info-for (term-name)
+  "Get HOL to print overload information for term-name"
+  (interactive "sOverloaded name: ")
+  (send-string-to-hol (format "overload_info_for \"%s\"" term-name)))
+
+
+;;load-path
+(defun ml-quote (s)
+   (let* (
+     (s1 (replace-regexp-in-string "\\\\" "\\\\\\\\" s))
+     (s2 (replace-regexp-in-string "\n" "\\\\n" s1))
+     (s3 (replace-regexp-in-string "\t" "\\\\t" s2))
+     (s4 (replace-regexp-in-string "\"" "\\\\\"" s3))
+   ) s4))
+
+(defun hol-add-load-path (path)
+  (interactive "DAdd new load-path: ")
+  (let ((epath (expand-file-name path)))
+  (if (file-accessible-directory-p epath)
+     (progn
+        (send-raw-string-to-hol
+            (concat "loadPath := \"" (ml-quote epath) "\" :: !loadPath;")
+            nil)
+        (message (concat "Load-path \"" epath "\" added.")))
+     (progn (ding) (message "Not a directory!")))
+))
+
+
+(defun hol-show-current-load-paths ()
+   (interactive)
+   (send-raw-string-to-hol "print_current_load_paths ()" nil))
+
+(defun hol-type-info ()
+   "Gives informations about the type of a term"
+   (interactive)
+   (let* ((txt (buffer-substring-no-properties (region-beginning) (region-end)))
+          (use-marked (and (is-region-active) (= (cl-count ?\` txt) 0)))
+          (at-point-term (thing-at-point 'hol-term))
+
+          (main-term (ml-quote (if use-marked txt at-point-term)))
+          (context-term (ml-quote (if use-marked at-point-term "")))
+          (command-s (concat "print_type_of_in_context true "
+                      (if use-marked (concat "(SOME \"" context-term "\")") "NONE")
+                      " \"" main-term "\"")))
+   (send-raw-string-to-hol command-s nil)))
+
+
+(defun holpp-decode-color (code)
+  (cond ((equal code "0") "#000000")
+        ((equal code "1") "#840000")
+        ((equal code "2") "#008400")
+        ((equal code "3") "#848400")
+        ((equal code "4") "#000084")
+        ((equal code "5") "#840084")
+        ((equal code "6") "#008484")
+        ((equal code "7") "#555555")
+        ((equal code "8") "#949494")
+        ((equal code "9") "#FF0000")
+        ((equal code "A") "#00C600")
+        ((equal code "B") "#FFFF00")
+        ((equal code "C") "#0000FF")
+        ((equal code "D") "#FF00FF")
+        ((equal code "E") "#00FFFF")
+        ((equal code "F") "#FFFFFF")
+))
+
+(defun holpp-decode-full-style (style)
+   (let* (
+       (fg (substring style 0 1))
+       (bg (substring style 1 2))
+       (b (substring style 2 3))
+       (u (substring style 3 4))
+       (fg-face (if (equal fg "-") nil
+                    (cons :foreground (cons (holpp-decode-color fg) ()))))
+       (bg-face (if (equal bg "-") nil
+                    (cons :background (cons (holpp-decode-color bg) ()))))
+       (b-face  (if (equal b "-") nil
+                    (cons :weight (cons 'bold ()))))
+       (u-face  (if (equal u "-") nil
+                    (cons :underline (cons t ())))))
+       (cons 'face (cons (append fg-face bg-face b-face u-face) ()))))
+
+
+(defun holpp-find-comment-end (n)
+   (if (not (re-search-forward "\\((\\*(\\*(\\*\\)\\|\\(\\*)\\*)\\*)\\)" nil t 1))
+       nil
+       (if (save-excursion (goto-char (- (point) 6))
+                           (looking-at "(\\*(\\*(\\*"))
+           (progn
+              (holpp-find-comment-end (+ n 1)))
+           (if (= n 1) t (holpp-find-comment-end (- n 1))))))
+
+(defun holpp-execute-code-face-tooltip (start end toolprop codeface)
+  (let ((tooltipprop
+         (if (equal toolprop nil) nil (list 'help-echo toolprop))))
+    (add-text-properties start end (append codeface tooltipprop))))
+
+(defun holpp-execute-code (code arg1 start end)
+  (cond ((equal code "FV")
+             (holpp-execute-code-face-tooltip start end arg1
+             '(face hol-free-variable)))
+        ((equal code "BV")
+             (holpp-execute-code-face-tooltip start end arg1
+             '(face hol-bound-variable)))
+        ((equal code "TV")
+             (holpp-execute-code-face-tooltip start end arg1
+             '(face hol-type-variable)))
+        ((equal code "TY")
+             (holpp-execute-code-face-tooltip start end arg1
+             '(face hol-type)))
+        ((equal code "CO")
+         (holpp-execute-code-face-tooltip start end arg1 nil))
+        ((equal code "ST")
+           (add-text-properties start end
+             (holpp-decode-full-style arg1)))))
+
+(setq temp-hol-output-buf nil)
+
+(defun holpp-quiet-reset ()
+  (let ((tmpbuf (or temp-hol-output-buf
+                     (generate-new-buffer " *HOL output filter*)"))))
+      (setq temp-hol-output-buf tmpbuf)
+      (with-current-buffer tmpbuf
+        (delete-region (point-min) (point-max)))))
+
+(defun holpp-reset ()
+  (interactive)
+  (holpp-quiet-reset)
+  (send-raw-string-to-hol "print \"\\n\\n*** hol-mode reset ***\\n\";" nil))
+
+; this filter function is complicated by the fact that comint chunks
+; output (in 1024 character chunks in my tests) and so doesn't
+; necessarily give complete (in the sense of containing matching
+; comment-blocks) strings to the filter. This means that a solution
+; with with-temp-buffer won't work. Instead, there is a persistent
+; working space buffer, and if the code finds a non-matching comment
+; start (a "(*(*(*" substring), it just leaves that in the working
+; space so that the next piece of output can be appended and processed
+; properly.
+(defun holpp-output-filter (s)
+  "Converts a munged emacs_terminal string into a pretty one with text properties."
+  (interactive "sinput: ")
+  (let* ((tmpbuf (or temp-hol-output-buf
+                     (generate-new-buffer " *HOL output filter*)")))
+         end)
+    (setq temp-hol-output-buf tmpbuf)
+    (with-current-buffer tmpbuf
+      (unwind-protect
+          (progn
+            (goto-char (point-max))
+            (insert s)
+            (goto-char (point-min))
+            (while (and (not end) (search-forward "(*(*(*" nil t))
+              (let ((uptoann (- (point) 6))
+                    (start (point)))
+                (if (not (holpp-find-comment-end 1))
+                    (progn
+                      (goto-char uptoann)
+                      (setq end t))
+                  (delete-region uptoann start)
+                  (let*
+                      ((start (- start 6))
+                       (code (buffer-substring start (+ start 2)))
+                       (argument
+                        (save-excursion
+                          (goto-char (+ start 2))
+                          (if (equal (following-char) 0)
+                              (progn
+                                (goto-char (+ (point) 1))
+                                (skip-chars-forward "^\^@")
+                                (prog1
+                                    (if (equal (+ start 3) (point)) nil
+                                    (buffer-substring (+ start 3)
+                                                            (point)))
+                                  (delete-region (+ start 2) (1+ (point)))))
+                            nil))))
+                       (holpp-execute-code code argument
+                        (+ start 2)
+                        (- (point) 6))
+                       (delete-region start (+ start 2))
+                       (delete-region (- (point) 6) (point))
+                       (goto-char start)))))
+            (if (not end)
+                (progn
+                  (goto-char (point-max))
+                  (skip-chars-backward "(*")))
+            (prog1
+                (buffer-substring (point-min) (point))
+              (delete-region (point-min) (point))))))))
+
+(defun holmakepp-mark-error (start end)
+   (add-text-properties start end '(face holmake-error)))
+
+
+(defun holmakepp-mark-mosml-error ()
+  (interactive)
+  (goto-char (point-min))
+  (while (re-search-forward "^!" nil t)
+     (let* ((start (match-beginning 0)))
+     (forward-line)
+     (while (or (looking-at "!") (looking-at " ")) (forward-line))
+     (holmakepp-mark-error start (- (point) 1))))
+)
+
+(setq temp-holmake-output-buf nil)
+(defun holmakepp-output-filter (s)
+  "Converts a munged emacs_terminal string into a pretty one with text properties."
+  (interactive "sinput: ")
+  (let* ((tmpbuf (or temp-holmake-output-buf
+                     (generate-new-buffer " *HOLMAKE output filter*)")))
+         end)
+    (setq temp-holmake-output-buf tmpbuf)
+    (with-current-buffer tmpbuf
+      (unwind-protect
+          (progn
+            (goto-char (point-max))
+            (insert s)
+            (holmakepp-mark-mosml-error)
+            (prog1
+                (buffer-substring (point-min) (point-max))
+              (delete-region (point-min) (point-max))))))))
+
+(add-hook 'sml-mode-hook
+          (lambda ()
+            (local-set-key "`" 'holscript-dbl-backquote)
+            (message "Running HOL SML hook")
+))
+
+(defun hol-find-quoted-material (limit)
+  (let ((beginmatch (re-search-forward hol-term-begin-re limit t))
+        (ppss (syntax-ppss)))
+    (while (and beginmatch (or (nth 3 ppss) (nth 4 ppss)))
+      (setq beginmatch (re-search-forward hol-term-begin-re limit t))
+      (setq ppss (syntax-ppss)))
+    (if (not beginmatch) nil
+      (let* ((start-delim (match-string-no-properties 0))
+             (begin-marker
+              (if (= (length start-delim) 1)
+                  (set-marker (make-marker) (1- (point)))
+                (point-marker)))
+             (endre (hol-term-matching-delim start-delim))
+             (endmatch (if endre (re-search-forward endre limit t)
+                         (message (format "No end-delim for %s" start-delim))
+                         nil)))
+        (if (not endmatch) nil
+          (if (= (length start-delim) 1) nil (goto-char (match-beginning 0)))
+          (set-match-data (list begin-marker (point-marker)))
+          t)))))
+;  (re-search-forward "^Theorem[[:space:]]+[A-Za-z0-9'_]+\\(?:\\[[A-Za-z0-9_,]+\\]\\)?[[:space:]]*:\\(\\(?:\n  \\|.\\)+\\)\nProof" limit t))
+
+(defun hol-thm-prefix (s)
+  (or (string-prefix-p "Theorem" s) (string-prefix-p "Triviality" s)))
+(defun hol-defn-prefix (s) (string-prefix-p "Definition" s))
+(defun hol-indn-prefix (s)
+  (or (string-prefix-p "Inductive" s) (string-prefix-p "CoInductive" s)))
+
+(defun hol-term-matching-delim (start-delim)
+  (pcase start-delim
+    ("“" "”")
+    ("‘" "’")
+    ("Datatype:" "^End\\>")
+    ((pred hol-thm-prefix) "^Proof\\>")
+    ((pred hol-indn-prefix) "^End\\>")
+    ((pred hol-defn-prefix) "^Termination\\>\\|^End\\>")))
+
+
+(defgroup hol-faces nil "Faces used in pretty-printing HOL values"
+  :group 'faces
+  :group 'hol)
+
+(defface holmake-error
+  '((((class color))
+     :foreground "red"
+     :weight bold))
+  "The face for errors shown by HOLMAKE."
+  :group 'hol-faces)
+
+(defface hol-free-variable
+  '((((class color))
+     :foreground "blue"
+     :weight bold))
+  "The face for presenting free variables in HOL terms."
+  :group 'hol-faces)
+
+(defface hol-bound-variable
+  '((((class color))
+     :foreground "#009900"))
+  "The face for presenting bound variables in HOL terms."
+  :group 'hol-faces)
+
+(defface hol-type-variable
+  '((((class color))
+     :foreground "purple"
+     :slant italic))
+  "The face for presenting free type variables in HOL terms."
+  :group 'hol-faces)
+
+(defface hol-type
+  '((((class color))
+     :foreground "cyan3"
+     :slant italic))
+  "The face for presenting HOL types."
+  :group 'hol-faces)
+
+(defun hol-region-to-unicode-pdf (filename beg end)
+  "Print region to FILE as a PDF, handling Unicode characters."
+  (interactive "FFile to write to: \nr")
+  (if (and transient-mark-mode (not mark-active))
+      (error "No active region"))
+  (let* ((temp-ps-file (make-temp-file "holprint" nil ".ps"))
+         (lpr-switches
+          (list "-font" hol-unicode-print-font-filename
+                "-out" temp-ps-file))
+         (lpr-add-switches nil)
+         (lpr-command "uniprint"))
+    (lpr-region beg end)
+    (shell-command (concat "ps2pdf " temp-ps-file " " filename))
+    (delete-file temp-ps-file)))
+
+(setq hol-term-beginend-re
+      (concat
+       (regexp-opt
+        '("Theorem" "End" "Definition" "Inductive" "Termination" "Proof"
+          "CoInductive" "Datatype" "Triviality") "^\\(")
+       "\\|"
+       (regexp-opt '("“" "‘" "”" "’"))))
+(defvar hol-term-end-re (regexp-opt '("End" "Termination" "Proof" "”" "’")))
+(defvar hol-term-begin-re
+  (concat
+   (regexp-opt '("“" "‘")) "\\|"
+   hol-quoted-theorem-proof-re-begin "\\|"
+   hol-quoted-definition-re-begin "\\|"
+   "Datatype[[:space:]]*:"))
+
+(defun hol-fl-term-bump-backwards (pos)
+  (save-excursion
+    (goto-char pos)
+    (let ((match (re-search-backward hol-term-beginend-re nil t)))
+      (if (not match) pos
+        (if (looking-at hol-term-end-re) pos
+          (if (looking-at hol-term-begin-re) (match-beginning 0) pos))))))
+
+(defun hol-fl-term-bump-forwards (pos)
+  (save-excursion
+    (goto-char pos)
+    (let ((match (re-search-forward hol-term-beginend-re nil t)))
+      (if (not match) pos
+        (goto-char (match-beginning 0))
+        (if (looking-at hol-term-begin-re) pos
+          (if (looking-at hol-term-end-re) (match-end 0) pos))))))
+
+(defun hol-select-pattern-list-tactic (begin end)
+  "Send current region (which must include the delimiting square
+brackets) as argument to Q.SELECT_GOAL_LT, which list-tactic
+takes a list of patterns to use to select the desired current
+goal. If the region is not active, instead scan for a term in
+the surrounding text (as done by ‘hol-do-goal’ and
+‘hol-subgoal-tactic’)."
+  (interactive "r")
+  (let ((tosend
+         (if (and begin (region-active-p))
+             (buffer-substring-no-properties begin end)
+           (format "[‘%s’]" (hol-term-at-point)))))
+    (send-raw-string-to-hol
+     (format "proofManagerLib.expand_list (Q.SELECT_GOAL_LT %s)" tosend)
+     hol-echo-commands-p)))
+
+;;The key combinations
+(define-key global-map "\M-h" 'hol-map)
+(define-key global-map (kbd "C-M-h") 'hol-movement-map)
+(define-prefix-command 'holpp-map)
+
+
+(define-key hol-map "\C-c" 'hol-interrupt)
+(define-key hol-map "\C-l" 'hol-recentre)
+(define-key hol-map "\C-q" 'hol-toggle-quietdec)
+(define-key hol-map "\C-s" 'hol-toggle-simplifier-trace)
+(define-key hol-map "\C-v" 'hol-scroll-up)
+(define-key hol-map "\M-r" 'copy-region-as-hol-definition)
+(define-key hol-map "\C-r" 'hol-what-was-copy-region-as-hol-definition-quietly)
+(define-key hol-map "\M-p" 'hol-select-pattern-list-tactic)
+(define-key hol-map "\M-P" 'holpp-map)
+(define-key hol-map "\M-t" 'hol-toggle-show-times)
+(define-key hol-map "\M-s" 'hol-subgoal-tactic)
+(define-key hol-map "\M-v" 'hol-scroll-down)
+(define-key hol-map "b"    'hol-backup)
+(define-key hol-map "B"    'hol-user-backup)
+(define-key hol-map "S"    'hol-user-save-backup)
+(define-key hol-map "d"    'hol-drop-goal)
+(define-key hol-map "D"    'hol-drop-all-goals)
+(define-key hol-map "e"    'copy-region-as-hol-tactic)
+(define-key hol-map "\M-e" 'hol-find-eval-next-tactic)
+(define-key hol-map "E"    'copy-region-as-goaltree-tactic)
+(define-key hol-map "g"    'hol-do-goal)
+(define-key hol-map "G"    'hol-do-goaltree)
+(define-key hol-map "h"    'hol)
+(define-key hol-map "H"    'hol-with-region)
+(define-key hol-map "\M-m" 'holmake)
+(define-key hol-map "2"    'hol-vertical)
+(define-key hol-map "3"    'hol-horizontal)
+(define-key hol-map "4"    'hol-display)
+(define-key hol-map "l"    'hol-load-file)
+(define-key hol-map "m"    'hol-db-match)
+(define-key hol-map "M"    'hol-db-select)
+(define-key hol-map "f"    'hol-db-find)
+(define-key hol-map "c" 'hol-db-find-consts)
+(define-key hol-map "n"    'hol-name-top-theorem)
+(define-key hol-map "o"    'hol-open-string)
+(define-key hol-map "O"    'hol-overload-info-for)
+(define-key hol-map "p"    'hol-print-goal)
+(define-key hol-map "P"    'hol-print-all-goals)
+(define-key hol-map "r"    'hol-rotate)
+(define-key hol-map "R"    'hol-restart-goal)
+(define-key hol-map "t"    'mark-hol-tactic)
+(define-key hol-map "T"    'hol-start-termination-proof)
+(define-key hol-map "i"    'hol-type-info)
+(define-key hol-map "s"    'interactive-send-string-to-hol)
+(define-key hol-map "u"    'hol-use-file)
+(define-key hol-map "C"    'hol-db-check-current)
+(define-key hol-map "a"    'hol-remove-unicode)
+(define-key hol-map "*"    'hol-template-comment-star)
+(define-key hol-map "-"    'hol-template-comment-minus)
+(define-key hol-map "="    'hol-template-comment-equal)
+(define-key hol-map "\M-c" 'hol-template-hol-coreln)
+(define-key hol-map "\M-d" 'hol-template-define)
+(define-key hol-map "\M-i" 'hol-template-hol-reln)
+(define-key hol-map "\M-x" 'hol-template-store-thm)
+
+
+(define-key hol-map   "\C-a" 'hol-toggle-show-assums)
+(define-key holpp-map "a"    'hol-toggle-show-assums)
+(define-key hol-map   "\C-t" 'hol-toggle-show-types)
+(define-key holpp-map "\C-t" 'hol-toggle-show-types)
+(define-key hol-map   "\C-n" 'hol-toggle-show-numeral-types)
+(define-key holpp-map "n"    'hol-toggle-show-numeral-types)
+(define-key hol-map   "\C-f" 'hol-toggle-goalstack-fvs)
+(define-key holpp-map "f"    'hol-toggle-goalstack-fvs)
+(define-key hol-map   "\C-o" 'hol-toggle-goalstack-print-goal-at-top)
+(define-key holpp-map "o"    'hol-toggle-goalstack-print-goal-at-top)
+(define-key hol-map   "\M-a" 'hol-toggle-goalstack-num-assums)
+(define-key holpp-map "\M-a" 'hol-toggle-goalstack-num-assums)
+(define-key hol-map   "\C-u" 'hol-toggle-unicode)
+(define-key holpp-map "u"    'hol-toggle-unicode)
+(define-key hol-map   "\C-p" 'hol-toggle-ppbackend)
+(define-key holpp-map "p"    'hol-toggle-ppbackend)
+(define-key holpp-map "b"    'hol-toggle-emacs-tooltips)
+(define-key holpp-map "t"    'hol-toggle-pp-annotations)
+(define-key holpp-map "s"    'hol-toggle-pp-styles)
+(define-key holpp-map "c"    'hol-toggle-pp-cases)
+
+(define-key hol-movement-map "u" 'hol-movement-backward-up-list)
+
+
+
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; The definition of the HOL menu
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define-key-after (lookup-key global-map [menu-bar])
+  [hol-menu]
+  (cons "HOL" (make-sparse-keymap "HOL"))
+  'tools)
+
+
+;; HOL misc
+(define-key
+  global-map
+  [menu-bar hol-menu hol-misc]
+  (cons "Misc" (make-sparse-keymap "Misc")))
+
+(define-key global-map [menu-bar hol-menu hol-misc clean-up]
+   '("Clean up (remove tab, white spaces at end of line, etc...)" .
+     hol-cleanup-buffer))
+
+(define-key global-map [menu-bar hol-menu hol-misc remove-unicode]
+   '("Replace common HOL unicode symbols" .
+     hol-remove-unicode))
+
+(define-key global-map [menu-bar hol-menu hol-misc check-names]
+   '("Check names in store_thm, ..." . hol-check-statement-eq-string))
+
+(define-key global-map [menu-bar hol-menu hol-misc sep4]
+   '(menu-item "--"))
+
+(define-key global-map [menu-bar hol-menu hol-misc check-theory-current]
+   '("Sanity check current theory" . hol-db-check-current))
+
+(define-key global-map [menu-bar hol-menu hol-misc check-theory]
+   '("Sanity check theory" . hol-db-check))
+
+(define-key global-map [menu-bar hol-menu hol-misc sep3]
+   '(menu-item "--"))
+
+(define-key global-map [menu-bar hol-menu hol-misc mark-tactic]
+   '("Mark tactic" . mark-hol-tactic))
+
+(define-key global-map [menu-bar hol-menu hol-misc backward-tactic]
+   '("Move to previous tactic" . backward-hol-tactic))
+
+(define-key global-map [menu-bar hol-menu hol-misc forward-tactic]
+   '("Move to next tactic" . forward-hol-tactic))
+
+(define-key global-map [menu-bar hol-menu hol-misc sep2]
+   '(menu-item "--"))
+
+(define-key global-map [menu-bar hol-menu hol-misc open-string]
+   '("Load and open" . hol-open-string))
+
+(define-key global-map [menu-bar hol-menu hol-misc use-file]
+   '("Use file" . hol-use-file))
+
+(define-key global-map [menu-bar hol-menu hol-misc load-file]
+   '("Load file" . hol-load-file))
+
+(define-key global-map [menu-bar hol-menu hol-misc auto-load]
+   '(menu-item "Automatic loading" hol-toggle-auto-load
+                     :button (:toggle
+                              . (and (boundp 'hol-auto-load-p)
+                                     hol-auto-load-p))))
+
+(define-key global-map [menu-bar hol-menu hol-misc show-load-paths]
+   '("Show load-paths" . hol-show-current-load-paths))
+
+(define-key global-map [menu-bar hol-menu hol-misc add-load-path]
+   '("Add load-path ..." . hol-add-load-path))
+
+(define-key global-map [menu-bar hol-menu hol-misc sep1]
+   '(menu-item "--"))
+
+(define-key global-map [menu-bar hol-menu hol-misc hol-overload-info-for]
+  '("Overload info for string" . hol-overload-info-for))
+
+(define-key global-map [menu-bar hol-menu hol-misc hol-type-info]
+   '("Type info of marked term" . hol-type-info))
+
+(define-key global-map [menu-bar hol-menu hol-misc sep0]
+   '(menu-item "--"))
+
+(define-key global-map [menu-bar hol-menu hol-misc db-find]
+   '("DB find" . hol-db-find))
+
+(define-key global-map [menu-bar hol-menu hol-misc db-match]
+   '("DB match" . hol-db-match))
+
+
+
+;; templates
+(define-key
+  global-map
+  [menu-bar hol-menu hol-template]
+  (cons "Templates" (make-sparse-keymap "Templates")))
+
+(define-key global-map [menu-bar hol-menu hol-template new-script]
+   '("New theory" . hol-template-new-script-file))
+
+(define-key global-map [menu-bar hol-menu hol-template new-datatype]
+   '("New datatype" . hol-template-new-datatype))
+
+(define-key global-map [menu-bar hol-menu hol-template hol-coreln]
+   '("Coinductive definition" . hol-template-hol-coreln))
+
+(define-key global-map [menu-bar hol-menu hol-template hol-reln]
+   '("Inductive definition" . hol-template-hol-reln))
+
+(define-key global-map [menu-bar hol-menu hol-template define]
+   '("New definition" . hol-template-define))
+
+(define-key global-map [menu-bar hol-menu hol-template store-thm]
+   '("Store theorem" . hol-template-store-thm))
+
+(define-key global-map [menu-bar hol-menu hol-template sep1]
+   '(menu-item "--"))
+
+(define-key global-map [menu-bar hol-menu hol-template comment-star]
+   '("Comment *" . hol-template-comment-star))
+
+(define-key global-map [menu-bar hol-menu hol-template comment-equal]
+   '("Comment =" . hol-template-comment-equal))
+
+(define-key global-map [menu-bar hol-menu hol-template comment-minus]
+   '("Comment -" . hol-template-comment-minus))
+
+
+;; printing
+(define-key
+  global-map
+  [menu-bar hol-menu hol-printing]
+  (cons "Printing switches" (make-sparse-keymap "Printing switches")))
+
+(define-key global-map [menu-bar hol-menu hol-printing simplifier-trace]
+   '("Simplifier trace" . hol-toggle-simplifier-trace))
+
+(define-key global-map [menu-bar hol-menu hol-printing times]
+   '("Show times" . hol-toggle-show-times))
+
+(define-key global-map [menu-bar hol-menu hol-printing echo]
+   '("Echo commands" . hol-toggle-echo-commands))
+
+(define-key global-map [menu-bar hol-menu hol-printing quiet]
+   '("Quiet (hide output except errors)" . hol-toggle-quietdec))
+
+(define-key
+  global-map
+  [menu-bar hol-menu hol-printing backends]
+  (cons "Pretty-printing backends" (make-sparse-keymap "Pretty-printing backends")))
+
+(define-key global-map [menu-bar hol-menu hol-printing backends ppreset]
+  '("Reset hol-mode pretty-printing (error recovery)" . holpp-reset))
+
+(define-key global-map [menu-bar hol-menu hol-printing backends sep1]
+   '(menu-item "--"))
+
+(define-key global-map [menu-bar hol-menu hol-printing backends ppstyles]
+  '("Toggle use styles" . hol-toggle-pp-styles))
+
+(define-key global-map [menu-bar hol-menu hol-printing backends ppannotations]
+  '("Toggle use annotations" . hol-toggle-pp-annotations))
+
+(define-key global-map [menu-bar hol-menu hol-printing backends pptooltip]
+  '("Toggle show tooltips" . hol-toggle-emacs-tooltips))
+
+(define-key global-map [menu-bar hol-menu hol-printing backends sep2]
+   '(menu-item "--"))
+
+(define-key global-map [menu-bar hol-menu hol-printing backends ppbackend]
+  '("Toggle pretty-printing backend" . hol-toggle-ppbackend))
+
+(define-key global-map [menu-bar hol-menu hol-printing unicode]
+   '("Unicode" . hol-toggle-unicode))
+
+(define-key global-map [menu-bar hol-menu hol-printing ppcases]
+  '("Toggle pretty-printing of cases" . hol-toggle-pp-cases))
+
+(define-key global-map [menu-bar hol-menu hol-printing sep2]
+   '(menu-item "--"))
+
+
+(define-key global-map [menu-bar hol-menu hol-printing num-subgoals]
+   '("Set no. of shown subgoals" . hol-toggle-goalstack-num-subgoals))
+
+(define-key global-map [menu-bar hol-menu hol-printing num-assums]
+   '("Set no. of shown assumptions" . hol-toggle-goalstack-num-assums))
+
+(define-key global-map [menu-bar hol-menu hol-printing print-goal-at-top]
+   '("Print goal at top" . hol-toggle-goalstack-print-goal-at-top))
+
+(define-key global-map [menu-bar hol-menu hol-printing goal-fvs]
+   '("Show free vars in goal" . hol-toggle-goalstack-fvs))
+
+(define-key global-map [menu-bar hol-menu hol-printing sep1]
+   '(menu-item "--"))
+
+
+(define-key global-map [menu-bar hol-menu hol-printing show-assums]
+   '("Show assumptions" . hol-toggle-show-assums))
+
+(define-key global-map [menu-bar hol-menu hol-printing show-tags]
+   '("Show tags" . hol-toggle-show-tags))
+
+(define-key global-map [menu-bar hol-menu hol-printing show-axioms]
+   '("Show axioms" . hol-toggle-show-axioms))
+
+(define-key global-map [menu-bar hol-menu hol-printing show-num-types]
+   '("Show numeral types" . hol-toggle-show-numeral-types))
+
+(define-key global-map [menu-bar hol-menu hol-printing show-types-verbosely]
+   '("Show types verbosely" . hol-toggle-show-types-verbosely))
+
+(define-key global-map [menu-bar hol-menu hol-printing show-types]
+   '("Show types" . hol-toggle-show-types))
+
+
+
+
+
+;; HOL goals
+(define-key
+  global-map
+  [menu-bar hol-menu hol-goalstack]
+  (cons "Goalstack" (make-sparse-keymap "Goalstack")))
+
+
+(define-key global-map [menu-bar hol-menu hol-goalstack apply-tactic-goaltree]
+   '("Apply tactic (goaltree)" . copy-region-as-goaltree-tactic))
+
+(define-key global-map [menu-bar hol-menu hol-goalstack new-goaltree]
+   '("New goaltree" . hol-do-goaltree))
+
+(define-key global-map [menu-bar hol-menu hol-goalstack sep3]
+   '(menu-item "--"))
+
+(define-key global-map [menu-bar hol-menu hol-goalstack restart-goal]
+   '("Restart goal" . hol-restart-goal))
+
+(define-key global-map [menu-bar hol-menu hol-goalstack drop-all]
+   '("Drop all goals" . hol-drop-all-goals))
+
+(define-key global-map [menu-bar hol-menu hol-goalstack drop-goal]
+   '("Drop goal" . hol-drop-goal))
+
+(define-key global-map [menu-bar hol-menu hol-goalstack sep1]
+   '(menu-item "--"))
+
+(define-key global-map [menu-bar hol-menu hol-goalstack print-all]
+   '("Print all goals" . hol-print-all-goals))
+
+(define-key global-map [menu-bar hol-menu hol-goalstack print-top]
+   '("Print goal" . hol-print-goal))
+
+(define-key global-map [menu-bar hol-menu hol-goalstack sep0]
+   '(menu-item "--"))
+
+(define-key global-map [menu-bar hol-menu hol-goalstack top-thm]
+   '("Name top theorem" . hol-name-top-theorem))
+
+(defun hol-suffices-tactic () (interactive) (hol-subgoal-tactic 1))
+(define-key global-map [menu-bar hol-menu hol-goalstack suffices-tac]
+  '(menu-item "Suffices-by tactic" hol-suffices-tactic
+              :keys "C-u M-h M-s"))
+
+(define-key global-map [menu-bar hol-menu hol-goalstack subgoal-tac]
+   '("Subgoal tactic" . hol-subgoal-tactic))
+
+(define-key global-map [menu-bar hol-menu hol-goalstack rotate]
+   '("Rotate" . hol-rotate))
+
+(define-key global-map [menu-bar hol-menu hol-goalstack back-up-user]
+   '("Restore" . hol-user-backup))
+
+(define-key global-map [menu-bar hol-menu hol-goalstack back-up-save-user]
+   '("Save" . hol-user-save-backup))
+
+(define-key global-map [menu-bar hol-menu hol-goalstack back-up]
+   '("Back up" . hol-backup))
+
+(define-key global-map [menu-bar hol-menu hol-goalstack apply-tactic]
+   '("Apply tactic" . copy-region-as-hol-tactic))
+
+(define-key global-map [menu-bar hol-menu hol-goalstack new-termination-goal]
+  '("New termination goal" . hol-start-termination-proof))
+
+(define-key global-map [menu-bar hol-menu hol-goalstack new-goal]
+   '("New goal" . hol-do-goal))
+
+
+
+;;process
+(define-key
+  global-map
+  [menu-bar hol-menu hol-process]
+  (cons "Process" (make-sparse-keymap "Process")))
+
+(define-key global-map [menu-bar hol-menu hol-process hol-scroll-down]
+   '("Scroll down" . hol-scroll-down))
+
+(define-key global-map [menu-bar hol-menu hol-process hol-scroll-up]
+   '("Scroll up" . hol-scroll-up))
+
+(define-key global-map [menu-bar hol-menu hol-process hol-recentre]
+   '("Recentre" . hol-recentre))
+
+(define-key global-map [menu-bar hol-menu hol-process sep2]
+   '(menu-item "--"))
+
+(define-key global-map [menu-bar hol-menu hol-process hol-send-string]
+   '("Send string to HOL" . interactive-send-string-to-hol))
+
+(define-key global-map [menu-bar hol-menu hol-process hol-send-region-quietly]
+   '("Send region to HOL - hide non-errors" . copy-region-as-hol-definition-quietly))
+
+(define-key global-map [menu-bar hol-menu hol-process hol-send-region]
+   '("Send region to HOL" . copy-region-as-hol-definition))
+
+(define-key global-map [menu-bar hol-menu hol-process sep1]
+   '(menu-item "--"))
+
+(define-key global-map [menu-bar hol-menu hol-process toggle-hol-bare]
+   '(menu-item "Use bare" hol-toggle-bare
+                     :button (:toggle
+                              . (and (boundp 'hol-bare-p)
+                                     hol-bare-p))))
+
+(define-key global-map [menu-bar hol-menu hol-process hol-show-info]
+   '("Show HOL information" . hol-print-info))
+
+(define-key global-map [menu-bar hol-menu hol-process hol-exe]
+   '("Set HOL executable" . hol-set-executable))
+
+(define-key global-map [menu-bar hol-menu hol-process hol-kill]
+   '("Kill HOL" . hol-kill))
+
+(define-key global-map [menu-bar hol-menu hol-process hol-interrupt]
+   '("Interrupt HOL" . hol-interrupt))
+
+(define-key global-map [menu-bar hol-menu hol-process sep02]
+   '(menu-item "--"))
+
+(define-key global-map [menu-bar hol-menu hol-process holmake]
+   '("Run Holmake" . holmake))
+
+(define-key global-map [menu-bar hol-menu hol-process sep01]
+   '(menu-item "--"))
+
+(define-key global-map [menu-bar hol-menu hol-process hol-display]
+   '("Display HOL buffer" . hol-display))
+
+(define-key global-map [menu-bar hol-menu hol-process hol-start-vertical]
+   '("Start HOL - vertical split" . hol-vertical))
+
+(define-key global-map [menu-bar hol-menu hol-process hol-start-horizontal]
+   '("Start HOL - horizontal split" . hol-horizontal))
+
+(define-key global-map [menu-bar hol-menu hol-process hol-start]
+  '("Start HOL" . hol))
+
+(define-key global-map [menu-bar hol-menu hol-process hol-with-region]
+  '("Start HOL & run to cursor" . hol-with-region))
+
+;; Support for snippet expansion, if yasnippet is installed.
+(when (require 'yasnippet nil 'noerror)
+  (let ((HOLsnippets
+         (concat
+          (string-remove-suffix "/bin/hol" hol-executable)
+          "/tools/yasnippets" "")))
+    (setq yas-snippet-dirs (nconc yas-snippet-dirs (cons HOLsnippets '())))
+    (yas-reload-all)
+    (define-key hol-map (kbd "TAB") 'yas-expand)))
diff --git a/tools/vim/filetype.vim b/tools/vim/filetype.vim
new file mode 100644
index 0000000000..0cce22cc82
--- /dev/null
+++ b/tools/vim/filetype.vim
@@ -0,0 +1,9 @@
+augroup filetypedetect
+  au BufRead,BufNewFile *.sml let maplocalleader = "h" | source /Users/josephchan/HOL/tools/vim/hol.vim
+  " recognise pre-munger files as latex source
+  au BufRead,BufNewFile *.htex setlocal filetype=htex syntax=tex
+  "Uncomment the line below to automatically load Unicode
+  "au BufRead,BufNewFile *?Script.sml source /Users/josephchan/HOL/tools/vim/holabs.vim
+  "Uncomment the line below to fold proofs
+  "au BufRead,BufNewFile *?Script.sml setlocal foldmethod=marker foldmarker=Proof,QED foldnestmax=1
+augroup END
diff --git a/tools/vim/hol-config.sml b/tools/vim/hol-config.sml
new file mode 100644
index 0000000000..d4b57025de
--- /dev/null
+++ b/tools/vim/hol-config.sml
@@ -0,0 +1 @@
+use "/Users/josephchan/HOL/tools/vim/vimhol.sml"
diff --git a/tools/vim/hol.vim b/tools/vim/hol.vim
new file mode 100644
index 0000000000..4ea2d3975f
--- /dev/null
+++ b/tools/vim/hol.vim
@@ -0,0 +1,374 @@
+if exists("b:did_hol")
+  finish
+endif
+
+let s:defaultholpipe = "/Users/josephchan/HOL/tools/vim/fifo"
+" initialise pipe if yet unset
+if ! has_key(s:,'holpipe')
+  if empty($VIMHOL_FIFO)
+    let s:holpipe = s:defaultholpipe
+  else
+    let s:holpipe = $VIMHOL_FIFO
+  endif
+endif
+let s:holtogglequiet = "val _ = HOL_Interactive.toggle_quietdec();"
+
+" create the hidden buffer once
+if ! has_key(s:,'holnr') || ! bufexists(s:holnr)
+  new
+  setlocal buftype=nofile
+  setlocal bufhidden=hide
+  setlocal nobuflisted
+  setlocal noswapfile
+  let s:holnr = bufnr("")
+  hide
+endif
+
+
+let s:tmpprefix = "/tmp/vimhol"
+fu! TempName()
+  let l:n = 0
+  while glob(s:tmpprefix.l:n."Script.sml") != ""
+    let l:n = l:n + 1
+  endwhile
+  return s:tmpprefix.l:n."Script.sml"
+endf
+
+fu! HOLCStart()
+  let s:prev = bufnr("")
+  let s:wins = winsaveview()
+  silent exe "keepjumps hide bu" s:holnr
+  setlocal foldmethod=manual
+  keepjumps %d_
+endf
+
+fu! HOLCRestore()
+  silent exe "w>>" . s:holpipe
+  silent exe "keepjumps bu" s:prev
+  call winrestview(s:wins)
+endf
+
+fu! HOLCEnd()
+  let s:temp = TempName()
+  silent exe "w" . s:temp
+  keepjumps %d_
+  silent exe "normal iReadFile " . s:temp
+  call HOLCRestore()
+endf
+
+fu! HOLLoadSetup()
+  keepjumps silent normal P
+  keepjumps silent %s/\s/\r/ge
+  keepjumps silent %s/\<local\>\|\<open\>\|\<in\>\|\<end\>\|;//ge
+  keepjumps silent g/^\s*$/d_
+  keepjumps silent g/./normal ival _ = load"
+  keepjumps silent g/./normal $a";
+endf
+
+fu! HOLLoad()
+  call HOLLoadSetup()
+  call HOLLoadMessage("HOLLoad",line("$"))
+endf
+
+fu! HOLLoadSendQuiet()
+  call HOLLoadSetup()
+  exe "keepjumps normal Go" . s:holtogglequiet
+  let l:l = line(".")-1
+  silent normal op
+  exe "keepjumps normal Go" . s:holtogglequiet
+  call HOLLoadMessage("HOLLoadSendQuiet",l:l)
+endf
+
+fu! HOLLoadMessage(s,l)
+  keepjumps normal Goval _ = print "
+  execute "normal a" . a:s
+  execute "keepjumps silent 1," . a:l . "g/./normal f\"yi\"G$a p"
+  keepjumps normal G$a completed\n";
+endf
+
+fu! HOLSend()
+  silent normal P
+  call HOLEnsureEnd()
+endf
+
+fu! HOLEnsureEnd()
+  keepjumps normal G$a;
+endf
+
+fu! HOLSendQuiet()
+  call HOLSend()
+  exe "keepjumps normal ggO" . s:holtogglequiet
+  exe "keepjumps normal Go" . s:holtogglequiet
+endf
+
+fu! HOLGoal()
+  silent keepjumps normal pG$
+  keepjumps normal G$a)
+  while search(',\_s*)\%$','bW')
+    silent keepjumps normal vG$"_dG$a)
+  endw
+  keepjumps normal gg0iproofManagerLib.g(
+endf
+
+fu! HOLUQGoal()
+  silent keepjumps normal pG$a`)
+  silent keepjumps normal gg0iproofManagerLib.g(`
+endf
+
+let s:stripStart     = ')\|\]\|\['
+let s:stripEnd       = '(\|\['
+let s:stripBothWords = 'THEN[1L]\?\|by'
+let s:stripBoth      = ',\|<<\|>>\|++\|\\\\\|>-\|>|\|>\~'
+let s:delim          = '\_[[:space:]()]'
+
+fu! HOLExpand()
+  silent keepjumps normal pgg0
+  while search('\%^\_s*\%(\%('.s:stripBoth.'\|'.s:stripStart.'\)\|\%('.s:stripBothWords.'\)\)\ze'.s:delim,'cWe')
+    silent keepjumps normal vgg0"_d
+  endw
+  while search('\%(\%('.s:stripBoth.'\|'.s:stripEnd.'\)\|'.s:delim.'\zs\%('.s:stripBothWords.'\)\)\_s*\%$','cW')
+    silent keepjumps normal vG$"_dgg0
+  endw
+  keepjumps normal iproofManagerLib.expand(
+  keepjumps normal G$a)
+endf
+
+fu! HOLSubgoal()
+  keepjumps normal iproofManagerLib.expand(bossLib.sg(
+  silent normal p
+  if search(s:delim.'by'.s:delim.'\_.*','cW')
+    silent keepjumps normal vG$"_d
+  en
+  silent keepjumps normal G$a))
+endf
+
+fu! HOLSuffices()
+  keepjumps normal iproofManagerLib.expand(bossLib.qsuff_tac(
+  silent normal p
+  if search(s:delim.'suffices_by'.s:delim.'\_.*','cW')
+    silent keepjumps normal vG$"_d
+  en
+  silent keepjumps normal G$a))
+endf
+
+fu! HOLF(f)
+  exe "normal i" . a:f
+endf
+
+fu! YankThenHOLCall(f,a) range
+  silent normal gvy
+  call HOLCall(a:f,a:a)
+  exe "normal gv\<Esc>"
+endf
+
+fu! HOLCall(f,a)
+  call HOLCStart()
+  call call(a:f,a:a)
+  call HOLCEnd()
+endf
+
+fu! HOLRepeat(s)
+  call HOLCStart()
+  exe "normal" v:count1 . "i" . a:s
+  call HOLCEnd()
+endf
+
+fu! HOLRotate()
+  call HOLCStart()
+  exe "normal iproofManagerLib.rotate(" . v:count1 .")"
+  call HOLCEnd()
+endf
+
+fu! HOLINT()
+  call HOLCStart()
+  normal iInterrupt
+  call HOLCRestore()
+endf
+
+fu! HOLSelect(l,r)
+  let l:cursor = getpos(".")
+  if search(a:l,"Wbc") == 0
+    return
+  endif
+  normal v
+  if search(a:r,"W") == 0
+    normal <ESC>
+    call setpos('.', l:cursor)
+    return
+  endif
+  call search(a:r,"ce")
+endf
+
+fu! HOLPattern()
+  silent keepjumps normal pgg0
+  while search('\%^\_s*\%(\%('.s:stripBoth.'\|'.s:stripStart.'\)\|\%('.s:stripBothWords.'\)\)\ze'.s:delim,'cWe')
+    silent keepjumps normal vgg0"_d
+  endw
+  while search('\%(\%('.s:stripBoth.'\|'.s:stripEnd.'\)\|'.s:delim.'\zs\%('.s:stripBothWords.'\)\)\_s*\%$','cW')
+    silent keepjumps normal vG$"_dgg0
+  endw
+  keepjumps normal iproofManagerLib.expand_list(Q.SELECT_GOAL_LT(
+  keepjumps normal G$a))
+endf
+
+if !(exists("maplocalleader"))
+  let maplocalleader = "\\"
+endif
+vn <buffer><silent> <LocalLeader>l :call YankThenHOLCall(function("HOLLoadSendQuiet"),[])<CR>
+vn <buffer><silent> <LocalLeader>L :call YankThenHOLCall(function("HOLLoad"),[])<CR>
+vn <buffer><silent> <LocalLeader>s :call YankThenHOLCall(function("HOLSend"),[])<CR>
+vn <buffer><silent> <LocalLeader>u :call YankThenHOLCall(function("HOLSendQuiet"),[])<CR>
+vn <buffer><silent> <LocalLeader>g :call YankThenHOLCall(function("HOLGoal"),[])<CR>
+vn <buffer><silent> <LocalLeader>G :call YankThenHOLCall(function("HOLUQGoal"),[])<CR>
+vn <buffer><silent> <LocalLeader>e :call YankThenHOLCall(function("HOLExpand"),[])<CR>
+vn <buffer><silent> <LocalLeader>S :call YankThenHOLCall(function("HOLSubgoal"),[])<CR>
+vn <buffer><silent> <LocalLeader>F :call YankThenHOLCall(function("HOLSuffices"),[])<CR>
+vn <buffer><silent> <LocalLeader>P :call YankThenHOLCall(function("HOLPattern"),[])<CR>
+nm <buffer><silent><expr> <LocalLeader>l "V".maplocalleader."l"
+nm <buffer><silent><expr> <LocalLeader>L "V".maplocalleader."L"
+nm <buffer><silent><expr> <LocalLeader>s "V".maplocalleader."s"
+nm <buffer><silent><expr> <LocalLeader>u "V".maplocalleader."u"
+nm <buffer><silent><expr> <LocalLeader>g "V".maplocalleader."g"
+nm <buffer><silent><expr> <LocalLeader>G "V".maplocalleader."G"
+nm <buffer><silent><expr> <LocalLeader>e "V".maplocalleader."e"
+nm <buffer><silent><expr> <LocalLeader>S "V".maplocalleader."S"
+nm <buffer><silent><expr> <LocalLeader>F "V".maplocalleader."F"
+nm <buffer><silent><expr> <LocalLeader>P "V".maplocalleader."P"
+nn <buffer><silent> <LocalLeader>R :<C-U>call HOLRotate()<CR>
+nn <buffer><silent> <LocalLeader>b :<C-U>call HOLRepeat("proofManagerLib.backup();")<CR>
+nn <buffer><silent> <LocalLeader>B :<C-U>call HOLRepeat("proofManagerLib.restore();")<CR>
+nn <buffer><silent> <LocalLeader>v :call HOLCall(function("HOLF"),["proofManagerLib.save()"])<CR>
+nn <buffer><silent> <LocalLeader>d :<C-U>call HOLRepeat("proofManagerLib.drop();")<CR>
+nn <buffer><silent> <LocalLeader>p :call HOLCall(function("HOLF"),["proofManagerLib.p()"])<CR>
+nn <buffer><silent> <LocalLeader>r :call HOLCall(function("HOLF"),["proofManagerLib.restart()"])<CR>
+nn <buffer><silent> <LocalLeader>c :call HOLINT()<CR>
+nn <buffer><silent> <LocalLeader>t :call HOLSelect('`\\|‘','`\\|’')<CR>
+nn <buffer><silent> <LocalLeader>T :call HOLSelect('``\\|“','``\\|”')<CR>
+nn <buffer><silent> <LocalLeader>a :call HOLSelect('^Triviality\\|^Theorem','^Proof')<CR>-Vo+
+nn <buffer><silent> <LocalLeader>y :call HOLCall(function("HOLF"),["Globals.show_types:=not(!Globals.show_types)"])<CR>
+nn <buffer><silent> <LocalLeader>n :call HOLCall(function("HOLF"),["Feedback.set_trace \"PP.avoid_unicode\" (1 - Feedback.current_trace \"PP.avoid_unicode\")"])<CR>
+no <buffer><LocalLeader>h h
+
+if (!has('terminal') && ! has('nvim'))
+    \ || (has('nvim') && !exists(':terminal'))
+  " skip terminal feature
+  let b:did_hol = 1
+  echomsg "vimhol: no support for (n)vim terminal feature"
+  finish
+endif
+
+" finds hol located next Holmake (the lastmaker)
+function! LastmakerHOL()
+  let lastmakerfile = ".HOLMK/lastmaker"
+  if filereadable(lastmakerfile)
+    let lm = readfile(lastmakerfile,"",1)
+    if 0 < len(lm)
+      " assumes only one Holmake string in lastmaker path
+      return fnamemodify(lm[0],":s?Holmake?hol?")
+    endif
+  endif
+  return ""
+endfunction
+
+" finds a HOL executable
+function! WhichHOL()
+  let lm = LastmakerHOL()
+  let holdir = $HOLDIR . '/bin/hol'
+  " honouring 'hol' next to lastmaker
+  if executable(lm)
+    return lm
+  elseif executable(holdir)
+    return holdir
+  elseif executable('hol')
+    return 'hol'
+  endif
+  return ""
+endfunction
+
+" initialise
+if ! has_key(g:,'hol_repl')
+  let g:hol_repl = []
+endif
+
+function! HOLREPLnew()
+  let l:cmd = WhichHOL()
+  if ! (0 < len(l:cmd) && executable(l:cmd))
+    echoerr 'vimhol: hol command not found ' . l:cmd . ' Set HOLDIR environment variable'
+    return 0
+  endif
+  let s:holpipe = tempname()
+  call system('mkfifo '. s:holpipe)
+  "echomsg "holrepl pipe " . s:holpipe
+  let options = {
+  \  "cwd": expand('%:p:h'),
+  \  "vertical": 1,
+  \  "env": {
+  \    "VIMHOL_FIFO": s:holpipe
+  \  }}
+  let altname = expand("%:r:t") " alternate name for terminal buffer
+  echomsg 'vimhol repl cmd: ' . l:cmd
+  if has('nvim') " neovim terminal
+    let options.stdin = "null"
+    vsplit | enew
+    let l:terminal_job_id = termopen(l:cmd, options)
+    call add(g:hol_repl, {'buf': bufnr(''), 'job': l:terminal_job_id, 'pipe': s:holpipe})
+    " scroll to end of terminal buffer
+    silent! normal G
+  else " vim terminal
+    " Uncomment the next vimscript let-assignment to automatically close any
+    " terminated terminal buffer window. This is encouraged for advanced users
+    " only, because also any buffer with a failing hol command will be closed.
+    "let options.term_finish = "close"
+    rightbelow let s:replbuf = term_start(l:cmd, options)
+    call add(g:hol_repl, {'buf': s:replbuf, 'pipe': s:holpipe})
+    call term_setkill(g:hol_repl[-1].buf, 'term')
+  endif
+  " set (unique) buffer name containing the origin
+  let g:hol_repl[-1].altname = 'hol ('. g:hol_repl[-1].buf . '): ' . altname
+  exec 'file ' . g:hol_repl[-1].altname
+  wincmd p
+endfunction
+
+if has('nvim')
+  function! HOLREPLsend(text)
+    " only send commands if a terminal buffer exists
+    if has_key(g:,'hol_repl') && len(g:hol_repl) > 0
+      call chansend(g:hol_repl[-1].job, a:text)
+    else
+      echoerr "vimhol: no active hol repl found"
+    endif
+  endfunction
+else
+  function! HOLREPLsend(text)
+    " only send commands if a terminal buffer exists
+    if has_key(g:,'hol_repl') && len(g:hol_repl) > 0
+      call term_sendkeys(g:hol_repl[-1].buf, a:text)
+    else
+      echoerr "vimhol: no active hol repl found"
+    endif
+  endfunction
+endif
+
+" close terminal
+function! HOLREPLclose()
+  if has_key(g:,'hol_repl') && len(g:hol_repl) > 0
+    call HOLREPLsend("\<C-D>")
+    call remove(g:hol_repl, -1)
+    " (re)set the current holpipe
+    if len(g:hol_repl) > 0
+      let s:holpipe = g:hol_repl[-1].pipe
+    else
+      unlet s:holpipe
+    endif
+  endif
+endfunction
+" open a new hol terminal
+nn <buffer><silent> <LocalLeader>x :call HOLREPLnew()<CR>
+" close a hol_repl buffer
+nn <buffer><silent> <LocalLeader>X :call HOLREPLclose()<CR>
+" send current line (or highlighted section) to terminal
+vn <buffer><silent> <LocalLeader>w "0y:call HOLREPLsend(getreg('0',1) . ";\n")<CR>
+nm <buffer><silent><expr> <LocalLeader>w "V".maplocalleader."w"
+
+let b:did_hol = 1
+" vim: ft=vim
diff --git a/tools/vim/vimhol.sml b/tools/vim/vimhol.sml
new file mode 100644
index 0000000000..32f8e0bac0
--- /dev/null
+++ b/tools/vim/vimhol.sml
@@ -0,0 +1,120 @@
+val () = PolyML.print_depth 0;
+local
+val defaultFifoPath = "/Users/josephchan/HOL/tools/vim/fifo"
+  val fifoPath = Option.getOpt(OS.Process.getEnv "VIMHOL_FIFO",defaultFifoPath)
+  structure Queue :> (* Modified from http://mlton.org/MLtonThread *)
+     sig
+        type 'a t
+        val new: unit -> 'a t
+        val enque: 'a t * 'a -> unit
+        val deque: 'a t -> 'a option
+     end =
+     struct
+        datatype 'a t = T of {front: 'a list ref, back: 'a list ref}
+        fun new() = T{front = ref [], back = ref []}
+        fun enque(T{back, ...}, x) = back := x :: !back
+        fun deque(T{front, back}) =
+           case !front of
+              [] => (case !back of
+                        [] => NONE
+                      | l => let val l = rev l in
+                                back := []; front := (tl l); SOME (hd l)
+                             end)
+            | x :: l => (front := l; SOME x)
+     end
+  open TextIO Thread OS.FileSys Unix
+  val quiet = ref false
+  fun warn s = if !quiet then () else output(stdErr, s)
+  local open OS.Process Posix.FileSys in
+    fun die s = (warn s; exit failure)
+    val () = if access(fifoPath, []) then let
+               val st = stat fifoPath
+             in
+               if ST.isFIFO st then ()
+               else die (fifoPath^" is not a fifo\n")
+             end else let
+               open S val urw = flags [irusr, iwusr]
+             in
+               mkfifo(fifoPath, urw)
+             end
+  end
+  val m = Mutex.mutex ()
+  val c = ConditionVar.conditionVar ()
+  val q = Queue.new ()
+  val keepFiles = ref false
+  fun tryRemove s = remove s handle OS.SysErr _ => ()
+  fun checkTryRemove s = if !keepFiles then () else tryRemove s
+  fun removeQueue() = let
+    fun loop() = case Queue.deque q of
+      NONE => () |
+      SOME tmp => (checkTryRemove tmp; loop())
+    open Mutex
+  in
+    lock m; loop(); unlock m
+  end
+  local
+    fun removeAfterUse tmp =
+      (QUse.use tmp
+       handle e => (
+         checkTryRemove tmp;
+         TextIO.print ("Exception- " ^ exnMessage e ^ " raised\n");
+         PolyML.Exception.reraise e);
+       checkTryRemove tmp)
+    open Mutex ConditionVar
+  in
+    fun runner () =
+      (lock m;
+       case Queue.deque q of
+          NONE => (wait(c,m); unlock m)
+        | SOME tmp => (unlock m; removeAfterUse tmp);
+       runner ())
+  end
+  val tail = ref (execute("/usr/bin/env",["tail","/dev/null"]))
+  val fifo = ref (openString "")
+  fun stopTail () = (kill(!tail,Posix.Signal.term); reap (!tail); ())
+  fun restartTail () = (stopTail() handle OS.SysErr _ => ();
+                        tail := execute("/usr/bin/env", ["tail", "-f", fifoPath]);
+                        fifo := textInstreamOf (!tail))
+  val rpid = ref (Thread.fork(fn () => (), []))
+  fun poller () = let in
+    case inputLine (!fifo) of
+      NONE => (warn "Vimhol's tail gave eof\n"; restartTail())
+    | SOME line =>
+      case String.tokens Char.isSpace line of
+          ["Interrupt"] => (warn "Vim interrupt\n"; Thread.broadcastInterrupt ())
+        | ["ReadFile",tmp] => let open Thread Mutex ConditionVar in
+            warn ("Vim input "^tmp^"\n");
+            lock m;
+            Queue.enque(q,tmp);
+            unlock m;
+            if isActive (!rpid) then ()
+            else rpid := fork(runner,
+                              [InterruptState InterruptAsynch,
+                               EnableBroadcastInterrupt true]);
+            signal c
+          end
+        | [] => ()
+        | _ => warn ("Got this rubbish from Vim: "^line);
+    Thread.testInterrupt () handle Interrupt => (removeQueue(); Thread.exit());
+    poller ()
+  end
+  val () = OS.Process.atExit stopTail
+  val () = restartTail ()
+  val ppid = ref (Thread.fork(poller,[]))
+in
+  structure Vimhol = struct
+    val fifoPath = fifoPath
+    fun pActive() = Thread.isActive (!ppid)
+    fun rActive() = Thread.isActive (!rpid)
+    val stopTail = stopTail
+    val restartTail = restartTail
+    fun stop() = (if rActive() then Thread.interrupt (!rpid) else ();
+                  if pActive() then Thread.interrupt (!ppid) else ())
+    fun restart() = (stop(); ppid := Thread.fork(poller,[]))
+    val keepFiles = keepFiles
+    val quiet = quiet
+    val queue = q
+    val removeQueue = removeQueue
+  end
+end
+(* vim: set ft=sml:*)