1(provide 'holscript-mode) 2 3;; font-locking and syntax 4 5 6(defconst holscript-font-lock-keywords 7 (list '("^\\(Theorem\\|Triviality\\)[[:space:]]+\\([A-Za-z0-9'_]+\\)[[ :]" 8 (1 'holscript-theorem-syntax) (2 'holscript-thmname-syntax)) 9 '("^\\(Proof\\|^QED\\)\\>" . 'holscript-theorem-syntax) 10 '("^\\(Definition\\|\\(?:Co\\)?Inductive\\)[[:space:]]+\\([A-Za-z0-9'_]+\\)[[ :]" 11 (1 'holscript-definition-syntax) (2 'holscript-thmname-syntax)) 12 '("^Termination\\>\\|^End\\>" . 'holscript-definition-syntax) 13 '("^\\(Datatype\\)[[:space:]]*:" (1 'holscript-definition-syntax)) 14 '("^THEN[1L]?\\>" . 'holscript-then-syntax) 15 '("[^A-Za-z0-9_']\\(THEN[1L]?\\)\\>" 1 'holscript-then-syntax) 16 '("\\S.\\(>[->|]\\|\\\\\\\\\\)\\S." 1 'holscript-then-syntax) 17 "^Type\\>" 18 "^Overload\\>" 19 (list (regexp-opt 20 '("let" "local" "in" "end" "fun" "val" "open") 21 'symbols) 22 'quote 23 'holscript-smlsyntax) 24 '("\\<cheat\\>" . 'holscript-cheat-face) 25 '(holscript-find-syntax-error 0 'holscript-syntax-error-face prepend) 26 '(hol-find-quoted-material 0 'holscript-quoted-material prepend) 27 '("^\\[[[:space:]]*~?\\([A-Za-z0-9'_]+\\)\\(\\[[A-Za-z0-9'_,]+\\]\\)?[[:space:]]*:\\]" 0 28 'holscript-definition-label-face prepend))) 29 30(defconst holscript-font-lock-defaults '(holscript-font-lock-keywords)) 31 32(defvar holscript-mode-syntax-table 33 (let ((st (make-syntax-table))) 34 (modify-syntax-entry ?\* ". 23n" st) 35 (modify-syntax-entry ?\( "()1" st) 36 (modify-syntax-entry ?\) ")(4" st) 37 (modify-syntax-entry ?��� "(���" st) 38 (modify-syntax-entry ?��� ")���" st) 39 (modify-syntax-entry ?��� "(���" st) 40 (modify-syntax-entry ?��� ")���" st) 41 (modify-syntax-entry ?\\ "\\" st) 42 ;; backslash only escapes in strings but we need to have it seen 43 ;; as one in general if the hol-mode isn't to get seriously 44 ;; confused by script files that contain escaped quotation 45 ;; characters. This despite the fact that it does cause pain in 46 ;; terms such as \(x,y). x + y 47 (mapc (lambda (c) (modify-syntax-entry c "w" st)) "'") 48 (mapc (lambda (c) (modify-syntax-entry c "_" st)) "$_") 49 (mapc (lambda (c) (modify-syntax-entry c "." st)) ".%&+-/:<=>?@`^|!~#,;") 50 st) 51 "The syntax table used in `holscript-mode'.") 52 53;; key maps 54 55(defvar holscript-mode-map 56 (let ((map (make-sparse-keymap))) 57 (define-key map (kbd "`") 'holscript-dbl-backquote) 58 (define-key map (kbd "<RET>") 'holscript-newline-and-relative-indent) 59 ;;(define-key map "\M-f" 'forward-hol-tactic) 60 ;;(define-key map "\M-b" 'backward-hol-tactic) 61 ; (define-key map (kbd "C-M-<up>") 'hol-movement-backward-up-list) 62 ; (define-key map (kbd "C-M-<left>") 'hol-movement-backward-sexp) 63 map 64 ) 65 "Keymap used in `holscript-mode'.") 66 67;;; nicer editing with quotation symbols 68(defun holscript-to-left-quote () 69 "Move left in the buffer to the previous ��� or ��� character." 70 (interactive) 71 (re-search-backward "���\\|���")) 72 73(defun holscript-to-right-quote () 74 "Move right in the buffer to just beyond the next ��� or ��� character." 75 (interactive) 76 (re-search-forward "���\\|���")) 77 78(defun holscript-dbl-backquote () 79 "Perform 'smart' insertion of Unicode quotes. 80 81On existing quotes, toggles between ���-��� and ���-��� pairs. Otherwise, inserts a 82���-��� pair, leaving the cursor on the right quote, ready to insert text." 83 (interactive) 84 (cond 85 ((use-region-p) 86 (let ((beg (region-beginning)) 87 (end (region-end))) 88 (goto-char end) 89 (insert "���") 90 (goto-char beg) 91 (insert "���") 92 (backward-char 1))) 93 ((looking-at "���") 94 (if (= (char-before) #x2018) ; U+2018 = ��� 95 (progn 96 (backward-char 1) 97 (delete-char 2) 98 (insert "������") 99 (backward-char 1)) 100 (forward-char 1))) 101 ((looking-at "���") 102 (if (= (char-before) #x201C) ; U+201C = ��� 103 (progn 104 (backward-char 1) 105 (delete-char 2) 106 (insert "������") 107 (backward-char 1)) 108 (forward-char 1))) 109 ((looking-at "���") 110 (if (catch 'exit 111 (save-mark-and-excursion 112 (forward-char 1) 113 (if (re-search-forward "���\\|���" nil t) 114 (goto-char (match-beginning 0))) 115 (if (looking-at "���") 116 (progn (delete-char 1) (insert "���") (throw 'exit t)) 117 (throw 'exit nil)))) 118 (progn (delete-char 1) (insert "���") (backward-char 1)))) 119 ((looking-at "���") 120 (if (catch 'exit 121 (save-mark-and-excursion 122 (forward-char 1) 123 (if (re-search-forward "���\\|���" nil t) 124 (goto-char (match-beginning 0))) 125 (if (looking-at "���") 126 (progn (delete-char 1) (insert "���") (throw 'exit t)) 127 (throw 'exit nil)))) 128 (progn (delete-char 1) (insert "���") (backward-char 1)))) 129 (t (insert "������") (backward-char 1)))) 130 131(defun forward-smlsymbol (n) 132 (interactive "p") 133 (cond ((> n 0) 134 (while (> n 0) 135 (skip-syntax-forward "^.") 136 (skip-syntax-forward ".") 137 (setq n (- n 1)))) 138 ((< n 0) 139 (setq n (- n)) 140 (setq n (- n (if (equal (skip-syntax-backward ".") 0) 0 1)))) 141 (while (> n 0) 142 (skip-syntax-backward "^.") 143 (skip-syntax-backward ".") 144 (setq n (- n 1))))) 145 146(defun is-a-then (s) 147 (and s (or (string-equal s "THEN") 148 (string-equal s "THENL") 149 (string-equal s "QED") 150 (string-equal s "val") 151 (string-equal s ">-") 152 (string-equal s ">>") 153 (string-equal s ">|") 154 (string-equal s "\\\\")))) 155 156(defun next-hol-lexeme-terminates-tactic () 157 (forward-comment (point-max)) 158 (or (eobp) 159 (char-equal (following-char) ?,) 160 (char-equal (following-char) ?\)) 161 ;; (char-equal (following-char) ?=) 162 (char-equal (following-char) ?\;) 163 (is-a-then (word-at-point)) 164 (is-a-then (thing-at-point 'smlsymbol t)))) 165 166(defun previous-hol-lexeme-terminates-tactic () 167 (save-excursion 168 (forward-comment (- (point))) 169 (or (bobp) 170 (char-equal (preceding-char) ?,) 171 (char-equal (preceding-char) ?=) 172 (char-equal (preceding-char) ?\;) 173 (char-equal (preceding-char) ?\)) 174 (and (condition-case nil 175 (progn (backward-char 1) t) 176 (error nil)) 177 (or (is-a-then (word-at-point)) 178 (is-a-then (thing-at-point 'smlsymbol t))))))) 179 180(defun looking-at-tactic-terminator () 181 "Returns a cons-pair (x . y), with x the distance to end, and y the 182 size of the terminator, or nil if there isn't one there. The x value may 183 be zero, if point is immediately after the terminator." 184 (interactive) 185 (let ((c (following-char)) 186 (pc (preceding-char))) 187 (cond ((char-equal c ?,) '(1 . 1)) 188 ((char-equal pc ?,) '(0 . 1)) 189 ((char-equal c ?\)) '(1 . 1)) 190 ((char-equal pc ?\)) '(0 . 1)) 191 ((char-equal c ?\]) '(1 . 1)) 192 ((char-equal pc ?\]) '(0 . 1)) 193 ((char-equal c ?\;) '(1 . 1)) 194 ((char-equal pc ?\;) '(0 . 1)) 195 ((let ((w (word-at-point))) 196 (if (is-a-then w) 197 (cons 198 (- (cdr (bounds-of-thing-at-point 'word)) (point)) 199 (length w)) 200 (let ((w (thing-at-point 'smlsymbol t))) 201 (if (is-a-then w) 202 (cons 203 (- (cdr (bounds-of-thing-at-point 'smlsymbol)) (point)) 204 (length w)) 205 nil)))))))) 206 207(defun looking-at-tactic-starter () 208 "Returns a cons-pair (x . y), with x the distance to end, and y the 209 size of the terminator, or nil if there isn't one there. The x value may 210 be zero, if point is immediately after the terminator." 211 (interactive) 212 (let ((c (following-char)) 213 (pc (preceding-char))) 214 (cond ((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 ((char-equal c ?\;) '(1 . 1)) 221 ((char-equal pc ?\;) '(0 . 1)) 222 ((let ((w (word-at-point))) 223 (if (is-a-then w) 224 (cons 225 (- (cdr (bounds-of-thing-at-point 'word)) (point)) 226 (length w)) 227 (let ((w (thing-at-point 'smlsymbol t))) 228 (if (is-a-then w) 229 (cons 230 (- (cdr (bounds-of-thing-at-point 'smlsymbol)) (point)) 231 (length w)) 232 nil)))))))) 233 234 235(defun forward-tactic-terminator (n) 236 (interactive "^p") 237 (cond ((> n 0) 238 (let (c) 239 (while (> n 0) 240 (skip-syntax-forward " ") 241 (setq c (looking-at-tactic-terminator)) 242 (while (or (not c) (equal (car c) 0)) 243 (forward-sexp) 244 (skip-syntax-forward " ") 245 (setq c (looking-at-tactic-terminator))) 246 (forward-char (car c)) 247 (setq n (- n 1))))) 248 ((< n 0) 249 (setq n (- n)) 250 (let (c) 251 (while (> n 0) 252 (skip-syntax-backward " ") 253 (setq c (looking-at-tactic-terminator)) 254 (while (or (not c) (equal (car c) (cdr c))) 255 (condition-case nil 256 (backward-sexp) 257 (error (backward-char))) 258 (skip-syntax-backward " ") 259 (setq c (looking-at-tactic-terminator))) 260 (backward-char (- (cdr c) (car c))) 261 (setq n (- n 1))))))) 262 263(defun forward-tactic-starter (n) 264 (interactive "^p") 265 (cond ((> n 0) 266 (let (c) 267 (while (> n 0) 268 (skip-syntax-forward " ") 269 (setq c (looking-at-tactic-starter)) 270 (while (or (not c) (equal (car c) 0)) 271 (forward-sexp) 272 (skip-syntax-forward " ") 273 (setq c (looking-at-tactic-starter))) 274 (forward-char (car c)) 275 (setq n (- n 1))))) 276 ((< n 0) 277 (setq n (- n)) 278 (let (c) 279 (while (> n 0) 280 (skip-syntax-backward " ") 281 (setq c (looking-at-tactic-starter)) 282 (while (or (not c) (equal (car c) (cdr c))) 283 (condition-case nil 284 (backward-sexp) 285 (error (backward-char))) 286 (skip-syntax-backward " ") 287 (setq c (looking-at-tactic-starter))) 288 (backward-char (- (cdr c) (car c))) 289 (setq n (- n 1))))))) 290 291(defun preceded-by-starter () 292 (save-excursion 293 (backward-char) 294 (thing-at-point 'tactic-starter))) 295(defun forward-hol-tactic (n) 296 (interactive "^p") 297 (cond ((> n 0) 298 (while (> n 0) 299 (forward-comment (point-max)) 300 (while (thing-at-point 'tactic-terminator) 301 (forward-tactic-terminator 1) 302 (skip-syntax-forward " ")) 303 (while (not (thing-at-point 'tactic-terminator)) 304 (forward-sexp 1) 305 (skip-syntax-forward " ")) 306 (skip-syntax-backward " ") 307 (setq n (- n 1)))) 308 ((< n 0) 309 (setq n (- n)) 310 (while (> n 0) 311 (forward-comment (- (point))) 312 (while (preceded-by-starter) 313 (forward-tactic-starter -1) 314 (skip-syntax-backward " ")) 315 (while (not (preceded-by-starter)) 316 (forward-sexp -1) 317 (skip-syntax-backward " ")) 318 (skip-syntax-forward " ") 319 (setq n (- n 1)))))) 320 321(defconst holscript-symbolicthen-regexp "\\(?:>>\\|\\\\\\\\\\|>-\\|>|\\)") 322(defconst holscript-textthen-regexp "\\(?:\\<\\(THEN\\([1L]?\\)\\)\\>\\)") 323(defconst holscript-thenish-regexp 324 (concat "\\(?:" holscript-symbolicthen-regexp "\\|" 325 holscript-textthen-regexp "\\)")) 326(defconst holscript-doublethen-error-regexp 327 (concat holscript-thenish-regexp "[[:space:]]+" holscript-thenish-regexp)) 328(defun holscript-syntax-convert (n) (if (and n (equal (car n) 9)) '(1) n)) 329(defun holscript-bad-error-delims (p1 p2) 330 (let ((s0 (holscript-syntax-convert (syntax-after (1- p1)))) 331 (s1 (holscript-syntax-convert (syntax-after p1))) 332 (s2 (holscript-syntax-convert (syntax-after (1- p2)))) 333 (s3 (holscript-syntax-convert (syntax-after p2)))) 334 (or (equal s0 s1) (equal s2 s3)))) 335 336(defconst holscript-quoteddeclaration-begin 337 (concat 338 "^\\(Theorem\\|Triviality\\|Definition\\|Inductive\\|CoInductive\\)" 339 "[[:space:]]+\\([A-Za-z0-9'_]+\\)[[:space:]]*" ; name 340 "\\(\\[[A-Za-z0-9'_,]+\\]\\)?[[:space:]]*:"; optional annotations 341 ) 342 "Regular expression marking the beginning of the special syntax that marks 343a store_thm equivalent.") 344 345(defconst holscript-quoteddeclaration-end 346 (regexp-opt (list "End" "Proof" "Termination"))) 347 348(defconst holscript-quotedmaterial-delimiter-fullregexp 349 (concat holscript-quoteddeclaration-begin "\\|" 350 holscript-quoteddeclaration-end "\\|[������������]")) 351 352(defun holscript-in-quotedmaterialp (p) 353 (save-match-data 354 (save-mark-and-excursion 355 (goto-char p) 356 (let ((beginmatch 357 (re-search-backward 358 holscript-quotedmaterial-delimiter-fullregexp nil t)) 359 (ppss (syntax-ppss))) 360 (while (and beginmatch (or (nth 3 ppss) (nth 4 ppss))) 361 (setq beginmatch (re-search-backward 362 holscript-quotedmaterial-delimiter-fullregexp nil t)) 363 (setq ppss (syntax-ppss))) 364 (and beginmatch 365 (or (looking-at holscript-quoteddeclaration-begin) 366 (looking-at "[������]"))))))) 367 368(defun holscript-find-syntax-error (limit) 369 (let ((beginmatch 370 (re-search-forward holscript-doublethen-error-regexp limit t)) 371 (ppss (syntax-ppss))) 372 (while (and beginmatch 373 (or (nth 3 ppss) (nth 4 ppss) 374 (holscript-bad-error-delims (match-beginning 0) 375 (match-end 0)) 376 (holscript-in-quotedmaterialp (point)))) 377 (setq beginmatch 378 (re-search-forward holscript-doublethen-error-regexp limit t)) 379 (setq ppss (syntax-ppss))) 380 (if (not beginmatch) nil t))) 381 382;;templates 383(defun hol-extract-script-name (arg) 384 "Return the name of the theory associated with the given filename" 385(let* ( 386 (pos (string-match "[^/]*Script\.sml" arg))) 387 (cond (pos (substring arg pos -10)) 388 (t "<insert theory name here>")))) 389 390(defun hol-template-new-script-file () 391 "Inserts standard template for a HOL theory" 392 (interactive) 393 (insert "open HolKernel Parse boolLib bossLib;\n\nval _ = new_theory \"") 394 (insert (hol-extract-script-name buffer-file-name)) 395 (insert "\";\n\n\n\n\nval _ = export_theory();\n\n")) 396 397(defun hol-template-comment-star () 398 (interactive) 399 (insert "\n\n") 400 (insert "(******************************************************************************)\n") 401 (insert "(* *)\n") 402 (insert "(* *)\n") 403 (insert "(* *)\n") 404 (insert "(******************************************************************************)\n")) 405 406(defun hol-template-comment-minus () 407 (interactive) 408 (insert "\n\n") 409 (insert "(* -------------------------------------------------------------------------- *)\n") 410 (insert "(* *)\n") 411 (insert "(* *)\n") 412 (insert "(* *)\n") 413 (insert "(* -------------------------------------------------------------------------- *)\n")) 414 415(defun hol-template-comment-equal () 416 (interactive) 417 (insert "\n\n") 418 (insert "(* ========================================================================== *)\n") 419 (insert "(* *)\n") 420 (insert "(* *)\n") 421 (insert "(* *)\n") 422 (insert "(* ========================================================================== *)\n")) 423 424(defun hol-template-define (name) 425 (interactive "sNew name: ") 426 (insert "val ") 427 (insert name) 428 (insert "_def = Define `") 429 (insert name) 430 (insert " = `;\n")) 431 432(defun hol-template-store-thm (name) 433 (interactive "sTheorem name: ") 434 (insert "\nTheorem ") 435 (insert name) 436 (insert ":\n\nProof\nQED\n")) 437 438(defun hol-template-hol-relnish (style name) 439 (insert (format "\n%s %s:\n ...\nEnd\n" style name))) 440 441(defun hol-template-hol-reln (name) 442 (interactive "sConstant name: ") 443 (hol-template-hol-relnish "Inductive" name)) 444 445(defun hol-template-hol-coreln (name) 446 (interactive "sConstant name: ") 447 (hol-template-hol-relnish "CoInductive" name)) 448 449(defun hol-template-new-datatype () 450 (interactive) 451 (insert "val _ = Datatype `TREE = LEAF ('a -> num) | BRANCH TREE TREE`;\n")) 452 453;;checking for trouble with names in store_thm, save_thm, Define 454(setq store-thm-regexp 455 "val[ \t\n]*\\([^ \t\n]*\\)[ \t\n]*=[ \t\n]*store_thm[ \t\n]*([ \t\n]*\"\\([^\"]*\\)\"") 456(setq save-thm-regexp 457 "val[ \t\n]*\\([^ \t\n]*\\)[ \t\n]*=[ \t\n]*save_thm[ \t\n]*([ \t\n]*\"\\([^\"]*\\)\"") 458(setq define-thm-regexp 459 "val[ \t\n]*\\([^ \t\n]*\\)_def[ \t\n]*=[ \t\n]*Define[ \t\n]*`[ \t\n(]*\$?\\([^ \t\n([!?:]*\\)") 460 461(setq statement-eq-regexp-list (list store-thm-regexp save-thm-regexp define-thm-regexp)) 462 463(defun hol-correct-eqstring (s1 p1 s2 p2) 464 (interactive) 465 (let (choice) 466 (setq choice 0) 467 (while (eq choice 0) 468 (message 469 (concat 470 "Different names used. Please choose one:\n(0) " 471 s1 "\n(1) " s2 "\n(i) ignore")) 472 (setq choice (if (fboundp 'read-char-exclusive) 473 (read-char-exclusive) 474 (read-char))) 475 (cond ((= choice ?0) t) 476 ((= choice ?1) t) 477 ((= choice ?i) t) 478 (t (progn (setq choice 0) (ding)))) 479 ) 480 (if (= choice ?i) t 481 (let (so sr pr) 482 (cond ((= choice ?0) (setq so s1 sr s2 pr p2)) 483 (t (setq so s2 sr s1 pr p1))) 484 (delete-region pr (+ pr (length sr))) 485 (goto-char pr) 486 (insert so) 487 )))) 488 489 490(defun hol-check-statement-eq-string () 491 (interactive) 492 (save-excursion 493 (dolist (current-regexp statement-eq-regexp-list t) 494 (goto-char 0) 495 (let (no-error-found s1 p1 s2 p2) 496 (while (re-search-forward current-regexp nil t) 497 (progn (setq s1 (match-string-no-properties 1)) 498 (setq s2 (match-string-no-properties 2)) 499 (setq p1 (match-beginning 1)) 500 (setq p2 (match-beginning 2)) 501 (setq no-error-found (string= s1 s2)) 502 (if no-error-found t (hol-correct-eqstring s1 p1 s2 p2))))) 503 (message "checking for problematic names done")))) 504 505;; make newline do a newline and relative indent 506(defun holscript-newline-and-relative-indent () 507 "Insert a newline, then perform a `relative indent'." 508 (interactive "*") 509 (delete-horizontal-space t) 510 (let ((doindent (save-excursion (forward-line 0) 511 (equal (char-syntax (following-char)) ?\s)))) 512 (newline nil t) 513 (if doindent (indent-relative)))) 514 515;;indentation and other cleanups 516(defun hol-replace-tabs-with-spaces () 517 (save-excursion 518 (goto-char (point-min)) 519 (while (search-forward "\t" nil t) 520 (delete-region (- (point) 1) (point)) 521 (let* ((count (- tab-width (mod (current-column) tab-width)))) 522 (dotimes (i count) (insert " ")))))) 523 524(defun hol-remove-tailing-whitespaces () 525 (save-excursion 526 (goto-char (point-min)) 527 (while (re-search-forward " +$" nil t) 528 (delete-region (match-beginning 0) (match-end 0))))) 529 530 531(defun hol-remove-tailing-empty-lines () 532 (save-excursion 533 (goto-char (point-max)) 534 (while (bolp) (delete-char -1)) 535 (insert "\n"))) 536 537(defun hol-cleanup-buffer () 538 (interactive) 539 (hol-replace-tabs-with-spaces) 540 (hol-remove-tailing-whitespaces) 541 (hol-remove-tailing-empty-lines) 542 (message "Buffer cleaned up!")) 543 544;;replace common unicode chars with ascii version 545(setq hol-unicode-replacements '( 546 (nil "��" "~") 547 (nil "���" "/\\\\") 548 (nil "���" "\\\\/") 549 (nil "���" "==>") 550 (nil "���" "<=>") 551 (nil "���" "<=/=>") 552 (nil "���" "<>") 553 (nil "���" "?") 554 (nil "���" "!") 555 (t "���" "IN") 556 (t "���" "NOTIN") 557 (nil "��" "'a") 558 (nil "��" "'b") 559 (nil "��" "'c") 560 (nil "��" "'d") 561 (nil "��" "'e") 562 (nil "��" "'f") 563 (nil "��" "'g") 564 (nil "��" "'h") 565 (nil "��" "'i") 566 (nil "��" "'j") 567 (nil "��" "'l") 568 (nil "��" "'m") 569 (nil "��" "'n") 570 (nil "��" "'o") 571 (nil "��" "'p") 572 (nil "��" "'q") 573 (nil "��" "'r") 574 (nil "��" "'s") 575 (nil "��" "'t") 576 (nil "��" "'u") 577 (nil "��" "'v") 578 (nil "��" "'w") 579 (nil "��" "'x") 580 (nil "��" "'y") 581 (t "������" "<=+") 582 (t ">���" ">+") 583 (t "<���" "<+") 584 (t "������" ">=+") 585 (t "���" "<=") 586 (t "���" ">=") 587 (nil "���" "^+") 588 (t "������" "EMPTY_REL") 589 (t "�������" "RUNIV") 590 (t "������" "RSUBSET") 591 (t "������" "RUNION") 592 (t "������" "RINTER") 593 (t "���" "{}") 594 (nil "����" "univ") 595 (t "���" "SUBSET") 596 (t "���" "UNION") 597 (t "���" "INTER") 598 (t "���" "??") 599 (t "���" "||") 600 (t "���" "<<") 601 (t "���" ">>") 602 (t "���" ">>>") 603 (t "���" "#>>") 604 (t "���" "#<<") 605 (t "���" "o") 606 (t "������" "O") 607 (t "���" "-") 608)) 609 610 611(defun replace-string-in-buffer (s_old s_new) 612 (save-excursion 613 (goto-char (point-min)) 614 (while (search-forward s_old nil t) 615 (replace-match s_new)))) 616 617(defun replace-string-in-buffer_ensure_ws (s_old s_new) 618 (replace-string-in-buffer (concat " " s_old " ") (concat " " s_new " ")) 619 (replace-string-in-buffer (concat s_old " ") (concat " " s_new " ")) 620 (replace-string-in-buffer (concat " " s_old) (concat " " s_new " ")) 621 (replace-string-in-buffer s_old (concat " " s_new " ")) 622) 623 624(defun hol-remove-unicode () 625 (interactive) 626 (save-excursion 627 (save-restriction 628 (if (use-region-p) (narrow-to-region (region-beginning) (region-end))) 629 (dolist (elt hol-unicode-replacements) 630 (if (nth 0 elt) 631 (replace-string-in-buffer_ensure_ws (nth 1 elt) (nth 2 elt)) 632 (replace-string-in-buffer (nth 1 elt) (nth 2 elt)) 633 ))))) 634 635(defun hol-fl-extend-region () 636 (let ((newbeg (hol-fl-term-bump-backwards font-lock-beg)) 637 (newend (hol-fl-term-bump-forwards font-lock-end)) 638 (changed nil)) 639 (if (= newbeg font-lock-beg) nil 640 (setq font-lock-beg newbeg) 641 (setq changed t)) 642 (if (= newend font-lock-end) nil 643 (setq font-lock-end newend) 644 (setq changed t)) 645 changed)) 646 647(defun hol-movement-in-proof-p (pos) 648 (save-excursion 649 (goto-char pos) 650 (let ((pp (syntax-ppss))) 651 (and (not (nth 3 pp)) (not (nth 4 pp)) 652 (let ((nextre (re-search-backward hol-proof-beginend-re nil t))) 653 (and nextre 654 (let ((s (match-string-no-properties 0))) 655 (and (not (equal s "QED")) (not (equal s "End")) 656 (match-beginning 0))))))))) 657 658(defun hol-movement-backward-up-list 659 (&optional n escape-strings no-syntax-crossing) 660 (interactive "^p\nd\nd") 661 (or (let ((p (hol-movement-in-proof-p (point)))) (and p (goto-char p))) 662 (and (looking-at "^Proof\\>") 663 (re-search-backward "^\\(Triviality\\>\\|Theorem\\>\\)" nil t)) 664 (and (looking-at "^Termination\\>") 665 (re-search-backward "^Definition\\>" nil t)) 666 (backward-up-list n escape-strings no-syntax-crossing))) 667 668(defconst hol-movement-top-re 669 "^\\(Theorem\\|Triviality\\|Definition\\|Datatype\\|Overload\\|Type\\)") 670(defun hol-movement-backward-sexp (&optional arg) 671 (interactive "p") 672 (if (and (> arg 0) 673 (save-excursion 674 (beginning-of-line) 675 (looking-at hol-movement-top-re))) 676 (progn 677 (re-search-backward hol-movement-top-re nil t) 678 (hol-movement-backward-sexp (1- arg))) 679 (backward-sexp arg))) 680 681(defun holscript-fix-quotations (start end) 682 (interactive "r") 683 (shell-command-on-region start end 684 (concat (file-name-directory hol-executable) 685 "unquote --quotefix") 686 nil 687 t)) 688 689(defun holscript-mode-variables () 690 (set-syntax-table holscript-mode-syntax-table) 691 (setq local-abbrev-table holscript-mode-abbrev-table) 692 (smie-setup holscript-smie-grammar #'holscript-smie-rules 693 :backward-token #'holscript-smie-backward-token 694 :forward-token #'holscript-smie-forward-token) 695 (set (make-local-variable 'parse-sexp-ignore-comments) t) 696 (set (make-local-variable 'comment-start) "(* ") 697 (set (make-local-variable 'comment-end) " *)") 698 (set (make-local-variable 'comment-start-skip) "(\\*+\\s-*") 699 (set (make-local-variable 'comment-end-skip) "\\s-*\\*+)") 700 ;; No need to quote nested comments markers. 701 (set (make-local-variable 'comment-quote-nested) nil)) 702 703(defun holscript-indent-line () (indent-relative t)) 704 705(define-derived-mode holscript-mode prog-mode "HOLscript" 706 "\\<holscript-mode-map>Major mode for editing HOL Script.sml files. 707 708\\{sml-mode-map}" 709 (setq font-lock-multiline t) 710 (if (member 'hol-fl-extend-region font-lock-extend-region-functions) nil 711 (setq font-lock-extend-region-functions 712 (append font-lock-extend-region-functions 713 '(hol-fl-extend-region)))) 714 (set (make-local-variable 'font-lock-defaults) holscript-font-lock-defaults) 715 (set (make-local-variable 'indent-tabs-mode) nil) 716 (set (make-local-variable 'indent-line-function) 'holscript-indent-line) 717 (holscript-mode-variables) 718) 719 720(require 'hol-input) 721(add-hook 'holscript-mode-hook (lambda () (set-input-method "Hol"))) 722 723;; smie grammar 724 725(require 'smie) 726(defvar holscript-smie-grammar 727 (smie-prec2->grammar 728 (smie-bnf->prec2 729 '((id) 730 (decls (decls ";" decls) (decl)) 731 (decl ("^Theorem" theorem-contents "^QED") 732 ("^Triviality" theorem-contents "^QED") 733 ("^Theorem=" id) 734 ("^Triviality=" id) 735 ("^Definition" definition-contents "^End") 736 ("^Inductive" id-quoted "^End") 737 ("^CoInductive" id-quoted "^End") 738 ("^Overload" id) 739 ("^Type" id) 740 ("^Datatype:" quotedmaterial "^End") 741 ("val" id) 742 ("fun" id) 743 ("open" id) 744 ("datatype" id) 745 ("structure" id)) 746 (theorem-contents (id-quoted "^Proof" tactic)) 747 (definition-contents (id-quoted "^Termination" tactic) (id-quoted)) 748 (id-quoted (id ":" quotedmaterial)) 749 (quotedmaterial 750 ("QFIER." quotedmaterial "ENDQ." quotedmaterial) 751 (quotedmaterial "/\\" quotedmaterial) 752 (quotedmaterial "���" quotedmaterial) 753 (quotedmaterial "\\/" quotedmaterial) 754 (quotedmaterial "���" quotedmaterial) 755 (quotedmaterial "<=>" quotedmaterial) 756 (quotedmaterial "���" quotedmaterial) 757 (quotedmaterial "==>" quotedmaterial) 758 (quotedmaterial "���" quotedmaterial) 759 (quotedmaterial "=" quotedmaterial) 760 (quotedmaterial "<" quotedmaterial) 761 (quotedmaterial "���" quotedmaterial) 762 (quotedmaterial "<=" quotedmaterial) 763 (quotedmaterial "+" quotedmaterial) 764 (quotedmaterial "++" quotedmaterial) 765 (quotedmaterial "*" quotedmaterial) 766 (quotedmaterial ":=" quotedmaterial) 767 (quotedmaterial "<-" quotedmaterial) 768 (quotedmaterial "|" quotedmaterial) 769 (quotedmaterial "=>" quotedmaterial) 770 ("[defnlabel]" quotedmaterial) 771 ("case" quotedmaterial "of" quotedmaterial) 772 ("do" quotedmaterial "od") 773 ("if" quotedmaterial "then" quotedmaterial "else" quotedmaterial) 774 ("let" quotedmaterial "in" quotedmaterial) 775 ("<|" recd-fields "|>")) 776 (recd-fields (recd-fields ";" recd-fields) (quotedmaterial)) 777 (quotation ("���" quotedmaterial "���")) 778 (termtype ("���" quotedmaterial "���")) 779 (tactic (tactic ">>" tactic) 780 (tactic "\\\\" tactic) 781 (tactic ">-" tactic) 782 (tactic ">|" tactic) 783 (tactic "THEN" tactic) 784 (tactic "THEN1" tactic) 785 (tactic "THENL" tactic) 786 (quotation "by" tactic) 787 (quotation "suffices_by" tactic) 788 ("[" tactics "]")) 789 (tactics (tactic) (tactics "," tactics))) 790 '((assoc ",")) '((assoc ";")) 791 '((assoc "^Proof") 792 (left ">>" "\\\\" ">-" ">|" "THEN" "THEN1" "THENL") 793 (assoc "by" "suffices_by")) 794 '((assoc "ENDQ." "QFIER." "in" "of") 795 (assoc "|") 796 (assoc "=>") 797 (assoc "else") 798 (assoc "<=>" "���" "<-") 799 (assoc "==>" "���") (assoc "\\/" "���") (assoc "/\\" "���") 800 (assoc "[defnlabel]") 801 (assoc "=" "<" "���" "<=") (assoc ":=") (assoc "++" "+") (assoc "*"))))) 802 803(defvar holscript-quotedmaterial-delimiter-regexp 804 (regexp-opt (list "���" "���" "���" "���" holscript-quoteddeclaration-begin))) 805 806(defvar holscript-boolean-quantifiers '("���" "���" "���!")) 807 808(defvar holscript-quantifier-regexp 809 (concat (regexp-opt holscript-boolean-quantifiers) "\\|" 810 (regexp-opt '("some" "LEAST") 'symbols)) 811 "List of strings that can begin \"quantifier blocks\".") 812 813(defvar holscript-lambda-regexp "[��\\!?@]\\|?!" 814 "Regular expression for quantifiers that are (treated as) single punctuation 815class characters.") 816 817(defvar holscript-definitionlabel-re 818 "\\[~?[A-Za-z0-9_']+\\(\\[[A-Za-z0-9_',]+\\]\\)?[[:space:]]*:[[:space:]]*\\]" 819 "Regular expression for case-labels occurring within HOL definitions, 820ignoring fact that it should really only occur at the beginning of the line.") 821 822 823 824 825(defun holscript-can-find-earlier-quantifier (pp) 826 (let* ((pstk (nth 9 pp)) 827 (limit (car (last pstk))) 828 (case-fold-search nil)) 829 (save-mark-and-excursion 830 (catch 'found-one 831 (while (re-search-backward 832 (concat "\\(" holscript-quoteddeclaration-begin "\\)" "\\|" 833 "\\(" holscript-quoteddeclaration-end "\\)" "\\|" 834 holscript-quotedmaterial-delimiter-regexp "\\|" 835 holscript-quantifier-regexp "\\|" 836 holscript-lambda-regexp "\\|\\.") 837 limit 838 t) 839 (let ((pp1 (syntax-ppss)) 840 (sa (holscript-syntax-convert (syntax-after (point)))) 841 (sb (holscript-syntax-convert (syntax-after (1- (point)))))) 842 (if (or (nth 3 pp1) (nth 4 pp1)) 843 (goto-char (nth 8 pp1)) 844 (if (and sb (equal sa sb)) (forward-char -1) 845 (if (equal (car (last (nth 9 pp1))) limit) 846 (if (or (looking-at holscript-quantifier-regexp) 847 (looking-at holscript-lambda-regexp) 848 (looking-at "\\\\")) 849 (throw 'found-one (point)) 850 (throw 'found-one nil))))))))))) 851 852(defconst holscript-column0-keywords-regexp 853 (regexp-opt '("Definition" "Datatype" "Theorem" "Triviality" "Type" 854 "Proof" 855 "Termination" "End" "QED" "Inductive" "CoInductive" 856 "Overload"))) 857(defconst holscript-column0-declbegin-keyword 858 (regexp-opt '("Definition" "Datatype" "Theorem" "Triviality" 859 "Type" "Inductive" "CoInductive" "Overload"))) 860 861(defconst holscript-sml-declaration-keyword 862 (regexp-opt '("open" "val" "datatype" "local" "fun" "infix" "infixl" "infixr" 863 "structure" "signature" "functor") 'words)) 864 865(defun holscript-simple-token-forward () 866 (let* ((p (point)) 867 (sc (syntax-class (syntax-after p)))) 868 (cond 869 ((or (equal 1 sc) (equal 9 sc)); punctuation 870 (skip-syntax-forward ".\\") 871 (buffer-substring-no-properties p (point))) 872 ((equal 2 sc) ; word 873 (skip-syntax-forward "w") 874 (buffer-substring-no-properties p (point)))))) 875 876(defun holscript-simple-token-backward () 877 (let* ((p (point)) 878 (sc (syntax-class (syntax-after (1- p))))) 879 (cond 880 ((or (equal 1 sc) (equal 9 sc)); punctuation 881 (skip-syntax-backward ".\\") 882 (buffer-substring-no-properties (point) p)) 883 ((equal 2 sc) ; word 884 (skip-syntax-backward "w") 885 (buffer-substring-no-properties (point) p))))) 886 887(defun holscript-smie-forward-token () 888 (let ((p0 (point)) 889 (case-fold-search nil)) 890 (forward-comment (point-max)) 891 (if (and (not (= p0 (point))) 892 (or (looking-at 893 (concat holscript-column0-declbegin-keyword 894 "\\([[:space:]]\\|[[:space:]]*:\\)")) 895 (looking-at (concat "^" holscript-sml-declaration-keyword)))) 896 ";" 897 (let ((pp (syntax-ppss))) 898 (cond 899 ((and (looking-at (concat "\\(" holscript-column0-keywords-regexp 900 "\\)" "\\([[:space:]]\\|[[:space:]]*:\\)")) 901 (save-excursion (skip-chars-backward " \t") (bolp))) 902 (goto-char (match-end 1)) 903 (let ((ms (match-string-no-properties 1))) 904 (if (or (string= ms "Theorem") (string= ms "Triviality")) 905 (let ((eolpoint (save-excursion (end-of-line) (point)))) 906 (save-excursion 907 (if (re-search-forward ":" eolpoint t) (concat "^" ms) 908 (concat "^" ms "=")))) 909 (if (and (string= ms "Datatype") (looking-at "[[:space:]]*:")) 910 (progn (goto-char (match-end 0)) (concat "^" ms ":")) 911 (concat "^" ms))))) 912 ((looking-at holscript-quotedmaterial-delimiter-regexp) 913 (goto-char (match-end 0)) 914 (match-string-no-properties 0)) 915 ((and (looking-at holscript-definitionlabel-re) 916 (save-excursion (skip-chars-backward " \t") (bolp))) 917 (goto-char (match-end 0)) 918 "[defnlabel]") 919 ((looking-at "\\\\/") (goto-char (match-end 0)) "\\/") 920 ((looking-at "/\\\\") (goto-char (match-end 0)) "/\\") 921 ((looking-at "\\\\\\\\") (goto-char (match-end 0)) "\\\\") 922 ((looking-at "\\.") 923 (if (or (nth 3 pp) (nth 4 pp)) 924 (progn (forward-char 1) ".") 925 (let ((tok 926 (if (holscript-can-find-earlier-quantifier pp) "ENDQ." 927 "."))) 928 (forward-char 1) tok))) 929 ((looking-at holscript-quantifier-regexp) 930 (goto-char (match-end 0)) "QFIER.") 931 ((looking-at (concat "\\(?:" holscript-lambda-regexp "\\)\\S.")) 932 (if (equal 1 (syntax-class (syntax-after (1- (point))))) 933 (buffer-substring-no-properties 934 (point) 935 (progn (skip-syntax-forward ".") (point))) 936 (forward-char 1) "QFIER.")) 937 ((equal 1 (syntax-class (syntax-after (point)))) 938 ;; looking at "punctuation", meaning that it's what HOL could consider 939 ;; "symbolic" 940 (let* ((symstr (buffer-substring-no-properties 941 (point) 942 (progn (skip-syntax-forward ".") (point)))) 943 (ldel1 (cl-search "<|" symstr)) 944 (rdel1 (cl-search "|>" symstr)) 945 (del1 (or (and ldel1 rdel1 (min ldel1 rdel1)) ldel1 rdel1))) 946 (if del1 947 (if (= del1 0) 948 (progn 949 (forward-char (- 2 (length symstr))) 950 (substring symstr 0 2)) 951 (forward-char (- del1 (length symstr))) 952 (substring symstr 0 del1)) 953 symstr))) 954 ((looking-at "\\$") 955 (let ((p (point))) 956 (if (> (skip-chars-forward "$") 1) 957 (buffer-substring-no-properties p (point)) 958 (let ((simple-tok (holscript-simple-token-forward))) 959 (if (null simple-tok) 960 "$" 961 (if (= 1 ; punctuation, so don't look for more 962 (syntax-class 963 (aref (syntax-table) (aref simple-tok 0)))) 964 (buffer-substring-no-properties p (point)) 965 (if (looking-at "\\$") 966 (progn (forward-char 1) 967 (holscript-simple-token-forward))) 968 (buffer-substring-no-properties p (point)))))))) 969 (t (let ((p (point))) 970 (skip-syntax-forward "w_") 971 (if (looking-at "\\$") 972 (progn (forward-char 1) 973 (holscript-simple-token-forward))) 974 (buffer-substring-no-properties p (point))))))))) 975 976(defun holscript-maybe-skip-attr-list-backward () 977 (if (char-equal (char-before) ?\]) 978 (progn (forward-char -1) 979 (skip-chars-backward "A-Za-z0-9_',") 980 (if (char-equal (char-before) ?\[) (progn (forward-char -1) t) 981 nil)) 982 t)) 983 984(defun holscript-smie-backward-token () 985 (let ((case-fold-search nil)) 986 (if (or (and (looking-at 987 (concat holscript-column0-declbegin-keyword 988 "\\([[:space:]]\\|[[:space:]]*:\\)")) 989 (save-excursion (skip-chars-backward " \t") (bolp))) 990 (looking-at (concat "^" holscript-sml-declaration-keyword))) 991 (if (= (point) (point-min)) "" 992 (skip-syntax-backward " ") 993 ";") 994 (let ((cp (point))) 995 (forward-comment (- (point))) 996 (skip-syntax-backward " ") 997 (while (not (equal cp (point))) 998 (setq cp (point)) 999 (forward-comment (- (point))) 1000 (skip-syntax-backward " "))) 1001 (cond 1002 (; am I just after a keyword? 1003 (and (or 1004 (looking-back holscript-column0-keywords-regexp (- (point) 15) t) 1005 (looking-back "^\\(Datatype\\)[[:space:]]*:" (- (point) 20) t)) 1006 (let ((syn (syntax-after (point)))) 1007 ; next char is whitespace or colon 1008 (or (null syn) (= 0 (car syn)) (char-equal (char-after) ?:))) 1009 (save-excursion 1010 (goto-char (match-beginning 0)) 1011 (skip-chars-backward " \t") 1012 (bolp))) 1013 (goto-char (match-beginning 0)) 1014 (let ((ms (match-string-no-properties 0))) 1015 (if (or (string= ms "Theorem") (string= ms "Triviality")) 1016 (let ((eolpoint (save-excursion (end-of-line) (point)))) 1017 (save-excursion 1018 (if (re-search-forward ":" eolpoint t) (concat "^" ms) 1019 (concat "^" ms "=")))) 1020 (if (looking-at "Datatype[[:space:]]*:") "^Datatype:" 1021 (concat "^" ms))))) 1022 (; am I just after a quotation mark 1023 (looking-back holscript-quotedmaterial-delimiter-regexp (- (point) 1) t) 1024 (goto-char (match-beginning 0)) 1025 (match-string-no-properties 0)) 1026 (; am I after a definition-label 1027 (and (equal (char-before) ?\]) 1028 (let ((p (point))) 1029 (forward-char -1) 1030 (skip-chars-backward " \t") 1031 (if (equal (char-before) ?:) 1032 (progn (forward-char -1) 1033 (skip-chars-backward " \t") 1034 (if (holscript-maybe-skip-attr-list-backward) 1035 (progn 1036 (skip-chars-backward "A-Za-z0-9_'") 1037 (if (equal (char-before) ?~) (forward-char -1)) 1038 (skip-chars-backward " \t") 1039 (equal (char-before) ?\[)) 1040 (goto-char p) nil)) 1041 (goto-char p) nil))) 1042 (forward-char -1) "[defnlabel]") 1043 (; am I just after a quantifier 1044 (looking-back holscript-quantifier-regexp (- (point) 10) t) 1045 (goto-char (match-beginning 0)) 1046 (let ((c (char-before))) 1047 (if (and c (char-equal c ?$)) 1048 (progn (backward-char) (concat "$" (match-string-no-properties 0))) 1049 "QFIER."))) 1050 ((looking-back "\\\\\\\\" (- (point) 3)) 1051 (goto-char (match-beginning 0)) "\\\\") 1052 (; am I just after either a backslash or Greek lambda? 1053 (looking-back (concat "[^$[:punct:]]" holscript-lambda-regexp) 1054 (- (point) 3) nil) 1055 (if (equal 1 (syntax-class (syntax-after (point)))) 1056 (buffer-substring-no-properties 1057 (point) 1058 (progn (skip-syntax-backward ".") (point))) 1059 (backward-char) "QFIER.")) 1060 (; am I sitting on a full-stop that might end a quantifier block 1061 (let ((c (char-before))) (and c (char-equal c ?.))) 1062 (forward-char -1) 1063 (let* ((pp (syntax-ppss))) 1064 (if (or (nth 3 pp) (nth 4 pp)) "." 1065 (if (holscript-can-find-earlier-quantifier pp) "ENDQ." ".")))) 1066 ((looking-back "\\\\/" (- (point) 3)) 1067 (goto-char (match-beginning 0)) "\\/") 1068 ((looking-back "/\\\\" (- (point) 3)) 1069 (goto-char (match-beginning 0)) "/\\") 1070 (; am I sitting after "punctuation" 1071 (equal 1 (syntax-class (syntax-after (1- (point))))) 1072 (let* ((symstr (buffer-substring-no-properties 1073 (point) 1074 (progn (skip-syntax-backward ".") (point)))) 1075 (ldel (and (string-match ".*\\(<|\\)" symstr) 1076 (match-end 1))) 1077 (rdel (and (string-match ".*\\(|>\\)" symstr) 1078 (match-end 1))) 1079 (del (or (and ldel rdel (max ldel rdel)) ldel rdel)) 1080 (sz (length symstr))) 1081 (if del 1082 (if (= del sz) (progn (forward-char (- sz 2)) 1083 (substring symstr -2 nil)) 1084 (forward-char del) 1085 (substring symstr del nil)) 1086 symstr))) 1087 (t (buffer-substring-no-properties 1088 (point) 1089 (progn (skip-syntax-backward "w_") 1090 (point)))))))) 1091 1092(defvar holscript-indent-level 0 "Default indentation level") 1093(defcustom holscript-debugging-messages-p nil 1094 "Whether or not to emit debugging messages" 1095 :type 'boolean) 1096(defun holscript-message (s &rest rest) 1097 (if holscript-debugging-messages-p (apply 'message s rest))) 1098(defun holscript-smie-rules (kind token) 1099 (holscript-message "in smie rules, %d looking at (%s,>%s<)" 1100 (point) kind token) 1101 (pcase (cons kind token) 1102 (`(:elem . basic) (holscript-message "In elem rule") 0) 1103 (`(:list-intro . ":") 1104 (holscript-message "In list-intro :") 1105 holscript-indent-level) 1106 (`(:list-intro . "���") 1) 1107 (`(:list-intro . "���") 1) 1108 (`(:list-intro . "") 1109 (holscript-message "In (:list-intro \"\"))") holscript-indent-level) 1110 (`(:after . ":") 2) 1111 (`(:before . "^CoInductive") '(column . 0)) 1112 (`(:before . "^Definition") '(column . 0)) 1113 (`(:before . "^Inductive") '(column . 0)) 1114 (`(:before . "^Proof") '(column . 0)) 1115 (`(:before . "^QED") '(column . 0)) 1116 (`(:before . "^Termination") '(column . 0)) 1117 (`(:before . "^Theorem") '(column . 0)) 1118 (`(:before . "^Theorem=") '(column . 0)) 1119 (`(:before . "[defnlabel]") '(column . 0)) 1120 (`(:after . "[defnlabel]") 2) 1121 (`(:after . "^Proof") 2) 1122 (`(:after . "^Termination") 2) 1123 (`(:after . "^Datatype:") 2) 1124 (`(:before . "val") 0) 1125 (`(:before . "fun") 0) 1126 (`(:before . "open") 0) 1127 (`(:before . "ENDQ.") 0) 1128 (`(:after . "ENDQ.") 2) 1129 (`(:after . ";") 0) 1130 (`(:before . "let") (if (smie-rule-bolp) nil 0)) 1131 (`(:after . "let") 1132 (if (smie-rule-hanging-p) 1133 (progn (holscript-message "let-hanging") 1134 (cons 'column (+ (current-column) 2))) 1135 (holscript-message "Not let-hanging") 2)) 1136 (`(:after . "in") 2) 1137 (`(:before . "in") 1138 (if (smie-rule-parent-p "let") 1139 (progn (holscript-message "in: let a parent") 1140 (save-excursion 1141 (backward-up-list) 1142 (cons 'column (current-column)))) 1143 (smie-rule-parent))) 1144 (`(:after . "then") 2) 1145 (`(:after . "else") 2) 1146 (`(:after . "of") (if (smie-rule-next-p "|") 0 2)) 1147 (`(:before . "|") (if (smie-rule-parent-p "of") 0)) 1148 (`(:before ."if") 1149 (and (not (smie-rule-bolp)) 1150 (smie-rule-prev-p "else") 1151 (smie-rule-parent))) 1152 (`(:before . ":") holscript-indent-level) 1153 (`(:after . "=>") 2) 1154 (`(:after . "do") 2) 1155 ; (`(:before . "==>") 2) 1156 ; (`(:before . "���") 2) 1157 (`(:before . ,(or `"[" `"(" `"{")) 1158 (if (smie-rule-hanging-p) (smie-rule-parent 2))) 1159 (`(:before . "by") (cond ((smie-rule-parent-p "^Proof") 4) 1160 ((smie-rule-parent-p "(" "[") 3) 1161 (t 2))) 1162 (`(:before . "suffices_by") (cond ((smie-rule-parent-p "^Proof") 4) 1163 ((smie-rule-parent-p "(" "[") 3) 1164 (t 2))) 1165 (`(:close-all . _) t) 1166 (`(:after . "[") 2) 1167 (`(:after . "<|") 2) 1168 (`(:after . ">-") 1) 1169 (`(:after . "���") 1) 1170 (`(:after . "���") 1) 1171 (`(:after . "THEN1") 1) 1172 (`(:after . "���") 2) 1173)) 1174 1175;;; returns true and moves forward a sexp if this is possible, returns nil 1176;;; and stays where it is otherwise 1177(defun my-forward-sexp () 1178 (condition-case nil 1179 (progn (forward-sexp 1) t) 1180 (error nil))) 1181(defun my-backward-sexp() 1182 (condition-case nil 1183 (progn (backward-sexp 1) t) 1184 (error nil))) 1185 1186(defun word-before-point () 1187 (save-excursion 1188 (condition-case nil 1189 (progn (backward-char 1) (word-at-point)) 1190 (error nil)))) 1191 1192(defun backward-hol-tactic (n) 1193 (interactive "p") 1194 (forward-hol-tactic (if n (- n) -1))) 1195 1196(defun prim-mark-hol-tactic () 1197 (let ((bounds (bounds-of-thing-at-point 'hol-tactic))) 1198 (if bounds 1199 (progn 1200 (goto-char (cdr bounds)) 1201 (push-mark (car bounds) t t) 1202 (set-region-active)) 1203 (error "No tactic at point")))) 1204 1205(defun mark-hol-tactic () 1206 (interactive) 1207 (let ((initial-point (point))) 1208 (condition-case nil 1209 (prim-mark-hol-tactic) 1210 (error 1211 ;; otherwise, skip white-space forward to see if this would move us 1212 ;; onto a tactic. If so, great, otherwise, go backwards and look for 1213 ;; one there. Only if all this fails signal an error. 1214 (condition-case nil 1215 (progn 1216 (skip-chars-forward " \n\t\r") 1217 (prim-mark-hol-tactic)) 1218 (error 1219 (condition-case e 1220 (progn 1221 (if (skip-chars-backward " \n\t\r") 1222 (progn 1223 (backward-char 1) 1224 (prim-mark-hol-tactic)) 1225 (prim-mark-hol-tactic))) 1226 (error 1227 (goto-char initial-point) 1228 (signal (car e) (cdr e)))))))))) 1229 1230;; face info for syntax 1231(defface holscript-theorem-syntax 1232 '((((class color)) :foreground "blueviolet")) 1233 "The face for highlighting script file Theorem-Proof-QED syntax." 1234 :group 'holscript-faces) 1235 1236(defface holscript-thmname-syntax 1237 '((((class color)) :weight bold)) 1238 "The face for highlighting theorem names." 1239 :group 'holscript-faces) 1240 1241(defface holscript-cheat-face 1242 '((((class color)) :foreground "orange" :weight ultra-bold :box t)) 1243 "The face for highlighting occurrences of the cheat tactic." 1244 :group 'holscript-faces) 1245 1246(defface holscript-definition-syntax 1247 '((((class color)) :foreground "indianred")) 1248 "The face for highlighting script file definition syntax." 1249 :group 'holscript-faces) 1250 1251(defface holscript-quoted-material 1252 '((((class color)) :foreground "brown" :weight bold)) 1253 "The face for highlighting quoted material." 1254 :group 'holscript-faces) 1255 1256(defface holscript-then-syntax 1257 '((((class color)) :foreground "DarkSlateGray4" :weight bold)) 1258 "The face for highlighting `THEN' connectives in tactics." 1259 :group 'holscript-faces) 1260 1261(defface holscript-smlsyntax 1262 '((((class color)) :foreground "DarkOliveGreen" :weight bold)) 1263 "The face for highlighting important SML syntax that appears in script files." 1264 :group 'holscript-faces) 1265 1266(defface holscript-syntax-error-face 1267 '((((class color)) :foreground "red" :background "yellow" 1268 :weight bold :box t)) 1269 "The face for highlighting guaranteed syntax errors." 1270 :group 'holscript-faces) 1271 1272(defface holscript-definition-label-face 1273 '((((class color)) 1274 :foreground "PaleVioletRed4" 1275 :box (:line-width 1 :color "PaleVioletRed4" :style released-button) 1276 :slant normal :weight light)) 1277 "The face for highlighting definition labels in HOL material." 1278 :group 'holscript-faces) 1279 1280(setq auto-mode-alist (cons '("Script\\.sml" . holscript-mode) 1281 auto-mode-alist)) 1282