[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Syntax highlighting



Hi all,

This is a rather picky observation, but I’ve noticed that the syntax highlighting for PVS isn’t exactly right. Specifically, if you have a reserved word as part of a function or variable name, that part of the name is highlighted as if it were a stand alone word. E.g., a lemma titled “x_implies_y” will have the “implies” portion of the lemma highlighted. I tried digging around in pvs/emacs/emacs-src to see if I could find the syntax highlighting rules to fix it myself (basically, to tell it that the underscore is a word character), but I had no such luck. I found that there’s a function called “make-syntax-table” that’s being called, but I cannot find where that function is defined:
▶ find . -name "*.el" -exec grep -Hn make-syntax-table {} \;
./pvs-mode.el:110:     (setq pvs-mode-syntax-table (make-syntax-table))
./pvs-prover.el:571:     (setq pvs-proof-script-syntax-table (make-syntax-table))
./pvs-utils.el:55:     (setq pvs-search-syntax-table (make-syntax-table))
./tcl.el:246:  (setq tcl-mode-syntax-table (make-syntax-table))

Any insight would be appreciated.

Best Regards,
Ben Hocking