From f1d517a56247d394026020eb4ad38a6e47b3976c Mon Sep 17 00:00:00 2001 From: Joseph Chan Date: Mon, 16 Dec 2024 16:53:13 +1100 Subject: [PATCH] Delete auto-generated files. --- 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 deletions(-) delete mode 100644 tools/hol-mode.el delete mode 100644 tools/vim/filetype.vim delete mode 100644 tools/vim/hol-config.sml delete mode 100644 tools/vim/hol.vim delete mode 100644 tools/vim/vimhol.sml diff --git a/tools/hol-mode.el b/tools/hol-mode.el deleted file mode 100644 index ebdbdeac27..0000000000 --- a/tools/hol-mode.el +++ /dev/null @@ -1,2215 +0,0 @@ -;;; -*- 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 "") -;;; (load "") - -;;; 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+" "\\|" - "\\_"))) - (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 deleted file mode 100644 index 0cce22cc82..0000000000 --- a/tools/vim/filetype.vim +++ /dev/null @@ -1,9 +0,0 @@ -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 deleted file mode 100644 index d4b57025de..0000000000 --- a/tools/vim/hol-config.sml +++ /dev/null @@ -1 +0,0 @@ -use "/Users/josephchan/HOL/tools/vim/vimhol.sml" diff --git a/tools/vim/hol.vim b/tools/vim/hol.vim deleted file mode 100644 index 4ea2d3975f..0000000000 --- a/tools/vim/hol.vim +++ /dev/null @@ -1,374 +0,0 @@ -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/\\|\\|\\|\\|;//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\" -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 - 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 l :call YankThenHOLCall(function("HOLLoadSendQuiet"),[]) -vn L :call YankThenHOLCall(function("HOLLoad"),[]) -vn s :call YankThenHOLCall(function("HOLSend"),[]) -vn u :call YankThenHOLCall(function("HOLSendQuiet"),[]) -vn g :call YankThenHOLCall(function("HOLGoal"),[]) -vn G :call YankThenHOLCall(function("HOLUQGoal"),[]) -vn e :call YankThenHOLCall(function("HOLExpand"),[]) -vn S :call YankThenHOLCall(function("HOLSubgoal"),[]) -vn F :call YankThenHOLCall(function("HOLSuffices"),[]) -vn P :call YankThenHOLCall(function("HOLPattern"),[]) -nm l "V".maplocalleader."l" -nm L "V".maplocalleader."L" -nm s "V".maplocalleader."s" -nm u "V".maplocalleader."u" -nm g "V".maplocalleader."g" -nm G "V".maplocalleader."G" -nm e "V".maplocalleader."e" -nm S "V".maplocalleader."S" -nm F "V".maplocalleader."F" -nm P "V".maplocalleader."P" -nn R :call HOLRotate() -nn b :call HOLRepeat("proofManagerLib.backup();") -nn B :call HOLRepeat("proofManagerLib.restore();") -nn v :call HOLCall(function("HOLF"),["proofManagerLib.save()"]) -nn d :call HOLRepeat("proofManagerLib.drop();") -nn p :call HOLCall(function("HOLF"),["proofManagerLib.p()"]) -nn r :call HOLCall(function("HOLF"),["proofManagerLib.restart()"]) -nn c :call HOLINT() -nn t :call HOLSelect('`\\|‘','`\\|’') -nn T :call HOLSelect('``\\|“','``\\|”') -nn a :call HOLSelect('^Triviality\\|^Theorem','^Proof')-Vo+ -nn y :call HOLCall(function("HOLF"),["Globals.show_types:=not(!Globals.show_types)"]) -nn n :call HOLCall(function("HOLF"),["Feedback.set_trace \"PP.avoid_unicode\" (1 - Feedback.current_trace \"PP.avoid_unicode\")"]) -no 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("\") - 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 x :call HOLREPLnew() -" close a hol_repl buffer -nn X :call HOLREPLclose() -" send current line (or highlighted section) to terminal -vn w "0y:call HOLREPLsend(getreg('0',1) . ";\n") -nm w "V".maplocalleader."w" - -let b:did_hol = 1 -" vim: ft=vim diff --git a/tools/vim/vimhol.sml b/tools/vim/vimhol.sml deleted file mode 100644 index 32f8e0bac0..0000000000 --- a/tools/vim/vimhol.sml +++ /dev/null @@ -1,120 +0,0 @@ -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:*)