hoa-mode.el 8.12 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
;;; hoa-mode.el --- Major mode for the Hanoi Omega Automata format

;; Copyright (C) 2015  Alexandre Duret-Lutz

;; Author: Alexandre Duret-Lutz <adl@lrde.epita.fr>
;; Maintainer: Alexandre Duret-Lutz <adl@lrde.epita.fr>
;; URL: https://gitlab.lrde.epita.fr/spot/emacs-modes
;; Keywords: major-mode, automata, convenience
;; Created: 2015-11-13

;;; License:

;; This package is free software; you can redistribute it and/or modify
;; it under the terms of the GNU General Public License as published by
;; the Free Software Foundation; either version 3, or (at your option)
;; any later version.
;;
;; This package is distributed in the hope that it will be useful,
;; but WITHOUT ANY WARRANTY; without even the implied warranty of
;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
;; GNU General Public License for more details.
;;
;; You should have received a copy of the GNU General Public License
;; along with GNU Emacs.  If not, see <http://www.gnu.org/licenses/>.

;;; Commentary:

;; Major mode for editing files in the Hanoi Omega Automata format.
;; (See URL `http://adl.github.io/hoaf/' for that format.)  This
;; provides rules for syntax highlighting, some navigation functions,
;; and a convenient way to display the automata in Emacs.

;;; Code:

;;;###autoload
(add-to-list 'auto-mode-alist '("\\.hoa\\'" . hoa-mode))

;;;###autoload
(add-to-list 'magic-mode-alist '("\\<HOA:\\s-*v" . hoa-mode))

(defgroup hoa-mode nil
  "Major mode for editing Hanoi Omega Automata files."
  :group 'data)

(defgroup hoa-mode-faces nil
  "Faces used by `hoa-mode'."
  :group 'hoa-mode
  :group 'faces)

(defface hoa-header-uppercase-face
  '((t :inherit font-lock-type-face :weight bold))
  "Face for headers with an uppercase initial."
  :group 'hoa-mode-faces)

(defface hoa-header-lowercase-face
  '((t :inherit font-lock-type-face :weight normal))
  "Face for headers with a lowercase initial."
  :group 'hoa-mode-faces)

(defface hoa-keyword-face
  '((t :inherit font-lock-keyword-face))
  "Face used for --BODY--, --END--, and --ABORT--."
  :group 'hoa-mode-faces)

(defface hoa-builtin-face
  '((t :inherit font-lock-builtin-face))
  "Face used for Inf, Fin, t, and f."
  :group 'hoa-mode-faces)

(defface hoa-acceptance-set-face
  '((t :inherit font-lock-constant-face :weight bold))
  "Face used for acceptance sets."
  :group 'hoa-mode-faces)

(defface hoa-alias-face
  '((t :inherit font-lock-variable-name-face))
  "Face used for aliases."
  :group 'hoa-mode-faces)

(defface hoa-ap-number-face
  '((t :inherit font-lock-constant-face))
  "Face used for numbers that denote atomic propositions."
  :group 'hoa-mode-faces)

(defconst hoa-alias-regex
86
  "@[a-zA-Z0-9_.-]*\\_>"
87
88
  "Regex for matching aliases.")

89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
(defvar hoa-font-lock-keywords-1
  `(("\\_<--\\(:?BODY\\|END\\|ABORT\\)--" . 'hoa-keyword-face)
    ("\\_<\\(:?Inf\\|Fin\\|t\\|f\\)\\_>" . 'hoa-builtin-face)
    ("\\_<[A-Z][a-zA-Z0-9_.-]*:" . 'hoa-header-uppercase-face)
    ("\\_<[a-z][a-zA-Z0-9_.-]*:" . 'hoa-header-lowercase-face)
    (,hoa-alias-regex . 'hoa-alias-face))
  "Fontification rules for keywords, builtins, headers and aliases.")

(defvar hoa-font-lock-keywords-2
  (append hoa-font-lock-keywords-1
	  `(("(\\s-*\\([0-9]+\\)\\s-*)" 1 'hoa-acceptance-set-face)
	    ("{\\(\\([0-9]\\|\\s-\\)+\\)}" 1 'hoa-acceptance-set-face)
	    ;; numbers between brackets denote atomic propositions.
	    ("\\["
	     ("\\_<[0-9]+\\_>"
	      (save-excursion (search-forward "]" nil t))
	      nil
	      (0 'hoa-ap-number-face)))
	    ;; likewise for numbers following an Alias: definition
	    (,(concat "Alias:\\s-*" hoa-alias-regex)
	     ("\\_<[0-9]+\\_>"
	      (save-excursion
		(re-search-forward
		 (concat "\\(" hoa-alias-regex
			 "\\|[0-9|&!]\\|\\_<[ft]\\_>\\|\\s-\\)+") nil t))
	      nil
	      (0 'hoa-ap-number-face)))))
  "Complete fontification rules, including acceptance sets and AP numbers.")
117
118
119
120
121
122
123

(defvar hoa-mode-syntax-table
  (let ((st (make-syntax-table)))
    (modify-syntax-entry ?< "." st)
    (modify-syntax-entry ?> "." st)
    (modify-syntax-entry ?| "." st)
    (modify-syntax-entry ?_ "_" st)
124
    (modify-syntax-entry ?. "_" st)
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
    (modify-syntax-entry ?- "_" st)
    (modify-syntax-entry ?$ "." st)
    (modify-syntax-entry ?& "." st)
    (modify-syntax-entry ?+ "." st)
    (modify-syntax-entry ?/ ". 14bn" st)
    (modify-syntax-entry ?* ". 23bn" st)
    st)
  "Syntax table for `hoa-mode'.")

(defun hoa-start-of-automaton ()
  "Move to the start of the automaton at point."
  (interactive)
  (search-backward "HOA:"))

(defun hoa-end-of-automaton ()
  "Move to the end of the automaton at point."
  (interactive)
  ; if we are pointing inside something that looks like --END-- or
  ; --ABORT--, back out a bit.
  (if (looking-at "[ENDABORT-]*-")
      (backward-word))
  (re-search-forward "--\\(END\\|ABORT\\)--\n?"))

(defun hoa-mark-automaton-at-point ()
  "Mark the automaton at point."
  (interactive)
  (hoa-end-of-automaton)
  (set-mark (point))
  (hoa-start-of-automaton))

(defcustom hoa-display-error-buffer "*hoa-dot-error*"
  "The name of the buffer to display errors from `hoa-display-command'."
  :group 'hoa-mode
  :type 'string)

(defcustom hoa-display-buffer "*hoa-display*"
  "The name of the buffer to display automata."
  :group 'hoa-mode
  :type 'string)

(defcustom hoa-display-command "autfilt --dot='barf(Lato)' | dot -Tpng"
  "Command used to display HOA files.

The command is expected to take the automaton in HOA format on
its standard input, and output an image in PNG format on its
standard output.

The default value uses the tools autfilt (part of the Spot
package, see URL `https://spot.lrde.epita.fr/') and dot (part of
the GraphViz package, see URL `http://www.graphviz.org/')."
  :group 'hoa-mode
  :type 'string)

(defun hoa-display-automaton-at-point ()
  "Display the automaton-at-point.

This uses the command in `hoa-display-command' to convert HOA
into PNG, and then display the result in `hoa-display-buffer'.
If the command terminates with an error, its standard error is
put in `hoa-display-error-buffer' and shown."
  (interactive)
  (let ((b (save-excursion (if (not (looking-at "HOA:"))
			       (hoa-start-of-automaton)
			     (point))))
	(e (save-excursion (hoa-end-of-automaton) (point)))
	(dotbuf (generate-new-buffer "*hoa-dot-output*"))
	(errfile (make-temp-file
		  (expand-file-name "hoadot" temporary-file-directory)))
	(coding-system-for-read 'no-conversion))
    (with-current-buffer dotbuf
      (set-buffer-multibyte nil))
    (let ((exit-status
	   (call-process-region b e shell-file-name nil (list dotbuf errfile)
				nil shell-command-switch hoa-display-command)))
      (when (equal 0 exit-status)
200
201
	(let ((hoa-img (create-image (with-current-buffer dotbuf
				       (buffer-string))
202
203
				     'png t)))
	  (with-current-buffer (get-buffer-create hoa-display-buffer)
204
	    (setq buffer-read-only nil)
205
206
	    (erase-buffer)
	    (insert-image hoa-img)
207
	    (setq buffer-read-only t)
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
	    (display-buffer (current-buffer)))))
      (when (file-exists-p errfile)
	(when (< 0 (nth 7 (file-attributes errfile)))
	  (with-current-buffer (get-buffer-create hoa-display-error-buffer)
	    (setq buffer-read-only nil)
	    (erase-buffer)
	    (format-insert-file errfile nil)
	    (display-buffer (current-buffer))))
	(delete-file errfile))
      (kill-buffer dotbuf))))

(defvar hoa-mode-map
  (let ((map (make-keymap)))
    (define-key map "\M-e" 'hoa-end-of-automaton)
    (define-key map "\M-a" 'hoa-start-of-automaton)
    (define-key map "\C-\M-h" 'hoa-mark-automaton-at-point)
    (define-key map "\C-c\C-c" 'hoa-display-automaton-at-point)
    map)
  "Keymap for `hoa-mode'.")

;;;### autoload
229
(define-derived-mode hoa-mode fundamental-mode "HOA"
230
231
232
233
234
235
236
237
238
239
240
  "Major mode for editing files in the Hanoi Omega Automata format.

See URL `http://adl.github.io/hoaf/' for a definition of that format.

The following key bindings are installed in hoa-mode:

\\{hoa-mode-map}

By default the `hoa-display-automaton-at-point' function requires
extra software (Spot and GraphViz), but can be configured to use
other tools.  See that function for details."
241
242
243
244
  :group 'hoa-mode
  (setq font-lock-defaults '((hoa-font-lock-keywords-1
			      hoa-font-lock-keywords-1
			      hoa-font-lock-keywords-2))))
245
246
247

(provide 'hoa-mode)
;;; hoa-mode.el ends here