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

Re: [PVS-Help] Syntax highlighting

Hi Sam,

When I put that into my .pvsemacs (which did not previously exist), I get the message:
Wrong type argument: symbolp, “Syntax table for PVS mode.”

If I delete that line (but keep the final parenthesis), then it works, though.

Best Regards,
Ben Hocking

> On May 13, 2015, at 8:15 PM, Sam Owre <owre@xxxxxxxxxxx> wrote:
> 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)
>    st)
>  "Syntax table for PVS mode.")
> Regards,
> Sam
> 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