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

Re: [PVS-Help] loading files, indentation

If I remember correctly, since PVS 3.1 the command "$ pvs filename.pvs"
does not load filename.pvs (at least not in GNU Emacs 21). As for
indentations, it seems to me that they are not defined in the PVS emacs
mode (at least not in GNU Emacs 21).

On Wed, 2004-04-14 at 14:34, John Rushby wrote:
> Rob,
> > Is there a way of telling pvs to load a particular .pvs file from
> > the command line?
> PVS just passes command line arguments to Emacs, so it's just the same
> as starting Emacs on a file: type "pvs filename"
> However, the normal method of use is to start PVS when your machine
> boots, and to leave it running for months on end, so your question
> suggests you may be using PVS in some nonstandard way.  Maybe you need
> batch mode?  (See Chapter 5 of the system manual).
> > Do you know how I can see exactly what variables
> > 'pvs-mode' changes (and the functions it calls)?
> The source for all the PVS Emacs files are part of the distribution,
> so just look through them.  Usually, only real Emacs experts would
> tinker with this stuff, and only they would have settings that might
> conflict with PVS mode.   
> If you're not an Emacs guru, try describing you the problem you're
> confronting and we'll see if we can help you.
> John
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace      mailto://C.A.Munoz@larc.nasa.gov
144 Research Drive                  http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 766 1539 Fax +1 (757) 766 1855