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

[Uwe Brauer]

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
I am asking for advice.



    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