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

Re: [PVS-Help] Syntax highlighting

Hi Ben,

There was something wrong in the way the syntax table was generated.  It's
in emacs/emacs-src/pvs-mode.el.  I just now modified it and pushed the new
version.  You can quickly get it working by adding the following to your
~/.pvsemacs (create it if it doesn't exist):

(setq pvs-mode-syntax-table
  (let ((st (make-syntax-table)))
    (modify-syntax-entry ?_ "w" st)
    (modify-syntax-entry ?\? "w" st)
    (modify-syntax-entry ?: "." st)
    (modify-syntax-entry ?% "<" st)
    (modify-syntax-entry ?\f ">" st)
    (modify-syntax-entry ?\n ">" st)
    (modify-syntax-entry ?\r ">" st)
  "Syntax table for PVS mode.")


Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:

> 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
> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx