auctex-devel
[Top][All Lists]

## [AUCTeX-devel] Support of Lamport pf2.sty and some questions

 From: Uwe Brauer Subject: [AUCTeX-devel] Support of Lamport pf2.sty and some questions Date: Thu, 26 Jul 2018 18:41:18 +0200 User-agent: Gnus/5.13 (Gnus v5.13) Emacs/27.0.50 (gnu/linux)

Hi

I am currently getting acquainted with Leslie Lamports pf2.sty
(http://lamport.azurewebsites.net/latex/latex.html).

And try to add a corresponding lisp style auctex file.

Here is an example of a proof using Lamports pf2.sty

\pfhidelevel{1}
\begin{proof}
\step{item:test-lamport2:1b}{Text of step 1.}
\begin{proof}
\step{label-1.1}{Text of substep 1}
\begin{proof}
\pf\ Paragraph proof using results in \stepref{label-1.1} .~\qed
\end{proof}
\step{label-2.1}{Text of substep 2}
\end{proof}
\step{label-2.2}{Text of step 2}
\end{proof}

Most of the commands (which are not included in the above example) are
straightforward. There are, however, some complications and that is why

1. The reference system and reftex: Lamports syntax is to use
\stepref as a command not \ref (its label system is also
different). How could the stepref be included in reftex?

2. The step command. I think it would most convenient to treat the
step command as if it where a sort of item, and the corresponding
label would be inserted automatically. Diggin in the exam style
file I think I know how to produce \step{}{} but I don't know who
to insert \step{automatic label}{}.

3. The line          \step{label-1.1}{Text of substep 1} is
equivalent to
\begin{step+}{label-1.1}
Text of substep 1
\end{step+}
but again, how to I obtain automatically the {label-1.1}?

Thanks for any help

Uwe Brauer


smime.p7s
Description: S/MIME cryptographic signature