1;;; -*- emacs-lisp -*-
2;;; to use this mode, you will need to do something along the lines of
3;;; the following and have it in your .emacs file:
4;;;    (setq hol-executable "<fullpath to HOL executable>")
5;;;    (load "<fullpath to this file>")
6
7;;; The fullpath to this file can be just the name of the file, if
8;;; your elisp variable load-path includes the directory where it
9;;; lives.
10
11(require 'thingatpt)
12(require 'cl)
13(require 'subr-x)
14
15(defgroup hol nil
16  "Customising the Emacs interface to the HOL4 proof assistant."
17  :group 'external)
18
19(define-prefix-command 'hol-map)
20(define-prefix-command 'hol-d-map)
21(make-variable-buffer-local 'hol-buffer-name)
22(make-variable-buffer-local 'hol-buffer-ready)
23(set-default 'hol-buffer-ready nil)
24(set-default 'hol-buffer-name "*HOL*")
25
26(set-default 'hol-default-buffer nil)
27
28(defcustom hol-executable HOL-EXECUTABLE
29  "Path-name for the HOL executable."
30  :group 'hol
31  :type '(file :must-match t))
32
33(defcustom holmake-executable HOLMAKE-EXECUTABLE
34  "Path-name for the Holmake executable."
35  :group 'hol
36  :type '(file :must-match t))
37
38(defcustom hol-new-buffer-style-default 'new-frame
39  "Default style for creating new HOL buffers. Possible values are
40new-frame (create in a new-frame); horizontal (create in a new buffer
41that is horizontally adjacent and to the right); and vertical (create in
42a new buffer that is vertically adjacent and below)."
43  :group 'hol
44  :type '(choice (const new-frame :tag "new-frame")
45                 (const horizontal :tag "horizontal")
46                 (const vertical :tag "vertical")))
47
48(defun hol-set-executable (filename)
49  "*Set hol executable variable to be NAME."
50  (interactive "fHOL executable: ")
51  (setq hol-executable filename)
52  (setq hol-bare-p nil))
53
54(defun holmake-set-executable (filename)
55  "*Set holmake executable variable to be NAME."
56  (interactive "fHOL executable: ")
57  (setq holmake-executable filename))
58
59(defvar hol-mode-sml-init-command
60   "use (Globals.HOLDIR ^ \"/tools/hol-mode.sml\")"
61  "*The command to send to HOL to load the ML-part of hol-mode.")
62
63
64(defcustom hol-echo-commands-p nil
65  "Whether or not to echo the text of commands originating elsewhere."
66  :group 'hol
67  :type 'boolean)
68
69(defcustom hol-raise-on-recentre nil
70  "Controls if hol-recentre (\\[hol-recentre]) also raises the HOL frame."
71  :group 'hol
72  :type 'boolean)
73
74(defcustom hol-unicode-print-font-filename
75  "/usr/share/fonts/truetype/ttf-dejavu/DejaVuSans.ttf"
76  "File name of font to use when printing HOL output to a PDF file."
77  :group 'hol
78  :type '(file :must-match t))
79
80
81
82(defvar hol-generate-locpragma-p t
83  "*Whether or not to generate (*#loc row col *) pragmas for HOL.")
84
85(defvar hol-emit-time-elapsed-p nil
86  "*Whether or not to print time elapsed messages after causing HOL
87evaluations.")
88
89(defvar hol-auto-load-p t
90  "*Do automatic loading?")
91
92(defvar hol-bare-p nil
93  "*use hol.bare?")
94
95;;; For compatability between both Emacs and XEmacs, please use the following
96;;; two functions to determine if the mark is active, or to set it active.
97
98(defun is-region-active ()
99  (or
100    (and (fboundp 'region-active-p) (region-active-p)
101         (fboundp 'region-exists-p) (region-exists-p))
102    (and transient-mark-mode (boundp 'mark-active) mark-active)))
103
104(defun set-region-active ()
105  (or
106    (and (fboundp 'zmacs-activate-region) (zmacs-activate-region))
107    (and (boundp 'mark-active) (setq mark-active t))))
108
109(put 'hol-term 'end-op
110     (function (lambda () (skip-chars-forward "^`������"))))
111(defvar hol-beg-pos nil) ; ugh, global, but easiest this way
112(put 'hol-term 'beginning-op
113     (function (lambda () (skip-chars-backward "^`������") (setq hol-beg-pos (point)))))
114(defun hol-term-at-point ()
115  (let ((s (thing-at-point 'hol-term)))
116    (with-hol-locpragma hol-beg-pos s)))
117
118;;; makes buffer hol aware.  Currently this consists of no more than
119;;; altering the syntax table if its major is sml-mode.
120(defun make-buffer-hol-ready ()
121  (if (eq major-mode 'sml-mode)
122      (progn
123        (modify-syntax-entry ?` "$")
124        (modify-syntax-entry ?\\ "\\"))))
125
126(defun hol-buffer-ok (string)
127  "Checks a string to see if it is the name of a good HOL buffer.
128In reality this comes down to checking that a buffer-name has a live
129process in it."
130  (and string (get-buffer-process string)
131       (eq 'run
132           (process-status
133            (get-buffer-process string)))))
134
135(defun ensure-hol-buffer-ok ()
136  "Ensures by prompting that a HOL buffer name is OK, and returns it."
137  (if (not hol-buffer-ready)
138      (progn (make-buffer-hol-ready) (setq hol-buffer-ready t)))
139  (if (hol-buffer-ok hol-buffer-name) hol-buffer-name
140    (message
141     (cond (hol-buffer-name (concat hol-buffer-name " not valid anymore."))
142           (t "Please choose a HOL to attach this buffer to.")))
143    (sleep-for 1)
144    (setq hol-buffer-name (read-buffer "HOL buffer: " hol-default-buffer t))
145    (while (not (hol-buffer-ok hol-buffer-name))
146      (ding)
147      (message "Not a valid HOL process")
148      (sleep-for 1)
149      (setq hol-buffer-name
150            (read-buffer "HOL buffer: " hol-default-buffer t)))
151    (setq hol-default-buffer hol-buffer-name)
152    hol-buffer-name))
153
154
155(defun forward-smlsymbol (n)
156  (interactive "p")
157  (cond ((> n 0)
158         (while (> n 0)
159           (skip-syntax-forward "^.")
160           (skip-syntax-forward ".")
161           (setq n (- n 1))))
162        ((< n 0)
163         (setq n (- n))
164         (setq n (- n (if (equal (skip-syntax-backward ".") 0) 0 1))))
165         (while (> n 0)
166           (skip-syntax-backward "^.")
167           (skip-syntax-backward ".")
168           (setq n (- n 1)))))
169
170(defun is-a-then (s)
171  (and s (or (string-equal s "THEN")
172             (string-equal s "THENL")
173             (string-equal s "val")
174             (string-equal s ">-")
175             (string-equal s ">>")
176             (string-equal s ">|")
177             (string-equal s "\\\\"))))
178
179(defun next-hol-lexeme-terminates-tactic ()
180  (skip-syntax-forward " ")
181  (or (eobp)
182      (char-equal (following-char) ?,)
183      (char-equal (following-char) ?\))
184      ;; (char-equal (following-char) ?=)
185      (char-equal (following-char) ?\;)
186      (is-a-then (word-at-point))
187      (is-a-then (thing-at-point 'smlsymbol t))
188      (string= (word-at-point) "val")))
189
190(defun previous-hol-lexeme-terminates-tactic ()
191  (save-excursion
192    (skip-chars-backward " \n\t\r")
193    (or (bobp)
194        (char-equal (preceding-char) ?,)
195        (char-equal (preceding-char) ?=)
196        (char-equal (preceding-char) ?\;)
197        (char-equal (preceding-char) ?\))
198        (and (condition-case nil
199                 (progn (backward-char 1) t)
200                 (error nil))
201             (or (is-a-then (word-at-point))
202                 (is-a-then (thing-at-point 'smlsymbol t))
203                 (string= (word-at-point) "val"))))))
204
205(defun looking-at-tactic-terminator ()
206  "Returns a cons-pair (x . y), with x the distance to end, and y the
207   size of the terminator, or nil if there isn't one there. The x value may
208   be zero, if point is immediately after the terminator."
209  (interactive)
210  (let ((c (following-char))
211        (pc (preceding-char)))
212    (cond ((char-equal c ?,) '(1 . 1))
213          ((char-equal pc ?,) '(0 . 1))
214          ((char-equal c ?\)) '(1 . 1))
215          ((char-equal pc ?\)) '(0 . 1))
216          ((char-equal c ?\]) '(1 . 1))
217          ((char-equal pc ?\]) '(0 . 1))
218          ((char-equal c ?\;) '(1 . 1))
219          ((char-equal pc ?\;) '(0 . 1))
220          ((let ((w (word-at-point)))
221             (if (is-a-then w)
222                 (cons
223                  (- (cdr (bounds-of-thing-at-point 'word)) (point))
224                  (length w))
225               (let ((w (thing-at-point 'smlsymbol t)))
226                 (if (is-a-then w)
227                     (cons
228                      (- (cdr (bounds-of-thing-at-point 'smlsymbol)) (point))
229                      (length w))
230                   nil))))))))
231
232(defun looking-at-tactic-starter ()
233  "Returns a cons-pair (x . y), with x the distance to end, and y the
234   size of the terminator, or nil if there isn't one there. The x value may
235   be zero, if point is immediately after the terminator."
236  (interactive)
237  (let ((c (following-char))
238        (pc (preceding-char)))
239    (cond ((char-equal c ?,) '(1 . 1))
240          ((char-equal pc ?,) '(0 . 1))
241          ((char-equal c ?\() '(1 . 1))
242          ((char-equal pc ?\() '(0 . 1))
243          ((char-equal c ?\[) '(1 . 1))
244          ((char-equal pc ?\[) '(0 . 1))
245          ((char-equal c ?\;) '(1 . 1))
246          ((char-equal pc ?\;) '(0 . 1))
247          ((let ((w (word-at-point)))
248             (if (is-a-then w)
249                 (cons
250                  (- (cdr (bounds-of-thing-at-point 'word)) (point))
251                  (length w))
252               (let ((w (thing-at-point 'smlsymbol t)))
253                 (if (is-a-then w)
254                     (cons
255                      (- (cdr (bounds-of-thing-at-point 'smlsymbol)) (point))
256                      (length w))
257                   nil))))))))
258
259
260(defun forward-tactic-terminator (n)
261  (interactive "^p")
262  (cond ((> n 0)
263         (let (c)
264           (while (> n 0)
265             (skip-syntax-forward " ")
266             (setq c (looking-at-tactic-terminator))
267             (while (or (not c) (equal (car c) 0))
268               (forward-sexp)
269               (skip-syntax-forward " ")
270               (setq c (looking-at-tactic-terminator)))
271             (forward-char (car c))
272             (setq n (- n 1)))))
273        ((< n 0)
274         (setq n (- n))
275         (let (c)
276           (while (> n 0)
277             (skip-syntax-backward " ")
278             (setq c (looking-at-tactic-terminator))
279             (while (or (not c) (equal (car c) (cdr c)))
280               (condition-case nil
281                   (backward-sexp)
282                 (error (backward-char)))
283               (skip-syntax-backward " ")
284               (setq c (looking-at-tactic-terminator)))
285             (backward-char (- (cdr c) (car c)))
286             (setq n (- n 1)))))))
287
288(defun forward-tactic-starter (n)
289  (interactive "^p")
290  (cond ((> n 0)
291         (let (c)
292           (while (> n 0)
293             (skip-syntax-forward " ")
294             (setq c (looking-at-tactic-starter))
295             (while (or (not c) (equal (car c) 0))
296               (forward-sexp)
297               (skip-syntax-forward " ")
298               (setq c (looking-at-tactic-starter)))
299             (forward-char (car c))
300             (setq n (- n 1)))))
301        ((< n 0)
302         (setq n (- n))
303         (let (c)
304           (while (> n 0)
305             (skip-syntax-backward " ")
306             (setq c (looking-at-tactic-starter))
307             (while (or (not c) (equal (car c) (cdr c)))
308               (condition-case nil
309                   (backward-sexp)
310                 (error (backward-char)))
311               (skip-syntax-backward " ")
312               (setq c (looking-at-tactic-starter)))
313             (backward-char (- (cdr c) (car c)))
314             (setq n (- n 1)))))))
315
316(defun preceded-by-starter ()
317  (save-excursion
318    (backward-char)
319    (thing-at-point 'tactic-starter)))
320(defun forward-hol-tactic (n)
321  (interactive "^p")
322  (cond ((> n 0)
323         (while (> n 0)
324           (skip-syntax-forward " ")
325           (while (thing-at-point 'tactic-terminator)
326             (forward-tactic-terminator 1)
327             (skip-syntax-forward " "))
328           (while (not (thing-at-point 'tactic-terminator))
329             (forward-sexp 1)
330             (skip-syntax-forward " "))
331           (skip-syntax-backward " ")
332           (setq n (- n 1))))
333        ((< n 0)
334         (setq n (- n))
335         (while (> n 0)
336           (skip-syntax-backward " ")
337           (while (preceded-by-starter)
338             (forward-tactic-starter -1)
339             (skip-syntax-backward " "))
340           (while (not (preceded-by-starter))
341             (forward-sexp -1)
342             (skip-syntax-backward " "))
343           (skip-syntax-forward " ")
344           (setq n (- n 1))))))
345
346;;; returns true and moves forward a sexp if this is possible, returns nil
347;;; and stays where it is otherwise
348(defun my-forward-sexp ()
349  (condition-case nil
350      (progn (forward-sexp 1) t)
351    (error nil)))
352(defun my-backward-sexp()
353  (condition-case nil
354      (progn (backward-sexp 1) t)
355    (error nil)))
356
357(defun word-before-point ()
358  (save-excursion
359    (condition-case nil
360        (progn (backward-char 1) (word-at-point))
361      (error nil))))
362
363(defun backward-hol-tactic (n)
364  (interactive "p")
365  (forward-hol-tactic (if n (- n) -1)))
366
367(defun prim-mark-hol-tactic ()
368  (let ((bounds (bounds-of-thing-at-point 'hol-tactic)))
369    (if bounds
370        (progn
371          (goto-char (cdr bounds))
372          (push-mark (car bounds) t t)
373          (set-region-active))
374      (error "No tactic at point"))))
375
376(defun mark-hol-tactic ()
377  (interactive)
378  (let ((initial-point (point)))
379    (condition-case nil
380        (prim-mark-hol-tactic)
381      (error
382       ;; otherwise, skip white-space forward to see if this would move us
383       ;; onto a tactic.  If so, great, otherwise, go backwards and look for
384       ;; one there.  Only if all this fails signal an error.
385       (condition-case nil
386           (progn
387             (skip-chars-forward " \n\t\r")
388             (prim-mark-hol-tactic))
389         (error
390          (condition-case e
391              (progn
392                (if (skip-chars-backward " \n\t\r")
393                    (progn
394                      (backward-char 1)
395                      (prim-mark-hol-tactic))
396                  (prim-mark-hol-tactic)))
397            (error
398             (goto-char initial-point)
399             (signal (car e) (cdr e))))))))))
400
401
402(defun with-hol-locpragma (pos s)
403  (if hol-generate-locpragma-p
404      (concat (hol-locpragma-of-position pos) s)
405      s))
406
407(defun hol-locpragma-of-position (pos)
408  "Convert Elisp position into HOL location pragma.  Not for interactive use."
409  (let ((initial-point (point)))
410    (goto-char pos)
411    (let* ((rowstart (point-at-bol))  ;; (line-beginning-position)
412           (row      (+ (count-lines 1 pos)
413                      (if (= rowstart pos) 1 0)))
414           (col      (+ (current-column) 1)))
415      (goto-char initial-point)
416      (format " (*#loc %d %d *)" row col))))
417
418(defun send-timed-string-to-hol (string echo-p)
419  "Send STRING to HOL (with send-string-to-hol), and emit information about
420how long this took."
421  (interactive)
422  (send-raw-string-to-hol
423   "val hol_mode_time0 = #usr (Timer.checkCPUTimer Globals.hol_clock);" nil nil)
424  (send-string-to-hol string echo-p)
425  (send-raw-string-to-hol
426       "val _ = let val t = #usr (Timer.checkCPUTimer Globals.hol_clock)
427                      val elapsed = Time.-(t, hol_mode_time0)
428                in
429                      print (\"\\n*** Time taken: \"^
430                             Time.toString elapsed^\"s\\n\")
431                  end" nil nil))
432
433(defvar tactic-connective-regexp
434  "[[:space:]]*\\(THEN1\\|THENL\\|THEN\\|>>\\|>|\\|>-\\|\\\\\\\\\\)[[:space:]]*[[(]?"
435  "Regular expression for strings used to put tactics together.")
436
437(defun tactic-cleanup-leading (string)
438  "Remove leading instances of tactic connectives from a string.
439A tactic connective is any one of \"THEN\", \"THENL\", \"THEN1\", \">>\", \">|\"
440or \">-\"."
441  (let* ((case-fold-search nil)
442         (pattern (concat "\\`" tactic-connective-regexp)))
443    (replace-regexp-in-string pattern "" string)))
444
445(defun tactic-cleanup-trailing (string)
446  "Remove trailing instances of tactic connectives from a string.
447A tactic connective is any one of \"THEN\", \"THENL\", \"THEN1\", \">>\", \">|\"
448or \">-\"."
449  (let* ((case-fold-search nil)
450         (pattern (concat tactic-connective-regexp "\\'")))
451    (replace-regexp-in-string pattern "" string)))
452
453(defun hol-find-eval-next-tactic (arg)
454  "Highlights the next tactic in the source and evaluates in the HOL buffer.
455With a prefix ARG, uses `expandf' rather than `e'."
456  (interactive "P")
457  (deactivate-mark)
458  (skip-syntax-forward " ")
459  (let
460      ((term (thing-at-point 'tactic-terminator))
461       (sqb (char-equal (following-char) ?\[)))
462    (while (or term sqb)
463      (cond (term (forward-tactic-terminator 1))
464            (sqb (forward-char)))
465      (skip-syntax-forward " ")
466      (setq term (thing-at-point 'tactic-terminator))
467      (setq sqb (char-equal (following-char) ?\[))))
468  (mark-hol-tactic)
469  (copy-region-as-hol-tactic (region-beginning) (region-end) arg)
470  (goto-char (region-end)))
471
472(defun copy-region-as-hol-tactic (start end arg)
473  "Send selected region to HOL process as tactic."
474  (interactive "r\nP")
475  (let*
476      ((region-string0 (buffer-substring start end))
477       (region-string1 (tactic-cleanup-leading region-string0))
478       (region-string2 (tactic-cleanup-trailing region-string1))
479       (start-offset (- (length region-string0) (length region-string1)))
480       (region-string3 (with-hol-locpragma (+ start start-offset) region-string2))
481       (ste "\"show_typecheck_errors\"")
482       (region-string (concat "let val old = Feedback.current_trace "
483                              ste
484                              " val _ = Feedback.set_trace "
485                              ste
486                              " 0 in ("
487                              region-string3
488                              ") before "
489                              "Feedback.set_trace " ste " old end"))
490       (e-string (concat "proofManagerLib." (if arg "expandf" "e")))
491       (tactic-string (format "%s (%s)" e-string region-string))
492       (sender (if hol-emit-time-elapsed-p
493                   'send-timed-string-to-hol
494                 'send-string-to-hol)))
495    (funcall sender tactic-string hol-echo-commands-p)))
496
497;;; For goaltrees
498(defun copy-region-as-goaltree-tactic (start end)
499  "Send selected region to HOL process as goaltree tactic."
500  (interactive "r\nP")
501  (let* ((region-string (with-hol-locpragma start
502                          (buffer-substring-no-properties start end)))
503         (tactic-string
504           (format "proofManagerLib.expandv (%S,%s) handle e => Raise e"
505                   region-string region-string))
506         (sender (if hol-emit-time-elapsed-p
507                     'send-timed-string-to-hol
508                   'send-string-to-hol)))
509    (funcall sender tactic-string hol-echo-commands-p)))
510
511(defun send-string-as-hol-goal (s)
512  (let ((goal-string (format  "proofManagerLib.g `%s`" s)))
513    (send-raw-string-to-hol goal-string hol-echo-commands-p t)
514    (send-raw-string-to-hol "proofManagerLib.set_backup 100;" nil nil)))
515
516(defun hol-do-goal (arg)
517  "Send term around point to HOL process as goal.
518If prefix ARG is true, or if in transient mark mode, region is active and
519the region contains no backquotes, then send region instead."
520  (interactive "P")
521  (let ((txt (condition-case nil
522                 (with-hol-locpragma (region-beginning)
523                    (buffer-substring (region-beginning) (region-end)))
524               (error nil))))
525    (if (or (and (is-region-active) (= (count ?\` txt) 0))
526            arg)
527      (send-string-as-hol-goal txt)
528    (send-string-as-hol-goal (hol-term-at-point)))))
529
530
531(defun send-string-as-hol-goaltree (s)
532  (let ((goal-string
533         (format  "proofManagerLib.gt `%s` handle e => Raise e" s)))
534    (send-raw-string-to-hol goal-string hol-echo-commands-p t)
535    (send-raw-string-to-hol "proofManagerLib.set_backup 100;" nil nil)))
536
537
538(defun hol-do-goaltree (arg)
539  "Send term around point to HOL process as goaltree.
540If prefix ARG is true, or if in transient mark mode, region is active and
541the region contains no backquotes, then send region instead."
542  (interactive "P")
543  (let ((txt (condition-case nil
544                 (with-hol-locpragma (region-beginning)
545                    (buffer-substring (region-beginning) (region-end)))
546               (error nil))))
547    (if (or (and (is-region-active) (= (count ?\` txt) 0))
548            arg)
549      (send-string-as-hol-goaltree txt)
550    (send-string-as-hol-goaltree (hol-term-at-point)))))
551
552(defun copy-region-as-hol-definition (start end arg)
553  "Send selected region to HOL process as definition/expression.  With a
554prefix arg of 4 (hit control-u once), wrap what is sent so that it becomes
555( .. ) handle e => Raise e, allowing HOL_ERRs to be displayed cleanly.
556With a prefix arg of 16 (hit control-u twice), toggle Moscow ML's quiet-dec
557variable before and after the region is sent."
558  (interactive "r\np")
559  (let* ((buffer-string
560            (with-hol-locpragma start (buffer-substring start end)))
561         (send-string
562          (if (= arg 4)
563              (concat "(" buffer-string ") handle e => Raise e")
564            buffer-string))
565         (sender (if hol-emit-time-elapsed-p
566                     'send-timed-string-to-hol
567                   'send-string-to-hol)))
568    (if (= arg 16) (hol-toggle-quietdec))
569    (funcall sender send-string hol-echo-commands-p)
570    (if (> (length send-string) 300)
571        (send-string-to-hol
572         "val _ = print \"\\n*** Emacs/HOL command completed ***\\n\\n\""))
573    (if (= (prefix-numeric-value arg) 16) (hol-toggle-quietdec))))
574
575
576
577(defun copy-region-as-hol-definition-quietly (start end)
578   (interactive "r")
579   (hol-toggle-quiet-quietdec)
580   (copy-region-as-hol-definition start end 0)
581   (hol-toggle-quiet-quietdec))
582
583
584(defun hol-name-top-theorem (string arg)
585  "Name the top theorem of the proofManagerLib.
586With prefix argument, drop the goal afterwards."
587  (interactive "sName for top theorem: \nP")
588  (if (not (string= string ""))
589      (send-raw-string-to-hol
590       (format "val %s = top_thm()" string)
591       hol-echo-commands-p t))
592  (if arg (send-raw-string-to-hol "proofManagerLib.drop()" hol-echo-commands-p nil)))
593
594(defun hol-start-termination-proof (arg)
595  "Send definition around point to HOL process as Defn.tgoal.
596If prefix ARG is true, or if in transient mark mode, region is active and
597the region contains no backquotes, then send region instead."
598  (interactive "P")
599  (let ((txt (condition-case nil
600                 (with-hol-locpragma (region-beginning)
601                    (buffer-substring (region-beginning) (region-end)))
602               (error nil))))
603    (if (or (and (is-region-active) (= (count ?\` txt) 0))
604            arg)
605      (hol-send-string-as-termination-proof txt)
606    (hol-send-string-as-termination-proof (hol-term-at-point)))))
607
608(defun hol-send-string-as-termination-proof (str)
609  (send-raw-string-to-hol
610   (concat
611    "Defn.tgoal (Defn.Hol_defn \"HOLmode_defn\" `" str "`) handle e => Raise e") nil t))
612
613(defun remove-sml-comments (end)
614  (let (done (start (point)))
615    (while (and (not done) (re-search-forward "(\\*\\|\\*)" end t))
616        (if (string= (match-string 0) "*)")
617            (progn
618              (delete-region (- start 2) (point))
619              (setq done t))
620          ;; found a comment beginning
621          (if (not (remove-sml-comments end)) (setq done t))))
622      (if (not done) (message "Incomplete comment in region given"))
623      done))
624
625(defun remove-quoted-hol-term (bq eq end-marker)
626  (let ((start (point))
627        (bqsize (length bq)))
628    (if (re-search-forward eq end-marker t)
629        (delete-region (- start bqsize) (point))
630      (error
631       (format "Incomplete (%s...%s-quoted) HOL term in region given; \
632starts >%s%s<"
633               bq eq
634               bq
635               (buffer-substring (point) (+ (point) 10)))))))
636
637(defun remove-hol-string (end-marker)
638  (let ((start (point)))
639    (if (re-search-forward "\n\\|[^\\]?\"" end-marker t)
640        (if (string= (match-string 0) "\n")
641            (message "String literal terminated by newline - not allowed!")
642          (delete-region (- start 1) (point))))))
643
644
645(defun remove-sml-junk (start end)
646  "Removes all sml comments, HOL terms and strings in the given region."
647  (interactive "r")
648  (let ((m (make-marker)))
649    (set-marker m end)
650    (save-excursion
651      (goto-char start)
652      (while (re-search-forward "(\\*\\|`\\|\"\\|���\\|���" m t)
653        (let ((ms (match-string 0)))
654          (cond ((string= ms "(*") (remove-sml-comments m))
655                ((string= ms "\"") (remove-hol-string m))
656                ((string= ms "���") (remove-quoted-hol-term "���" "���" m))
657                ((string= ms "���") (remove-quoted-hol-term "���" "���" m))
658                (t ; must be a back-tick
659                 (if (not (looking-at "`"))
660                     (remove-quoted-hol-term "`" "`" m)
661                   (forward-char 1)
662                   (remove-quoted-hol-term "``" "``" m))))))
663      (set-marker m nil))))
664
665(defun remove-sml-lets-locals
666  (start end &optional looking-for-end &optional recursing)
667  "Removes all local-in-ends and let-in-ends from a region.  We assume
668that the buffer has already had HOL terms, comments and strings removed."
669  (interactive "r")
670  (let ((m (if (not recursing) (set-marker (make-marker) end) end))
671        retval)
672    (if (not recursing) (goto-char start))
673    (if (re-search-forward "\\blet\\b\\|\\blocal\\b\\|\\bend\\b" m t)
674        (let ((declstring (match-string 0)))
675          (if (or (string= declstring "let") (string= declstring "local"))
676              (and
677               (remove-sml-lets-locals (- (point) (length declstring)) m t t)
678               (remove-sml-lets-locals start m looking-for-end t)
679               (setq retval t))
680            ;; found an "end"
681            (if (not looking-for-end)
682                (message "End without corresponding let/local")
683              (delete-region start (point))
684              (setq retval t))))
685      ;; didn't find anything
686      (if looking-for-end
687          (message "Let/local without corresponding end")
688        (setq retval t)))
689    (if (not recursing) (set-marker m nil))
690    retval))
691
692(defun word-list-to-regexp (words)
693  (mapconcat (lambda (s) (concat "\\b" s "\\b")) words "\\|"))
694
695(setq hol-open-terminator-regexp
696      (concat ";\\|"
697              (word-list-to-regexp
698               '("val" "fun" "in" "infix[lr]?" "open" "local" "type"
699                 "datatype" "nonfix" "exception" "end" "structure"))))
700
701(setq sml-struct-id-regexp "[A-Za-z][A-Za-z0-9_]*")
702
703(defun send-string-to-hol (string &optional echoit)
704  "Send a string to HOL process."
705  (let ((buf (ensure-hol-buffer-ok))
706        (hol-ok hol-buffer-ready)
707        (tmpbuf (generate-new-buffer "*HOL temporary*"))
708        (old-mark-active (is-region-active)))
709    (unwind-protect
710        (save-excursion
711          (set-buffer tmpbuf)
712          (modify-syntax-entry ?_ "w")
713          (setq hol-buffer-name buf) ; version of this variable in tmpbuf
714          (setq hol-buffer-ready hol-ok) ; version of this variable in tmpbuf
715          (setq case-fold-search nil) ; buffer-local version
716          (insert string)
717          (goto-char (point-min))
718          (remove-sml-junk (point-min) (point-max))
719          (goto-char (point-min))
720          ;; first thing to do is to search through buffer looking for
721          ;; identifiers of form id.id.  When spotted such identifiers need
722          ;; to have the first component of the name loaded.
723          (if hol-auto-load-p
724             (while (re-search-forward (concat "\\(" sml-struct-id-regexp
725                                            "\\)\\.\\w+")
726                                       (point-max) t)
727               (hol-load-string (match-string 1)))
728             t)
729          ;; next thing to do is to look for open declarations
730          (goto-char (point-min))
731          ;; search through buffer for open declarations
732          (while (re-search-forward "\\s-open\\s-" (point-max) t)
733            ;; point now after an open, now search forward to end of
734            ;; buffer or a semi-colon, or an infix declaration or a
735            ;; val or a fun or another open  (as per the regexp defined just
736            ;; before this function definition
737            (let ((start (point))
738                  (end
739                   (save-excursion
740                     (if (re-search-forward hol-open-terminator-regexp
741                                            (point-max) t)
742                         (- (point) (length (match-string 0)))
743                       (point-max)))))
744              (hol-load-modules-in-region start end)))
745          ;; send the string
746          (delete-region (point-min) (point-max))
747          (insert string)
748          (send-buffer-to-hol-maybe-via-file echoit))
749      (kill-buffer tmpbuf)) ; kill buffer always
750    ;; deactivate-mark will have likely been set by all the editting actions
751    ;; in the temporary buffer.  We fix this here, thereby keeping the mark
752    ;; active, if it is active.
753    ;; if in XEmacs, use (zmacs-activate-region) instead.
754    (if (boundp 'deactivate-mark)
755        (if deactivate-mark (setq deactivate-mark nil))
756        (if (and old-mark-active (fboundp 'zmacs-activate-region))
757            (zmacs-activate-region)))))
758
759(defun interactive-send-string-to-hol (string &optional echoit)
760   "Send a string to HOL process."
761   (interactive "sString to send to HOL process: \nP")
762   (if hol-emit-time-elapsed-p
763       (send-timed-string-to-hol string echoit)
764     (send-string-to-hol string echoit)))
765
766(if (null temporary-file-directory)
767    (if (equal system-type 'windows-nt)
768        (if (not (null (getenv "TEMP")))
769            (setq temporary-file-directory (getenv "TEMP")))
770      (setq temporary-file-directory "/tmp")))
771
772(defun make-temp-file-xemacs (prefix &optional dir-flag)
773  "Create a temporary file.
774The returned file name (created by appending some random characters at the end
775of PREFIX, and expanding against `temporary-file-directory' if necessary,
776is guaranteed to point to a newly created empty file.
777You can then use `write-region' to write new data into the file.
778
779If DIR-FLAG is non-nil, create a new empty directory instead of a file."
780  (let (file)
781    (while (condition-case ()
782	       (progn
783		 (setq file
784		       (make-temp-name
785			(expand-file-name prefix temporary-file-directory)))
786		 (if dir-flag
787		     (make-directory file)
788		   (write-region "" nil file nil 'silent nil)) ;; 'excl
789		 nil)
790	    (file-already-exists t))
791      ;; the file was somehow created by someone else between
792      ;; `make-temp-name' and `write-region', let's try again.
793      nil)
794    file))
795
796(defvar hol-mode-to-delete nil
797  "String optionally containing name of last temporary file used to transmit
798HOL sources to a running session (using \"use\")")
799
800(defun send-buffer-to-hol-maybe-via-file (&optional echoit)
801  "Send the contents of current buffer to HOL, possibly putting it into a
802file to \"use\" first."
803  (if (< 500 (buffer-size))
804          (let ((fname (if (fboundp 'make-temp-file)
805                              ;; then
806                                    (make-temp-file "hol")
807                              ;; else
808                                    (make-temp-file-xemacs "hol")
809                                 )))
810            (if (stringp hol-mode-to-delete)
811                (progn (condition-case nil
812                           (delete-file hol-mode-to-delete)
813                         (error nil))
814                       (setq hol-mode-to-delete nil)))
815            ; below, use visit parameter = 1 to stop message in mini-buffer
816            (write-region (point-min) (point-max) fname nil 1)
817            (send-raw-string-to-hol (format "use \"%s\"" fname) nil t)
818            (setq hol-mode-to-delete fname))
819    (send-raw-string-to-hol (buffer-string) echoit t)))
820
821
822(defun send-raw-string-to-hol (string echoit newstart)
823  "Sends a string in the raw to HOL.  Not for interactive use."
824  (let ((buf (ensure-hol-buffer-ok)))
825    (if echoit
826        (save-excursion
827          (set-buffer buf)
828          (goto-char (point-max))
829          (princ (concat string ";") (get-buffer buf))
830          (goto-char (point-max))
831          (comint-send-input)
832          (hol-recentre))
833      (comint-send-string buf (concat string ";\n")))))
834
835
836(defun hol-backup ()
837  "Perform a HOL backup."
838  (interactive)
839  (send-raw-string-to-hol "proofManagerLib.b()" hol-echo-commands-p t))
840
841(defun hol-user-backup ()
842  "Perform a HOL backup to a user-defined save-point."
843  (interactive)
844  (send-raw-string-to-hol "proofManagerLib.restore()" hol-echo-commands-p t))
845
846(defun hol-print-info ()
847  "Show some information about the currently running HOL and the settings of hol-mode."
848  (interactive)
849  (send-raw-string-to-hol
850   (concat "print_current_hol_status" "\""
851     hol-executable "\" \"" holmake-executable "\" ();") hol-echo-commands-p t))
852
853(defun hol-user-save-backup ()
854  "Saves the current status of the proof for later backups to this point."
855  (interactive)
856  (send-raw-string-to-hol "proofManagerLib.save()" hol-echo-commands-p t))
857
858(defun hol-print-goal ()
859  "Print the current HOL goal."
860  (interactive)
861  (send-raw-string-to-hol "proofManagerLib.p()" hol-echo-commands-p t))
862
863(defun hol-print-all-goals ()
864  "Print all the current HOL goals."
865  (interactive)
866  (send-raw-string-to-hol "proofManagerLib.status()" hol-echo-commands-p t))
867
868(defun hol-interrupt ()
869  "Perform a HOL interrupt."
870  (interactive)
871  (let ((buf (ensure-hol-buffer-ok)))
872    (interrupt-process (get-buffer-process buf))))
873
874
875(defun hol-kill ()
876  "Kill HOL process."
877  (interactive)
878  (let ((buf (ensure-hol-buffer-ok)))
879    (kill-process (get-buffer-process buf))))
880
881(defun hol-recentre ()
882  "Display the HOL window in such a way that it displays most text."
883  (interactive)
884  (if (get-buffer-window hol-buffer-name t)
885      (save-selected-window
886        (select-window (get-buffer-window hol-buffer-name t))
887        (and hol-raise-on-recentre (raise-frame))
888        (goto-char (point-max))
889        (recenter -1))))
890
891(defun hol-rotate (arg)
892  "Rotate the goal stack N times.  Once by default."
893  (interactive "p")
894  (send-raw-string-to-hol (format "proofManagerLib.r %d" arg)
895                          hol-echo-commands-p t))
896
897(defun hol-scroll-up (arg)
898  "Scrolls the HOL window."
899  (interactive "P")
900  (ensure-hol-buffer-ok)
901  (save-excursion
902    (select-window (get-buffer-window hol-buffer-name t))
903    (scroll-up arg)))
904
905(defun hol-scroll-down (arg)
906  "Scrolls the HOL window."
907  (interactive "P")
908  (ensure-hol-buffer-ok)
909  (save-excursion
910    (select-window (get-buffer-window hol-buffer-name t))
911    (scroll-down arg)))
912
913(defun hol-use-file (filename)
914  "Gets HOL session to \"use\" a file."
915  (interactive "fFile to use: ")
916  (send-raw-string-to-hol (concat "use \"" filename "\";")
917                          hol-echo-commands-p nil))
918
919(defun hol-load-string (s)
920  "Loads the ML object file NAME.uo; checking that it isn't already loaded."
921  (let* ((buf (ensure-hol-buffer-ok))
922         (mys (format "%s" s)) ;; gets rid of text properties
923         (commandstring
924          (concat "val _ = if List.exists (fn s => s = \""
925                  mys
926                  "\") (emacs_hol_mode_loaded()) then () else "
927                  "(print  \"Loading " mys
928                  "\\n\"; " "Meta.load \"" mys "\");\n")))
929    (comint-send-string buf commandstring)))
930
931(defun hol-load-modules-in-region (start end)
932  "Attempts to load all of the words in the region as modules."
933  (interactive "rP")
934  (save-excursion
935    (goto-char start)
936    (while (re-search-forward (concat "\\b" sml-struct-id-regexp "\\b") end t)
937      (hol-load-string (match-string 0)))))
938
939(defun hol-load-file (arg)
940  "Gets HOL session to \"load\" the file at point.
941If there is no filename at point, then prompt for file.  If the region
942is active (in transient mark mode) and it looks like it might be a
943module name or a white-space delimited list of module names, then send
944region instead. With prefix ARG prompt for a file-name to load."
945  (interactive "P")
946  (let* ((wap (word-at-point))
947         (txt (condition-case nil
948                  (buffer-substring (region-beginning) (region-end))
949                (error nil))))
950    (cond (arg (hol-load-string (read-string "Library to load: ")))
951          ((and (is-region-active)
952                (string-match (concat "^\\(\\s-*" sml-struct-id-regexp
953                                      "\\)+\\s-*$") txt))
954           (hol-load-modules-in-region (region-beginning) (region-end)))
955          ((and wap (string-match "^\\w+$" wap)) (hol-load-string wap))
956          (t (hol-load-string (read-string "Library to load: "))))))
957
958
959(defun hol-mode-init-sml ()
960   (hol-toggle-quiet-quietdec)
961   (send-raw-string-to-hol hol-mode-sml-init-command nil nil)
962   (hol-toggle-quiet-quietdec))
963
964(defun turn-off-hol-font-lock (oldvar)
965  (interactive)
966  (if (not oldvar)
967      (progn
968        (message "Turning on font-lock mode does nothing in HOL mode")
969        (setq font-lock-defaults nil)))
970  (setq font-lock-mode nil))
971
972(defun holmake (&optional dir)
973   (interactive "DRun Holmake in dir: ")
974   (if (not (null dir))
975      (save-excursion
976         (set-buffer (get-buffer-create "*Holmake*"))
977         (delete-region (point-min) (point-max))
978         (cd (expand-file-name dir)))
979      )
980   (let* ((buf (make-comint "Holmake"
981                  holmake-executable nil "--qof" "-k")))
982      (save-excursion
983         (set-buffer buf)
984         (font-lock-mode 0)
985         (make-local-variable 'font-lock-function)
986         (setq font-lock-function 'turn-off-hol-font-lock)
987         (setq comint-preoutput-filter-functions '(holmakepp-output-filter)))
988         (setq comint-scroll-show-maximum-output t)
989         (setq comint-scroll-to-bottom-on-output t)
990      (display-buffer buf)
991   ))
992
993;** hol map keys and function definitions
994(defun hol-executable-with-bare ()
995  (if hol-bare-p (concat hol-executable ".bare")
996                 hol-executable))
997
998(defun hol ()
999  "Runs a HOL session in a comint window."
1000  (interactive)
1001  (let* ((hol-was-ok (hol-buffer-ok hol-buffer-name))
1002         (buf (make-comint "HOL" (hol-executable-with-bare))))
1003    (setq hol-buffer-name (buffer-name buf))
1004    (switch-to-buffer buf)
1005    (setq comint-prompt-regexp "^- ")
1006    (setq hol-buffer-name (buffer-name buf))
1007    ;; must go to ridiculous lengths to ensure that font-lock-mode is
1008    ;; turned off and stays off
1009    (font-lock-mode 0)
1010    (make-local-variable 'font-lock-function)
1011    (setq font-lock-function 'turn-off-hol-font-lock)
1012    (make-local-variable 'comint-preoutput-filter-functions)
1013    (holpp-quiet-reset)
1014    (setq comint-preoutput-filter-functions '(holpp-output-filter))
1015    (setq comint-scroll-show-maximum-output t)
1016    (setq comint-scroll-to-bottom-on-output t)
1017    (if hol-was-ok t (hol-mode-init-sml))
1018    (send-raw-string-to-hol
1019     "val _ = Parse.current_backend := PPBackEnd.emacs_terminal;" nil nil)))
1020
1021(defun hol-toggle-bare ()
1022  "Toggles the elisp variable 'hol-bare-p."
1023  (interactive)
1024  (setq hol-bare-p (not hol-bare-p))
1025  (concat "using " (hol-executable-with-bare)))
1026
1027(defun hol-display ()
1028   (interactive)
1029   (display-buffer hol-buffer-name));
1030
1031
1032(defun hol-vertical ()
1033  "Runs a HOL session after splitting the window"
1034  (interactive)
1035  (split-window-vertically)
1036  (other-window 1)
1037  (hol)
1038  (other-window -1))
1039
1040(defun hol-horizontal ()
1041  "Runs a HOL session after splitting the window"
1042  (interactive)
1043  (split-window-horizontally)
1044  (other-window 1)
1045  (hol)
1046  (other-window -1))
1047
1048(defun hol-new-frame ()
1049  "Runs a HOL session in a new frame"
1050  (interactive)
1051  (let* ((curframe (selected-frame))
1052         (oldtop (cdr (assoc 'top (frame-parameters))))
1053         (oldleft (cdr (assoc 'left (frame-parameters))))
1054         (newframe (make-frame)))
1055    (set-frame-position newframe (+ oldleft 500) oldtop) ; disgusting
1056    (select-frame newframe)
1057    (hol)
1058    (select-frame-set-input-focus curframe)))
1059
1060(defvar hol-new-buffer-style hol-new-buffer-style-default)
1061
1062(setq hol-new-buffer-style-alist
1063      '((horizontal . hol-horizontal)
1064        (vertical . hol-vertical)
1065        (new-frame . hol-new-frame)))
1066
1067(defun hol-with-region ()
1068  "Starts a HOL session and pastes selected region into it. If there is no active region, pastes whole buffer."
1069  (interactive)
1070  (let* ((style-str (completing-read
1071                     (concat "HOL buffer position ("
1072                             (symbol-name hol-new-buffer-style)
1073                             "): ")
1074                     '("horizontal" "vertical" "new-frame")
1075                     nil
1076                     t
1077                     nil
1078                     nil
1079                     (symbol-name hol-new-buffer-style)
1080                     t))
1081         (style (intern style-str))
1082         (starter (cdr (assoc style hol-new-buffer-style-alist))))
1083    (setq hol-new-buffer-style style)
1084    (funcall starter)
1085    (if (region-active-p)
1086        (copy-region-as-hol-definition-quietly (region-beginning) (region-end))
1087      (copy-region-as-hol-definition-quietly (point-min) (point-max)))))
1088
1089(defun run-program (filename niceness)
1090  "Runs a PROGRAM in a comint window, with a given (optional) NICENESS."
1091  (interactive "fProgram to run: \nP")
1092  (let* ((niceval (cond ((null niceness) 0)
1093                        ((listp niceness) 10)
1094                        (t (prefix-numeric-value niceness))))
1095         (progname (format "%s(n:%d)"
1096                          (file-name-nondirectory filename)
1097                          niceval))
1098         (buf (cond ((> niceval 0)
1099                     (make-comint progname "nice" nil
1100                                  (format "-%d" niceval)
1101                                  (expand-file-name filename)))
1102                   (t (make-comint progname
1103                                   (expand-file-name filename)
1104                                   nil)))))
1105    (switch-to-buffer buf)))
1106
1107(defun hol-toggle-var (s)
1108  "Toggles the boolean variable STRING."
1109  (message (concat "Toggling " s))
1110  (send-raw-string-to-hol
1111   (format (concat "val _ = (%s := not (!%s);"
1112                   "print (\"*** %s now \" ^"
1113                   "Bool.toString (!%s)^\" ***\\n\"))")
1114           s s s s) nil nil))
1115
1116(defun hol-toggle-var-quiet (s)
1117  "Toggles the boolean variable STRING."
1118  (send-raw-string-to-hol
1119   (format "val _ = (%s := not (!%s));"
1120           s s) nil nil))
1121
1122(defun hol-toggle-trace (s &optional arg)
1123  "Toggles the trace variable STRING between zero and non-zero.  With prefix
1124argument N, sets the trace to that value in particular."
1125  (interactive "sTrace name: \nP")
1126  (if (null arg)
1127      (progn
1128        (message (concat "Toggling " s))
1129        (send-raw-string-to-hol
1130         (format "val _ = let val nm = \"%s\"
1131                      fun findfn r = #name r = nm
1132                      val old =
1133                            #trace_level (valOf (List.find findfn (traces())))
1134                  in
1135                      print (\"** \"^nm^\" trace now \");
1136                      if 0 < old then (set_trace nm 0; print \"off\\n\")
1137                      else (set_trace nm 1; print \"on\\n\")
1138                  end handle Option =>
1139                        print \"** No such trace var: \\\"%s\\\"\\n\""
1140                 s s) nil nil))
1141    (let ((n (prefix-numeric-value arg)))
1142      (message (format "Setting %s to %d" s n))
1143      (send-raw-string-to-hol
1144       (format "val _ = (set_trace \"%s\" %d; print \"** %s trace now %d\\n\")
1145                        handle HOL_ERR _ =>
1146                           print \"** No such trace var: \\\"%s\\\"\\n\""
1147               s n s n s) nil nil))))
1148
1149(defun hol-toggle-unicode ()
1150  "Toggles the \"Unicode\" trace."
1151  (interactive)
1152  (hol-toggle-trace "Unicode"))
1153
1154
1155(defun hol-toggle-emacs-tooltips ()
1156  "Toggles whether HOL produces tooltip information while pretty-printing."
1157  (interactive)
1158  (hol-toggle-trace "PPBackEnd show types"))
1159
1160(defun hol-toggle-pp-styles ()
1161  "Toggles whether HOL produces style informations while pretty-printing."
1162  (interactive)
1163  (hol-toggle-trace "PPBackEnd use styles"))
1164
1165(defun hol-toggle-pp-cases ()
1166  "Toggles the \"pp_cases\" trace."
1167  (interactive)
1168  (hol-toggle-trace "pp_cases")
1169  (hol-toggle-trace "use pmatch_pp"))
1170
1171(defun hol-toggle-pp-annotations ()
1172  "Toggles whether HOL produces annotations while pretty-printing."
1173  (interactive)
1174  (hol-toggle-trace "PPBackEnd use annotations"))
1175
1176(defun hol-toggle-goalstack-fvs ()
1177  "Toggles the trace \"Goalstack.print_goal_fvs\"."
1178  (interactive)
1179  (hol-toggle-trace "Goalstack.print_goal_fvs"))
1180
1181(defun hol-toggle-goalstack-print-goal-at-top ()
1182  "Toggles the trace \"Goalstack.print_goal_at_top\"."
1183  (interactive)
1184  (hol-toggle-trace "Goalstack.print_goal_at_top"))
1185
1186(defun hol-toggle-goalstack-num-assums (arg)
1187  "Toggles the number of assumptions shown in a goal."
1188  (interactive "nMax. number of visible assumptions: ")
1189  (hol-toggle-trace "Goalstack.howmany_printed_assums" arg))
1190
1191(defun hol-toggle-goalstack-num-subgoals (arg)
1192  "Toggles the number of shown subgoals."
1193  (interactive "nMax. number of shown subgoals: ")
1194  (hol-toggle-trace "Goalstack.howmany_printed_subgoals" arg))
1195
1196(defun hol-toggle-simplifier-trace (arg)
1197  "Toggles the trace \"simplifier\".  With ARG sets trace to this value."
1198  (interactive "P")
1199  (hol-toggle-trace "simplifier" arg))
1200
1201(defun hol-toggle-show-types (arg)
1202  "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)."
1203  (interactive "P")
1204  (hol-toggle-trace "types" arg))
1205
1206(defun hol-toggle-show-types-verbosely ()
1207  "Toggles the global show_types_verbosely variable."
1208  (interactive)
1209  (hol-toggle-var "Globals.show_types_verbosely"))
1210
1211(defun hol-toggle-show-numeral-types()
1212  "Toggles the global show_numeral_types variable."
1213  (interactive)
1214  (hol-toggle-var "Globals.show_numeral_types"))
1215
1216(defun hol-toggle-show-assums()
1217  "Toggles the global show_assums variable."
1218  (interactive)
1219  (hol-toggle-var "Globals.show_assums"))
1220
1221(defun hol-toggle-show-tags()
1222  "Toggles the global show_tags variable."
1223  (interactive)
1224  (hol-toggle-var "Globals.show_tags"))
1225
1226(defun hol-toggle-show-axioms()
1227  "Toggles the global show_axioms variable."
1228  (interactive)
1229  (hol-toggle-var "Globals.show_axioms"))
1230
1231(defun hol-toggle-quietdec ()
1232  "Toggles quiet declarations in the interactive system."
1233  (interactive)
1234  (message "Toggling 'Quiet declaration'")
1235  (send-raw-string-to-hol
1236   (concat
1237    "val _ = print (\"*** 'Quiet declaration' now \" ^"
1238    "Bool.toString (HOL_Interactive.toggle_quietdec()) ^ \" ***\\n\")") nil nil)
1239  (hol-toggle-var "Globals.interactive"))
1240
1241(defun hol-toggle-quiet-quietdec ()
1242  "Toggles quiet declarations in the interactive system."
1243  (interactive)
1244  (send-raw-string-to-hol
1245    "val _ = HOL_Interactive.toggle_quietdec()" nil nil)
1246  (hol-toggle-var-quiet "Globals.interactive"))
1247
1248(defun hol-toggle-show-times()
1249  "Toggles the elisp variable 'hol-emit-time-elapsed-p."
1250  (interactive)
1251  (setq hol-emit-time-elapsed-p (not hol-emit-time-elapsed-p))
1252  (message (if hol-emit-time-elapsed-p "Elapsed times WILL be displayed"
1253             "Elapsed times WON'T be displayed")))
1254
1255(defun hol-toggle-echo-commands ()
1256  "Toggles the elisp variable 'hol-echo-commands-p."
1257  (interactive)
1258  (setq hol-echo-commands-p (not hol-echo-commands-p))
1259  (message (if hol-echo-commands-p "Commands WILL be echoed"
1260             "Commands WON'T be echoed")))
1261
1262(defun hol-toggle-auto-load ()
1263  "Toggles the elisp variable 'hol-auto-load-p."
1264  (interactive)
1265  (setq hol-auto-load-p (not hol-auto-load-p))
1266  (message (if hol-auto-load-p "automatic loading ON"
1267             "automatic loading OFF")))
1268
1269(defun hol-toggle-ppbackend ()
1270  "Toggles between using the Emacs and \"raw\" terminal pretty-printing."
1271  (interactive)
1272  (send-raw-string-to-hol
1273   (concat
1274    "val _ = if #name (!Parse.current_backend) = \"emacs_terminal\" then"
1275    "(Parse.current_backend := PPBackEnd.raw_terminal;"
1276    "print \"*** PP Backend now \\\"raw\\\" ***\\n\")"
1277    "else (Parse.current_backend := PPBackEnd.emacs_terminal;"
1278    "print \"*** PP Backend now \\\"emacs\\\" ***\\n\")") nil nil))
1279
1280(defun hol-restart-goal ()
1281  "Restarts the current goal."
1282  (interactive)
1283  (send-raw-string-to-hol "proofManagerLib.restart()" hol-echo-commands-p t))
1284
1285(defun hol-drop-goal ()
1286  "Drops the current goal."
1287  (interactive)
1288  (send-raw-string-to-hol "proofManagerLib.drop()" hol-echo-commands-p t))
1289
1290(defun hol-open-string (prefixp)
1291  "Opens HOL modules, prompting for the name of the module to load.
1292With prefix ARG, toggles quietdec variable before and after opening,
1293potentially saving a great deal of time as tediously large modules are
1294printed out.  (That's assuming that quietdec is false to start with.)"
1295  (interactive "P")
1296  (let* ((prompt0 "Name of module to (load and) open")
1297         (prompt (concat prompt0 (if prefixp " (toggling quietness)") ": "))
1298         (module-name (read-string prompt)))
1299    (hol-load-string module-name)
1300    (if prefixp (hol-toggle-quietdec))
1301    (send-raw-string-to-hol (concat "open " module-name) hol-echo-commands-p t)
1302    (if prefixp (hol-toggle-quietdec))))
1303
1304(defun hol-db-match (tm)
1305  "Does a DB.match [] on the given TERM (given as a string, without quotes) and formats the result nicely."
1306  (interactive "sTerm to match on: ")
1307  (send-raw-string-to-hol (format "Hol_pp.print_match [] (Term`%s`)" tm)
1308                          hol-echo-commands-p t))
1309
1310(defun hol-db-find (tm)
1311  "Does a DB.find on the given string and formats the result nicely."
1312  (interactive "sTheorem name part: ")
1313  (send-raw-string-to-hol (format "Hol_pp.print_find \"%s\"" tm)
1314                          hol-echo-commands-p t))
1315
1316(defun hol-db-check (ty)
1317  "Does a sanity check on the current theory."
1318  (interactive "sTheory name: ")
1319  (send-raw-string-to-hol (format "Sanity.sanity_check_theory \"%s\"" ty)
1320                          hol-echo-commands-p t))
1321
1322(defun hol-db-check-current ()
1323  "Does a sanity check on the current theory."
1324  (interactive)
1325  (send-raw-string-to-hol "Sanity.sanity_check()"
1326                          hol-echo-commands-p t))
1327
1328(defun hol-drop-all-goals ()
1329  "Drops all HOL goals from the current proofs object."
1330  (interactive)
1331  (send-raw-string-to-hol
1332   (concat "proofManagerLib.dropn (case proofManagerLib.status() of "
1333           "Manager.PRFS l => List.length l)") nil t))
1334
1335(defun hol-subgoal-tactic (p)
1336  "Without a prefix argument, sends term at point (delimited by backquote
1337characters) as a subgoal to prove.  Will usually create at least two sub-
1338goals; one will be the term just sent, and the others will be the term sent
1339STRIP_ASSUME'd onto the assumption list of the old goal.  This mimicks what
1340happens with the \"by\" command.
1341
1342With a prefix argument, sends the delimited term as if the
1343argument of a \"suffices_by\" command, making two new goals: the
1344first is to show that the new term implies the old goal, and the
1345second is to show the new term.
1346
1347(Loads the BasicProvers module if not already loaded.)"
1348  (interactive "P")
1349  (let ((tactic (if p "Tactical.Q_TAC Tactic.SUFF_TAC"
1350                      "(fn q => BasicProvers.byA(q,ALL_TAC))")))
1351    (send-string-to-hol
1352     (format "proofManagerLib.e (%s `%s`)"
1353             tactic
1354             (hol-term-at-point)))))
1355
1356
1357;; (defun hol-return-key ()
1358;;   "Run comint-send-input, but only if both: the user is editting the
1359;; last command in the buffer, and that command ends with a semicolon.
1360;; Otherwise, insert a newline at point."
1361;;   (interactive)
1362;;   (let ((comand-finished
1363;;          (let ((process (get-buffer-process (current-buffer))))
1364;;            (and (not (null process))
1365;;                 (let ((pmarkpos (marker-position
1366;;                                  (process-mark process))))
1367;;                   (and (< (point) pmarkpos)
1368;;                        (string-match ";[ \t\n\r]*$"
1369;;                                      (buffer-substring pmarkpos
1370;;                                                        (point-max)))))))))
1371;;     (if command-finished
1372;;         (progn
1373;;           (goto-char (point-max))
1374;;           (comint-send-input))
1375;;       (insert "\n"))))
1376
1377;; (define-key comint-mode-map "\r" 'hol-return-key)
1378
1379
1380
1381;;templates
1382(defun hol-extract-script-name (arg)
1383  "Return the name of the theory associated with the given filename"
1384(let* (
1385   (pos (string-match "[^/]*Script\.sml" arg)))
1386   (cond (pos (substring arg pos -10))
1387         (t "<insert theory name here>"))))
1388
1389(defun hol-template-new-script-file ()
1390  "Inserts standard template for a HOL theory"
1391   (interactive)
1392   (insert "open HolKernel Parse boolLib bossLib;\n\nval _ = new_theory \"")
1393   (insert (hol-extract-script-name buffer-file-name))
1394   (insert "\";\n\n\n\n\nval _ = export_theory();\n\n"))
1395
1396(defun hol-template-comment-star ()
1397   (interactive)
1398   (insert "\n\n")
1399   (insert "(******************************************************************************)\n")
1400   (insert "(*                                                                            *)\n")
1401   (insert "(*                                                                            *)\n")
1402   (insert "(*                                                                            *)\n")
1403   (insert "(******************************************************************************)\n"))
1404
1405(defun hol-template-comment-minus ()
1406   (interactive)
1407   (insert "\n\n")
1408   (insert "(* -------------------------------------------------------------------------- *)\n")
1409   (insert "(*                                                                            *)\n")
1410   (insert "(*                                                                            *)\n")
1411   (insert "(*                                                                            *)\n")
1412   (insert "(* -------------------------------------------------------------------------- *)\n"))
1413
1414(defun hol-template-comment-equal ()
1415   (interactive)
1416   (insert "\n\n")
1417   (insert "(* ========================================================================== *)\n")
1418   (insert "(*                                                                            *)\n")
1419   (insert "(*                                                                            *)\n")
1420   (insert "(*                                                                            *)\n")
1421   (insert "(* ========================================================================== *)\n"))
1422
1423(defun hol-template-define (name)
1424   (interactive "sNew name: ")
1425   (insert "val ")
1426   (insert name)
1427   (insert "_def = Define `")
1428   (insert name)
1429   (insert " = `;\n"))
1430
1431(defun hol-template-store-thm (name)
1432   (interactive "sTheorem name: ")
1433   (insert "val ")
1434   (insert name)
1435   (insert " = store_thm(")
1436   (cond ((> (length name) 30) (insert "\n  "))
1437          (t t))
1438   (insert "\"")
1439   (insert name)
1440   (insert "\",\n  ``  ``,\n"))
1441
1442(defun hol-template-new-datatype ()
1443   (interactive)
1444   (insert "val _ = Datatype `TREE = LEAF ('a -> num) | BRANCH TREE TREE`;\n"))
1445
1446;;checking for trouble with names in store_thm, save_thm, Define
1447(setq store-thm-regexp
1448   "val[ \t\n]*\\([^ \t\n]*\\)[ \t\n]*=[ \t\n]*store_thm[ \t\n]*([ \t\n]*\"\\([^\"]*\\)\"")
1449(setq save-thm-regexp
1450   "val[ \t\n]*\\([^ \t\n]*\\)[ \t\n]*=[ \t\n]*save_thm[ \t\n]*([ \t\n]*\"\\([^\"]*\\)\"")
1451(setq define-thm-regexp
1452   "val[ \t\n]*\\([^ \t\n]*\\)_def[ \t\n]*=[ \t\n]*Define[ \t\n]*`[ \t\n(]*\$?\\([^ \t\n([!?:]*\\)")
1453
1454(setq statement-eq-regexp-list (list store-thm-regexp save-thm-regexp define-thm-regexp))
1455
1456(defun hol-correct-eqstring (s1 p1 s2 p2)
1457  (interactive)
1458  (let (choice)
1459    (setq choice 0)
1460    (while (eq choice 0)
1461      (message
1462       (concat
1463	"Different names used. Please choose one:\n(0) "
1464	s1 "\n(1) " s2 "\n(i) ignore"))
1465      (setq choice (if (fboundp 'read-char-exclusive)
1466		       (read-char-exclusive)
1467		     (read-char)))
1468      (cond ((= choice ?0) t)
1469	    ((= choice ?1) t)
1470	    ((= choice ?i) t)
1471	    (t (progn (setq choice 0) (ding))))
1472      )
1473    (if (= choice ?i) t
1474    (let (so sr pr)
1475      (cond ((= choice ?0) (setq so s1 sr s2 pr p2))
1476	    (t             (setq so s2 sr s1 pr p1)))
1477      (delete-region pr (+ pr (length sr)))
1478      (goto-char pr)
1479      (insert so)
1480      ))))
1481
1482
1483(defun hol-check-statement-eq-string ()
1484  (interactive)
1485  (save-excursion
1486  (dolist (current-regexp statement-eq-regexp-list t)
1487  (goto-char 0)
1488  (let (no-error-found s1 p1 s2 p2)
1489    (while (re-search-forward current-regexp nil t)
1490      (progn (setq s1 (match-string-no-properties 1))
1491             (setq s2 (match-string-no-properties 2))
1492             (setq p1 (match-beginning 1))
1493             (setq p2 (match-beginning 2))
1494             (setq no-error-found (string= s1 s2))
1495             (if no-error-found t (hol-correct-eqstring s1 p1 s2 p2)))))
1496  (message "checking for problematic names done"))))
1497
1498
1499;;indentation and other cleanups
1500(defun hol-replace-tabs-with-spaces ()
1501   (save-excursion
1502      (goto-char (point-min))
1503      (while (search-forward "\t" nil t)
1504         (delete-region (- (point) 1) (point))
1505         (let* ((count (- tab-width (mod (current-column) tab-width))))
1506           (dotimes (i count) (insert " "))))))
1507
1508(defun hol-remove-tailing-whitespaces ()
1509   (save-excursion
1510      (goto-char (point-min))
1511      (while (re-search-forward " +$" nil t)
1512         (delete-region (match-beginning 0) (match-end 0)))))
1513
1514
1515(defun hol-remove-tailing-empty-lines ()
1516   (save-excursion
1517      (goto-char (point-max))
1518      (while (bolp) (delete-char -1))
1519      (insert "\n")))
1520
1521(defun hol-cleanup-buffer ()
1522   (interactive)
1523   (hol-replace-tabs-with-spaces)
1524   (hol-remove-tailing-whitespaces)
1525   (hol-remove-tailing-empty-lines)
1526   (message "Buffer cleaned up!"))
1527
1528;;replace common unicode chars with ascii version
1529(setq hol-unicode-replacements '(
1530  (nil "��" "~")
1531  (nil "���" "/\\\\")
1532  (nil "���" "\\\\/")
1533  (nil "���" "==>")
1534  (nil "���" "<=>")
1535  (nil "���" "<=/=>")
1536  (nil "���" "<>")
1537  (nil "���" "?")
1538  (nil "���" "!")
1539  (nil "��" "\\\\")
1540  (nil "���" "``")
1541  (nil "���" "``")
1542  (nil "���" "`")
1543  (nil "���" "`")
1544  (t "���" "IN")
1545  (t "���" "NOTIN")
1546  (nil "��" "'a")
1547  (nil "��" "'b")
1548  (nil "��" "'c")
1549  (nil "��" "'d")
1550  (nil "��" "'e")
1551  (nil "��" "'f")
1552  (nil "��" "'g")
1553  (nil "��" "'h")
1554  (nil "��" "'i")
1555  (nil "��" "'j")
1556  (nil "��" "'l")
1557  (nil "��" "'m")
1558  (nil "��" "'n")
1559  (nil "��" "'o")
1560  (nil "��" "'p")
1561  (nil "��" "'q")
1562  (nil "��" "'r")
1563  (nil "��" "'s")
1564  (nil "��" "'t")
1565  (nil "��" "'u")
1566  (nil "��" "'v")
1567  (nil "��" "'w")
1568  (nil "��" "'x")
1569  (nil "��" "'y")
1570  (t "������" "<=+")
1571  (t ">���" ">+")
1572  (t "<���" "<+")
1573  (t "������" ">=+")
1574  (t "���" "<=")
1575  (t "���" ">=")
1576  (nil "���" "^+")
1577  (t "������" "EMPTY_REL")
1578  (t "�������" "RUNIV")
1579  (t "������" "RSUBSET")
1580  (t "������" "RUNION")
1581  (t "������" "RINTER")
1582  (t "���" "EMPTY")
1583  (t "����" "UNIV")
1584  (t "���" "SUBSET")
1585  (t "���" "UNION")
1586  (t "���" "INTER")
1587  (t "���" "??")
1588  (t "���" "||")
1589  (t "���" "<<")
1590  (t "���" ">>")
1591  (t "���" ">>>")
1592  (t "���" "#>>")
1593  (t "���" "#<<")
1594))
1595
1596
1597(defun replace-string-in-buffer (s_old s_new)
1598   (save-excursion
1599      (goto-char (point-min))
1600      (while (search-forward s_old nil t)
1601         (replace-match s_new))))
1602
1603(defun replace-string-in-buffer_ensure_ws (s_old s_new)
1604  (replace-string-in-buffer (concat " " s_old " ") (concat " " s_new " "))
1605  (replace-string-in-buffer (concat s_old " ") (concat " " s_new " "))
1606  (replace-string-in-buffer (concat " " s_old) (concat " " s_new " "))
1607  (replace-string-in-buffer s_old (concat " " s_new " "))
1608)
1609
1610(defun hol-remove-unicode ()
1611  (interactive)
1612  (save-excursion
1613    (save-restriction
1614      (if (use-region-p) (narrow-to-region (region-beginning) (region-end)))
1615      (dolist (elt hol-unicode-replacements)
1616        (if (nth 0 elt)
1617          (replace-string-in-buffer_ensure_ws (nth 1 elt) (nth 2 elt))
1618          (replace-string-in-buffer (nth 1 elt) (nth 2 elt))
1619          )))))
1620
1621
1622;;load-path
1623(defun ml-quote (s)
1624   (let* (
1625     (s1 (replace-regexp-in-string "\\\\" "\\\\\\\\" s))
1626     (s2 (replace-regexp-in-string "\n" "\\\\n" s1))
1627     (s3 (replace-regexp-in-string "\t" "\\\\t" s2))
1628     (s4 (replace-regexp-in-string "\"" "\\\\\"" s3))
1629   ) s4))
1630
1631(defun hol-add-load-path (path)
1632  (interactive "DAdd new load-path: ")
1633  (let ((epath (expand-file-name path)))
1634  (if (file-accessible-directory-p epath)
1635     (progn
1636        (send-raw-string-to-hol
1637            (concat "loadPath := \"" (ml-quote epath) "\" :: !loadPath;")
1638            nil nil)
1639        (message (concat "Load-path \"" epath "\" added.")))
1640     (progn (ding) (message "Not a directory!")))
1641))
1642
1643
1644(defun hol-show-current-load-paths ()
1645   (interactive)
1646   (send-raw-string-to-hol "print_current_load_paths ()"
1647   nil nil))
1648
1649(defun hol-type-info ()
1650   "Gives informations about the type of a term"
1651   (interactive)
1652   (let* ((txt (buffer-substring-no-properties (region-beginning) (region-end)))
1653          (use-marked (and (is-region-active) (= (count ?\` txt) 0)))
1654          (at-point-term (thing-at-point 'hol-term))
1655
1656          (main-term (ml-quote (if use-marked txt at-point-term)))
1657          (context-term (ml-quote (if use-marked at-point-term "")))
1658          (command-s (concat "print_type_of_in_context true "
1659                      (if use-marked (concat "(SOME \"" context-term "\")") "NONE")
1660                      " \"" main-term "\"")))
1661   (send-raw-string-to-hol command-s nil nil)))
1662
1663
1664(defun holpp-decode-color (code)
1665  (cond ((equal code "0") "#000000")
1666        ((equal code "1") "#840000")
1667        ((equal code "2") "#008400")
1668        ((equal code "3") "#848400")
1669        ((equal code "4") "#000084")
1670        ((equal code "5") "#840084")
1671        ((equal code "6") "#008484")
1672        ((equal code "7") "#555555")
1673        ((equal code "8") "#949494")
1674        ((equal code "9") "#FF0000")
1675        ((equal code "A") "#00C600")
1676        ((equal code "B") "#FFFF00")
1677        ((equal code "C") "#0000FF")
1678        ((equal code "D") "#FF00FF")
1679        ((equal code "E") "#00FFFF")
1680        ((equal code "F") "#FFFFFF")
1681))
1682
1683(defun holpp-decode-full-style (style)
1684   (let* (
1685       (fg (substring style 0 1))
1686       (bg (substring style 1 2))
1687       (b (substring style 2 3))
1688       (u (substring style 3 4))
1689       (fg-face (if (equal fg "-") nil
1690                    (cons :foreground (cons (holpp-decode-color fg) ()))))
1691       (bg-face (if (equal bg "-") nil
1692                    (cons :background (cons (holpp-decode-color bg) ()))))
1693       (b-face  (if (equal b "-") nil
1694                    (cons :weight (cons 'bold ()))))
1695       (u-face  (if (equal u "-") nil
1696                    (cons :underline (cons t ())))))
1697       (cons 'face (cons (append fg-face bg-face b-face u-face) ()))))
1698
1699
1700(defun holpp-find-comment-end (n)
1701   (if (not (re-search-forward "\\((\\*(\\*(\\*\\)\\|\\(\\*)\\*)\\*)\\)" nil t 1))
1702       nil
1703       (if (save-excursion (goto-char (- (point) 6))
1704                           (looking-at "(\\*(\\*(\\*"))
1705           (progn
1706              (holpp-find-comment-end (+ n 1)))
1707           (if (= n 1) t (holpp-find-comment-end (- n 1))))))
1708
1709(defun holpp-execute-code-face-tooltip (start end toolprop codeface)
1710  (let ((tooltipprop
1711         (if (equal toolprop nil) nil (list 'help-echo toolprop))))
1712    (add-text-properties start end (append codeface tooltipprop))))
1713
1714(defun holpp-execute-code (code arg1 start end)
1715  (cond ((equal code "FV")
1716             (holpp-execute-code-face-tooltip start end arg1
1717             '(face hol-free-variable)))
1718        ((equal code "BV")
1719             (holpp-execute-code-face-tooltip start end arg1
1720             '(face hol-bound-variable)))
1721        ((equal code "TV")
1722             (holpp-execute-code-face-tooltip start end arg1
1723             '(face hol-type-variable)))
1724        ((equal code "TY")
1725             (holpp-execute-code-face-tooltip start end arg1
1726             '(face hol-type)))
1727        ((equal code "CO")
1728         (holpp-execute-code-face-tooltip start end arg1 nil))
1729        ((equal code "ST")
1730           (add-text-properties start end
1731             (holpp-decode-full-style arg1)))))
1732
1733(setq temp-hol-output-buf nil)
1734
1735(defun holpp-quiet-reset ()
1736  (let ((tmpbuf (or temp-hol-output-buf
1737                     (generate-new-buffer " *HOL output filter*)"))))
1738      (setq temp-hol-output-buf tmpbuf)
1739      (save-excursion
1740         (set-buffer tmpbuf)
1741         (delete-region (point-min) (point-max)))))
1742
1743(defun holpp-reset ()
1744  (interactive)
1745  (holpp-quiet-reset)
1746  (send-raw-string-to-hol "print \"\\n\\n*** hol-mode reset ***\\n\";" nil nil))
1747
1748; this filter function is complicated by the fact that comint chunks
1749; output (in 1024 character chunks in my tests) and so doesn't
1750; necessarily give complete (in the sense of containing matching
1751; comment-blocks) strings to the filter. This means that a solution
1752; with with-temp-buffer won't work. Instead, there is a persistent
1753; working space buffer, and if the code finds a non-matching comment
1754; start (a "(*(*(*" substring), it just leaves that in the working
1755; space so that the next piece of output can be appended and processed
1756; properly.
1757(defun holpp-output-filter (s)
1758  "Converts a munged emacs_terminal string into a pretty one with text properties."
1759  (interactive "sinput: ")
1760  (let* ((tmpbuf (or temp-hol-output-buf
1761                     (generate-new-buffer " *HOL output filter*)")))
1762         end)
1763    (setq temp-hol-output-buf tmpbuf)
1764    (save-excursion
1765      (set-buffer tmpbuf)
1766      (unwind-protect
1767          (progn
1768            (goto-char (point-max))
1769            (insert s)
1770            (goto-char (point-min))
1771            (while (and (not end) (search-forward "(*(*(*" nil t))
1772              (let ((uptoann (- (point) 6))
1773                    (start (point)))
1774                (if (not (holpp-find-comment-end 1))
1775                    (progn
1776                      (goto-char uptoann)
1777                      (setq end t))
1778                  (delete-region uptoann start)
1779                  (let*
1780                      ((start (- start 6))
1781                       (code (buffer-substring start (+ start 2)))
1782                       (argument
1783                        (save-excursion
1784                          (goto-char (+ start 2))
1785                          (if (equal (following-char) 0)
1786                              (progn
1787                                (goto-char (+ (point) 1))
1788                                (skip-chars-forward "^\^@")
1789                                (prog1
1790                                    (if (equal (+ start 3) (point)) nil
1791                                    (buffer-substring (+ start 3)
1792                                                            (point)))
1793                                  (delete-region (+ start 2) (1+ (point)))))
1794                            nil))))
1795                       (holpp-execute-code code argument
1796                        (+ start 2)
1797                        (- (point) 6))
1798                       (delete-region start (+ start 2))
1799                       (delete-region (- (point) 6) (point))
1800                       (goto-char start)))))
1801            (if (not end)
1802                (progn
1803                  (goto-char (point-max))
1804                  (skip-chars-backward "(*")))
1805            (prog1
1806                (buffer-substring (point-min) (point))
1807              (delete-region (point-min) (point))))))))
1808
1809(defun holmakepp-mark-error (start end)
1810   (add-text-properties start end '(face holmake-error)))
1811
1812
1813(defun holmakepp-mark-mosml-error ()
1814  (interactive)
1815  (goto-char (point-min))
1816  (while (re-search-forward "^!" nil t)
1817     (let* ((start (match-beginning 0)))
1818     (forward-line)
1819     (while (or (looking-at "!") (looking-at " ")) (forward-line))
1820     (holmakepp-mark-error start (- (point) 1))))
1821)
1822
1823(setq temp-holmake-output-buf nil)
1824(defun holmakepp-output-filter (s)
1825  "Converts a munged emacs_terminal string into a pretty one with text properties."
1826  (interactive "sinput: ")
1827  (let* ((tmpbuf (or temp-holmake-output-buf
1828                     (generate-new-buffer " *HOLMAKE output filter*)")))
1829         end)
1830    (setq temp-holmake-output-buf tmpbuf)
1831    (save-excursion
1832      (set-buffer tmpbuf)
1833      (unwind-protect
1834          (progn
1835            (goto-char (point-max))
1836            (insert s)
1837            (holmakepp-mark-mosml-error)
1838            (prog1
1839                (buffer-substring (point-min) (point-max))
1840              (delete-region (point-min) (point-max))))))))
1841
1842(defgroup hol-faces nil "Faces used in pretty-printing HOL values"
1843  :group 'faces
1844  :group 'hol)
1845
1846(defface holmake-error
1847  '((((class color))
1848     :foreground "red"
1849     :weight bold))
1850  "The face for errors shown by HOLMAKE."
1851  :group 'hol-faces)
1852
1853(defface hol-free-variable
1854  '((((class color))
1855     :foreground "blue"
1856     :weight bold))
1857  "The face for presenting free variables in HOL terms."
1858  :group 'hol-faces)
1859
1860(defface hol-bound-variable
1861  '((((class color))
1862     :foreground "#009900"))
1863  "The face for presenting bound variables in HOL terms."
1864  :group 'hol-faces)
1865
1866(defface hol-type-variable
1867  '((((class color))
1868     :foreground "purple"
1869     :slant italic))
1870  "The face for presenting free type variables in HOL terms."
1871  :group 'hol-faces)
1872
1873(defface hol-type
1874  '((((class color))
1875     :foreground "cyan3"
1876     :slant italic))
1877  "The face for presenting HOL types."
1878  :group 'hol-faces)
1879
1880(defun hol-region-to-unicode-pdf (filename beg end)
1881  "Print region to FILE as a PDF, handling Unicode characters."
1882  (interactive "FFile to write to: \nr")
1883  (if (and transient-mark-mode (not mark-active))
1884      (error "No active region"))
1885  (let* ((temp-ps-file (make-temp-file "holprint" nil ".ps"))
1886         (lpr-switches
1887          (list "-font" hol-unicode-print-font-filename
1888                "-out" temp-ps-file))
1889         (lpr-add-switches nil)
1890         (lpr-command "uniprint"))
1891    (lpr-region beg end)
1892    (shell-command (concat "ps2pdf " temp-ps-file " " filename))
1893    (delete-file temp-ps-file)))
1894
1895;;The key combinations
1896(define-key global-map "\M-h" 'hol-map)
1897(define-prefix-command 'holpp-map)
1898(define-key hol-map "\M-p" 'holpp-map)
1899
1900
1901(define-key hol-map "\C-c" 'hol-interrupt)
1902(define-key hol-map "\C-l" 'hol-recentre)
1903(define-key hol-map "\C-q" 'hol-toggle-quietdec)
1904(define-key hol-map "\C-s" 'hol-toggle-simplifier-trace)
1905(define-key hol-map "\C-v" 'hol-scroll-up)
1906(define-key hol-map "\M-f" 'forward-hol-tactic)
1907(define-key hol-map "\M-b" 'backward-hol-tactic)
1908(define-key hol-map "\M-r" 'copy-region-as-hol-definition)
1909(define-key hol-map "\C-r" 'copy-region-as-hol-definition-quietly)
1910(define-key hol-map "\M-q" 'copy-region-as-hol-definition-real-quietly)
1911(define-key hol-map "\M-t" 'hol-toggle-show-times)
1912(define-key hol-map "\M-s" 'hol-subgoal-tactic)
1913(define-key hol-map "\M-v" 'hol-scroll-down)
1914(define-key hol-map "b"    'hol-backup)
1915(define-key hol-map "B"    'hol-user-backup)
1916(define-key hol-map "S"    'hol-user-save-backup)
1917(define-key hol-map "d"    'hol-drop-goal)
1918(define-key hol-map "D"    'hol-drop-all-goals)
1919(define-key hol-map "e"    'copy-region-as-hol-tactic)
1920(define-key hol-map "\M-e" 'hol-find-eval-next-tactic)
1921(define-key hol-map "E"    'copy-region-as-goaltree-tactic)
1922(define-key hol-map "g"    'hol-do-goal)
1923(define-key hol-map "G"    'hol-do-goaltree)
1924(define-key hol-map "h"    'hol)
1925(define-key hol-map "H"    'hol-with-region)
1926(define-key hol-map "\M-m" 'holmake)
1927(define-key hol-map "4"    'hol-display)
1928(define-key hol-map "3"    'hol-horizontal)
1929(define-key hol-map "2"    'hol-vertical)
1930(define-key hol-map "l"    'hol-load-file)
1931(define-key hol-map "m"    'hol-db-match)
1932(define-key hol-map "f"    'hol-db-find)
1933(define-key hol-map "n"    'hol-name-top-theorem)
1934(define-key hol-map "o"    'hol-open-string)
1935(define-key hol-map "p"    'hol-print-goal)
1936(define-key hol-map "P"    'hol-print-all-goals)
1937(define-key hol-map "r"    'hol-rotate)
1938(define-key hol-map "R"    'hol-restart-goal)
1939(define-key hol-map "t"    'mark-hol-tactic)
1940(define-key hol-map "T"    'hol-start-termination-proof)
1941(define-key hol-map "i"    'hol-type-info)
1942(define-key hol-map "s"    'interactive-send-string-to-hol)
1943(define-key hol-map "u"    'hol-use-file)
1944(define-key hol-map "c"    'hol-db-check-current)
1945(define-key hol-map "a"    'hol-remove-unicode)
1946(define-key hol-map "*"    'hol-template-comment-star)
1947(define-key hol-map "-"    'hol-template-comment-minus)
1948(define-key hol-map "="    'hol-template-comment-equal)
1949(define-key hol-map "\M-d" 'hol-template-define)
1950(define-key hol-map "\M-x" 'hol-template-store-thm)
1951
1952
1953(define-key hol-map   "\C-a" 'hol-toggle-show-assums)
1954(define-key holpp-map "a"    'hol-toggle-show-assums)
1955(define-key hol-map   "\C-t" 'hol-toggle-show-types)
1956(define-key holpp-map "\C-t" 'hol-toggle-show-types)
1957(define-key hol-map   "\C-n" 'hol-toggle-show-numeral-types)
1958(define-key holpp-map "n"    'hol-toggle-show-numeral-types)
1959(define-key hol-map   "\C-f" 'hol-toggle-goalstack-fvs)
1960(define-key holpp-map "f"    'hol-toggle-goalstack-fvs)
1961(define-key hol-map   "\C-o" 'hol-toggle-goalstack-print-goal-at-top)
1962(define-key holpp-map "o"    'hol-toggle-goalstack-print-goal-at-top)
1963(define-key hol-map   "\M-a" 'hol-toggle-goalstack-num-assums)
1964(define-key holpp-map "\M-a" 'hol-toggle-goalstack-num-assums)
1965(define-key hol-map   "\C-u" 'hol-toggle-unicode)
1966(define-key holpp-map "u"    'hol-toggle-unicode)
1967(define-key hol-map   "\C-p" 'hol-toggle-ppbackend)
1968(define-key holpp-map "p"    'hol-toggle-ppbackend)
1969(define-key holpp-map "b"    'hol-toggle-emacs-tooltips)
1970(define-key holpp-map "t"    'hol-toggle-pp-annotations)
1971(define-key holpp-map "s"    'hol-toggle-pp-styles)
1972(define-key holpp-map "c"    'hol-toggle-pp-cases)
1973
1974
1975;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
1976;; The definition of the HOL menu
1977;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
1978
1979(define-key-after (lookup-key global-map [menu-bar])
1980  [hol-menu]
1981  (cons "HOL" (make-sparse-keymap "HOL"))
1982  'tools)
1983
1984
1985;; HOL misc
1986(define-key
1987  global-map
1988  [menu-bar hol-menu hol-misc]
1989  (cons "Misc" (make-sparse-keymap "Misc")))
1990
1991(define-key global-map [menu-bar hol-menu hol-misc clean-up]
1992   '("Clean up (remove tab, white spaces at end of line, etc...)" .
1993     hol-cleanup-buffer))
1994
1995(define-key global-map [menu-bar hol-menu hol-misc remove-unicode]
1996   '("Replace common HOL unicode symbols" .
1997     hol-remove-unicode))
1998
1999(define-key global-map [menu-bar hol-menu hol-misc check-names]
2000   '("Check names in store_thm, ..." . hol-check-statement-eq-string))
2001
2002(define-key global-map [menu-bar hol-menu hol-misc sep4]
2003   '(menu-item "--"))
2004
2005(define-key global-map [menu-bar hol-menu hol-misc check-theory-current]
2006   '("Sanity check current theory" . hol-db-check-current))
2007
2008(define-key global-map [menu-bar hol-menu hol-misc check-theory]
2009   '("Sanity check theory" . hol-db-check))
2010
2011(define-key global-map [menu-bar hol-menu hol-misc sep3]
2012   '(menu-item "--"))
2013
2014(define-key global-map [menu-bar hol-menu hol-misc mark-tactic]
2015   '("Mark tactic" . mark-hol-tactic))
2016
2017(define-key global-map [menu-bar hol-menu hol-misc backward-tactic]
2018   '("Move to previous tactic" . backward-hol-tactic))
2019
2020(define-key global-map [menu-bar hol-menu hol-misc forward-tactic]
2021   '("Move to next tactic" . forward-hol-tactic))
2022
2023(define-key global-map [menu-bar hol-menu hol-misc sep2]
2024   '(menu-item "--"))
2025
2026(define-key global-map [menu-bar hol-menu hol-misc open-string]
2027   '("Load and open" . hol-open-string))
2028
2029(define-key global-map [menu-bar hol-menu hol-misc use-file]
2030   '("Use file" . hol-use-file))
2031
2032(define-key global-map [menu-bar hol-menu hol-misc load-file]
2033   '("Load file" . hol-load-file))
2034
2035(define-key global-map [menu-bar hol-menu hol-misc auto-load]
2036   '(menu-item "Automatic loading" hol-toggle-auto-load
2037                     :button (:toggle
2038                              . (and (boundp 'hol-auto-load-p)
2039                                     hol-auto-load-p))))
2040
2041(define-key global-map [menu-bar hol-menu hol-misc show-load-paths]
2042   '("Show load-paths" . hol-show-current-load-paths))
2043
2044(define-key global-map [menu-bar hol-menu hol-misc add-load-path]
2045   '("Add load-path ..." . hol-add-load-path))
2046
2047(define-key global-map [menu-bar hol-menu hol-misc sep1]
2048   '(menu-item "--"))
2049
2050(define-key global-map [menu-bar hol-menu hol-misc hol-type-info]
2051   '("Type info of marked term" . hol-type-info))
2052
2053(define-key global-map [menu-bar hol-menu hol-misc sep0]
2054   '(menu-item "--"))
2055
2056(define-key global-map [menu-bar hol-menu hol-misc db-find]
2057   '("DB find" . hol-db-find))
2058
2059(define-key global-map [menu-bar hol-menu hol-misc db-match]
2060   '("DB match" . hol-db-match))
2061
2062
2063
2064;; templates
2065(define-key
2066  global-map
2067  [menu-bar hol-menu hol-template]
2068  (cons "Templates" (make-sparse-keymap "Templates")))
2069
2070(define-key global-map [menu-bar hol-menu hol-template new-script]
2071   '("New theory" . hol-template-new-script-file))
2072
2073(define-key global-map [menu-bar hol-menu hol-template new-datatype]
2074   '("New datatype" . hol-template-new-datatype))
2075
2076(define-key global-map [menu-bar hol-menu hol-template define]
2077   '("New definition" . hol-template-define))
2078
2079(define-key global-map [menu-bar hol-menu hol-template store-thm]
2080   '("Store theorem" . hol-template-store-thm))
2081
2082(define-key global-map [menu-bar hol-menu hol-template sep1]
2083   '(menu-item "--"))
2084
2085(define-key global-map [menu-bar hol-menu hol-template comment-star]
2086   '("Comment *" . hol-template-comment-star))
2087
2088(define-key global-map [menu-bar hol-menu hol-template comment-equal]
2089   '("Comment =" . hol-template-comment-equal))
2090
2091(define-key global-map [menu-bar hol-menu hol-template comment-minus]
2092   '("Comment -" . hol-template-comment-minus))
2093
2094
2095;; printing
2096(define-key
2097  global-map
2098  [menu-bar hol-menu hol-printing]
2099  (cons "Printing switches" (make-sparse-keymap "Printing switches")))
2100
2101(define-key global-map [menu-bar hol-menu hol-printing simplifier-trace]
2102   '("Simplifier trace" . hol-toggle-simplifier-trace))
2103
2104(define-key global-map [menu-bar hol-menu hol-printing times]
2105   '("Show times" . hol-toggle-show-times))
2106
2107(define-key global-map [menu-bar hol-menu hol-printing echo]
2108   '("Echo commands" . hol-toggle-echo-commands))
2109
2110(define-key global-map [menu-bar hol-menu hol-printing quiet]
2111   '("Quiet (hide output except errors)" . hol-toggle-quietdec))
2112
2113(define-key
2114  global-map
2115  [menu-bar hol-menu hol-printing backends]
2116  (cons "Pretty-printing backends" (make-sparse-keymap "Pretty-printing backends")))
2117
2118(define-key global-map [menu-bar hol-menu hol-printing backends ppreset]
2119  '("Reset hol-mode pretty-printing (error recovery)" . holpp-reset))
2120
2121(define-key global-map [menu-bar hol-menu hol-printing backends sep1]
2122   '(menu-item "--"))
2123
2124(define-key global-map [menu-bar hol-menu hol-printing backends ppstyles]
2125  '("Toggle use styles" . hol-toggle-pp-styles))
2126
2127(define-key global-map [menu-bar hol-menu hol-printing backends ppannotations]
2128  '("Toggle use annotations" . hol-toggle-pp-annotations))
2129
2130(define-key global-map [menu-bar hol-menu hol-printing backends pptooltip]
2131  '("Toggle show tooltips" . hol-toggle-emacs-tooltips))
2132
2133(define-key global-map [menu-bar hol-menu hol-printing backends sep2]
2134   '(menu-item "--"))
2135
2136(define-key global-map [menu-bar hol-menu hol-printing backends ppbackend]
2137  '("Toggle pretty-printing backend" . hol-toggle-ppbackend))
2138
2139(define-key global-map [menu-bar hol-menu hol-printing unicode]
2140   '("Unicode" . hol-toggle-unicode))
2141
2142(define-key global-map [menu-bar hol-menu hol-printing ppcases]
2143  '("Toggle pretty-printing of cases" . hol-toggle-pp-cases))
2144
2145(define-key global-map [menu-bar hol-menu hol-printing sep2]
2146   '(menu-item "--"))
2147
2148
2149(define-key global-map [menu-bar hol-menu hol-printing num-subgoals]
2150   '("Set no. of shown subgoals" . hol-toggle-goalstack-num-subgoals))
2151
2152(define-key global-map [menu-bar hol-menu hol-printing num-assums]
2153   '("Set no. of shown assumptions" . hol-toggle-goalstack-num-assums))
2154
2155(define-key global-map [menu-bar hol-menu hol-printing print-goal-at-top]
2156   '("Print goal at top" . hol-toggle-goalstack-print-goal-at-top))
2157
2158(define-key global-map [menu-bar hol-menu hol-printing goal-fvs]
2159   '("Show free vars in goal" . hol-toggle-goalstack-fvs))
2160
2161(define-key global-map [menu-bar hol-menu hol-printing sep1]
2162   '(menu-item "--"))
2163
2164
2165(define-key global-map [menu-bar hol-menu hol-printing show-assums]
2166   '("Show assumptions" . hol-toggle-show-assums))
2167
2168(define-key global-map [menu-bar hol-menu hol-printing show-tags]
2169   '("Show tags" . hol-toggle-show-tags))
2170
2171(define-key global-map [menu-bar hol-menu hol-printing show-axioms]
2172   '("Show axioms" . hol-toggle-show-axioms))
2173
2174(define-key global-map [menu-bar hol-menu hol-printing show-num-types]
2175   '("Show numeral types" . hol-toggle-show-numeral-types))
2176
2177(define-key global-map [menu-bar hol-menu hol-printing show-types-verbosely]
2178   '("Show types verbosely" . hol-toggle-show-types-verbosely))
2179
2180(define-key global-map [menu-bar hol-menu hol-printing show-types]
2181   '("Show types" . hol-toggle-show-types))
2182
2183
2184
2185
2186
2187;; HOL goals
2188(define-key
2189  global-map
2190  [menu-bar hol-menu hol-goalstack]
2191  (cons "Goalstack" (make-sparse-keymap "Goalstack")))
2192
2193
2194(define-key global-map [menu-bar hol-menu hol-goalstack apply-tactic-goaltree]
2195   '("Apply tactic (goaltree)" . copy-region-as-goaltree-tactic))
2196
2197(define-key global-map [menu-bar hol-menu hol-goalstack new-goaltree]
2198   '("New goaltree" . hol-do-goaltree))
2199
2200(define-key global-map [menu-bar hol-menu hol-goalstack sep3]
2201   '(menu-item "--"))
2202
2203(define-key global-map [menu-bar hol-menu hol-goalstack restart-goal]
2204   '("Restart goal" . hol-restart-goal))
2205
2206(define-key global-map [menu-bar hol-menu hol-goalstack drop-all]
2207   '("Drop all goals" . hol-drop-all-goals))
2208
2209(define-key global-map [menu-bar hol-menu hol-goalstack drop-goal]
2210   '("Drop goal" . hol-drop-goal))
2211
2212(define-key global-map [menu-bar hol-menu hol-goalstack sep1]
2213   '(menu-item "--"))
2214
2215(define-key global-map [menu-bar hol-menu hol-goalstack print-all]
2216   '("Print all goals" . hol-print-all-goals))
2217
2218(define-key global-map [menu-bar hol-menu hol-goalstack print-top]
2219   '("Print goal" . hol-print-goal))
2220
2221(define-key global-map [menu-bar hol-menu hol-goalstack sep0]
2222   '(menu-item "--"))
2223
2224(define-key global-map [menu-bar hol-menu hol-goalstack top-thm]
2225   '("Name top theorem" . hol-name-top-theorem))
2226
2227(define-key global-map [menu-bar hol-menu hol-goalstack subgoal-tac]
2228   '("Subgoal tactic" . hol-subgoal-tactic))
2229
2230(define-key global-map [menu-bar hol-menu hol-goalstack rotate]
2231   '("Rotate" . hol-rotate))
2232
2233(define-key global-map [menu-bar hol-menu hol-goalstack back-up-user]
2234   '("Restore" . hol-user-backup))
2235
2236(define-key global-map [menu-bar hol-menu hol-goalstack back-up-save-user]
2237   '("Save" . hol-user-save-backup))
2238
2239(define-key global-map [menu-bar hol-menu hol-goalstack back-up]
2240   '("Back up" . hol-backup))
2241
2242(define-key global-map [menu-bar hol-menu hol-goalstack apply-tactic]
2243   '("Apply tactic" . copy-region-as-hol-tactic))
2244
2245(define-key global-map [menu-bar hol-menu hol-goalstack new-termination-goal]
2246  '("New termination goal" . hol-start-termination-proof))
2247
2248(define-key global-map [menu-bar hol-menu hol-goalstack new-goal]
2249   '("New goal" . hol-do-goal))
2250
2251
2252
2253;;process
2254(define-key
2255  global-map
2256  [menu-bar hol-menu hol-process]
2257  (cons "Process" (make-sparse-keymap "Process")))
2258
2259(define-key global-map [menu-bar hol-menu hol-process hol-scroll-down]
2260   '("Scroll down" . hol-scroll-down))
2261
2262(define-key global-map [menu-bar hol-menu hol-process hol-scroll-up]
2263   '("Scroll up" . hol-scroll-up))
2264
2265(define-key global-map [menu-bar hol-menu hol-process hol-recentre]
2266   '("Recentre" . hol-recentre))
2267
2268(define-key global-map [menu-bar hol-menu hol-process sep2]
2269   '(menu-item "--"))
2270
2271(define-key global-map [menu-bar hol-menu hol-process hol-send-string]
2272   '("Send string to HOL" . interactive-send-string-to-hol))
2273
2274(define-key global-map [menu-bar hol-menu hol-process hol-send-region-quietly]
2275   '("Send region to HOL - hide non-errors" . copy-region-as-hol-definition-quietly))
2276
2277(define-key global-map [menu-bar hol-menu hol-process hol-send-region]
2278   '("Send region to HOL" . copy-region-as-hol-definition))
2279
2280(define-key global-map [menu-bar hol-menu hol-process sep1]
2281   '(menu-item "--"))
2282
2283(define-key global-map [menu-bar hol-menu hol-process toggle-hol-bare]
2284   '(menu-item "Use bare" hol-toggle-bare
2285                     :button (:toggle
2286                              . (and (boundp 'hol-bare-p)
2287                                     hol-bare-p))))
2288
2289(define-key global-map [menu-bar hol-menu hol-process hol-show-info]
2290   '("Show HOL information" . hol-print-info))
2291
2292(define-key global-map [menu-bar hol-menu hol-process hol-exe]
2293   '("Set HOL executable" . hol-set-executable))
2294
2295(define-key global-map [menu-bar hol-menu hol-process hol-kill]
2296   '("Kill HOL" . hol-kill))
2297
2298(define-key global-map [menu-bar hol-menu hol-process hol-interrupt]
2299   '("Interrupt HOL" . hol-interrupt))
2300
2301(define-key global-map [menu-bar hol-menu hol-process sep02]
2302   '(menu-item "--"))
2303
2304(define-key global-map [menu-bar hol-menu hol-process holmake]
2305   '("Run Holmake" . holmake))
2306
2307(define-key global-map [menu-bar hol-menu hol-process sep01]
2308   '(menu-item "--"))
2309
2310(define-key global-map [menu-bar hol-menu hol-process hol-display]
2311   '("Display HOL buffer" . hol-display))
2312
2313(define-key global-map [menu-bar hol-menu hol-process hol-start-vertical]
2314   '("Start HOL - vertical split" . hol-vertical))
2315
2316(define-key global-map [menu-bar hol-menu hol-process hol-start-horizontal]
2317   '("Start HOL - horizontal split" . hol-horizontal))
2318
2319(define-key global-map [menu-bar hol-menu hol-process hol-start]
2320  '("Start HOL" . hol))
2321
2322;; Support for snippet expansion, if yasnippet is installed.
2323(when (require 'yasnippet nil 'noerror)
2324  (let ((HOLsnippets
2325         (concat
2326          (string-remove-suffix "/bin/hol" hol-executable)
2327          "/tools/yasnippets" "")))
2328    (setq yas-snippet-dirs (nconc yas-snippet-dirs (cons HOLsnippets '())))
2329    (yas-reload-all)
2330    (define-key hol-map (kbd "TAB") 'yas-expand)))
2331
2332(when (locate-library "company-yasnippet")
2333  (load-library "company")
2334  (setq company-backends (cons 'company-yasnippet company-backends)))
2335