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

Re: [PVS-Help] Syntax highlighting



Hi Ben,

Sorry about that; I copied a defvar and changed it to a setq without
noticing the document string.  Your fix is the correct one.

Sam

Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:

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