HOL4/tools/holscript-mode.el

3 ;; font-locking and syntax
8           (1 'holscript-theorem-syntax) (2 'holscript-thmname-syntax))
9         '("^\\(Proof\\|^QED\\)\\>" . 'holscript-theorem-syntax)
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)
25         '(holscript-find-syntax-error 0 'holscript-syntax-error-face prepend)
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)
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)) ".%&+-/:<=>?@`^|!~#,;")
51   "The syntax table used in `holscript-mode'.")
135            (skip-syntax-forward "^.")
136            (skip-syntax-forward ".")
140          (setq n (- n (if (equal (skip-syntax-backward ".") 0) 0 1))))
142            (skip-syntax-backward "^.")
143            (skip-syntax-backward ".")
240              (skip-syntax-forward " ")
244                (skip-syntax-forward " ")
252              (skip-syntax-backward " ")
258                (skip-syntax-backward " ")
268              (skip-syntax-forward " ")
272                (skip-syntax-forward " ")
280              (skip-syntax-backward " ")
286                (skip-syntax-backward " ")
302              (skip-syntax-forward " "))
305              (skip-syntax-forward " "))
306            (skip-syntax-backward " ")
314              (skip-syntax-backward " "))
317              (skip-syntax-backward " "))
318            (skip-syntax-forward " ")
328 (defun holscript-syntax-convert (n) (if (and n (equal (car n) 9)) '(1) n))
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))))
342   "Regular expression marking the beginning of the special syntax that marks
359             (ppss (syntax-ppss)))
363           (setq ppss (syntax-ppss)))
368 (defun holscript-find-syntax-error (limit)
371         (ppss (syntax-ppss)))
379       (setq ppss (syntax-ppss)))
511                                   (equal (char-syntax (following-char)) ?\s))))
650     (let ((pp (syntax-ppss)))
659     (&optional n escape-strings no-syntax-crossing)
666       (backward-up-list n escape-strings no-syntax-crossing)))
690   (set-syntax-table holscript-mode-syntax-table)
691   (setq local-abbrev-table holscript-mode-abbrev-table)
839           (let ((pp1 (syntax-ppss))
840                 (sa (holscript-syntax-convert (syntax-after (point))))
841                 (sb (holscript-syntax-convert (syntax-after (1- (point))))))
867          (sc (syntax-class (syntax-after p))))
870       (skip-syntax-forward ".\\")
873       (skip-syntax-forward "w")
878          (sc (syntax-class (syntax-after (1- p)))))
881       (skip-syntax-backward ".\\")
884       (skip-syntax-backward "w")
897       (let ((pp (syntax-ppss)))
932           (if (equal 1 (syntax-class (syntax-after (1- (point)))))
935                (progn (skip-syntax-forward ".") (point)))
937          ((equal 1 (syntax-class (syntax-after (point))))
942                          (progn (skip-syntax-forward ".") (point))))
962                          (syntax-class
963                           (aref (syntax-table) (aref simple-tok 0))))
970               (skip-syntax-forward "w_")
992           (skip-syntax-backward " ")
996         (skip-syntax-backward " ")
1000           (skip-syntax-backward " ")))
1006              (let ((syn (syntax-after (point))))
1055         (if (equal 1 (syntax-class (syntax-after (point))))
1058              (progn (skip-syntax-backward ".") (point)))
1063         (let* ((pp (syntax-ppss)))
1071         (equal 1 (syntax-class (syntax-after (1- (point)))))
1074                         (progn (skip-syntax-backward ".") (point))))
1089            (progn (skip-syntax-backward "w_")
1230 ;; face info for syntax
1231 (defface holscript-theorem-syntax
1233   "The face for highlighting script file Theorem-Proof-QED syntax."
1236 (defface holscript-thmname-syntax
1246 (defface holscript-definition-syntax
1248   "The face for highlighting script file definition syntax."
1256 (defface holscript-then-syntax
1263   "The face for highlighting important SML syntax that appears in script files."
1266 (defface holscript-syntax-error-face
1269   "The face for highlighting guaranteed syntax errors."