GitLab

The emacs mode for HOA, supports multiple automata in the same buffer. C-c C-c will display the automaton at point: this works by copying the surrounding HOA automaton, and piping it to autfilt and then dot. Of course when autfilt reports a syntax error, it will use line and column numbers that are relative to its input (just one automaton) so this will not make a lot of sense in the context of a buffer with many automata.

I would like to have an environment variable called SPOT_PARSE_LOCATION that could be used to "shift" the diagnostics of the HOA or LTL parsers in this kind of contexts. The variable would be read by the command-line tools in bin/ (I don't think it's good to have such a variable checked by the library), but the two parsers still need to provide the machinery necessary to shift error messages (or maybe simply set the original location).

For instance I'd like to have:

% autfilt -q < foo.hoa
3.9: syntax error, unexpected identifier
11.3: syntax error, unexpected ']'
11.2-3: ignoring this invalid label
% SPOT_PARSE_LOCATION=bar:11.1 autfilt -q < foo.hoa
bar:13.9: syntax error, unexpected identifier
bar:21.3: syntax error, unexpected ']'
bar:21.2-3: ignoring this invalid label

(Note that bar:11.1 describes the actual location of line 1, column 1 of the input.)