User Tools
Sidebar
latex:sty
tlalatex.sty
\usepackage{latexsym} \usepackage{ifthen} % \usepackage{color} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % SWITCHES % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newboolean{shading} \setboolean{shading}{false} \makeatletter %% this is needed only when inserted into the file, not when %% used as a package file. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % DEFINITIONS OF SYMBOL-PRODUCING COMMANDS % % % % TLA+ LaTeX % % symbol command % % ------ ------- % % => \implies % % <: \ltcolon % % :> \colongt % % == \defeq % % .. \dotdot % % :: \coloncolon % % =| \eqdash % % ++ \pp % % -- \mm % % ** \stst % % // \slsl % % ^ \ct % % \A \A % % \E \E % % \AA \AA % % \EE \EE % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newlength{\symlength} \newcommand{\implies}{\Rightarrow} \newcommand{\ltcolon}{\mathrel{<\!\!\mbox{:}}} \newcommand{\colongt}{\mathrel{\!\mbox{:}\!\!>}} \newcommand{\defeq}{\;\mathrel{\smash %% keep this symbol from being too tall {{\stackrel{\scriptscriptstyle\Delta}{=}}}}\;} \newcommand{\dotdot}{\mathrel{\ldotp\ldotp}} \newcommand{\coloncolon}{\mathrel{::\;}} \newcommand{\eqdash}{\mathrel = \joinrel \hspace{-.28em}|} \newcommand{\pp}{\mathbin{++}} \newcommand{\mm}{\mathbin{--}} \newcommand{\stst}{*\!*} \newcommand{\slsl}{/\!/} \newcommand{\ct}{\hat{\hspace{.4em}}} \newcommand{\A}{\forall} \newcommand{\E}{\exists} \renewcommand{\AA}{\makebox{$\raisebox{.05em}{\makebox[0pt][l]{% $\forall\hspace{-.517em}\forall\hspace{-.517em}\forall$}}% \forall\hspace{-.517em}\forall \hspace{-.517em}\forall\,$}} \newcommand{\EE}{\makebox{$\raisebox{.05em}{\makebox[0pt][l]{% $\exists\hspace{-.517em}\exists\hspace{-.517em}\exists$}}% \exists\hspace{-.517em}\exists\hspace{-.517em}\exists\,$}} \newcommand{\whileop}{\.{\stackrel {\mbox{\raisebox{-.3em}[0pt][0pt]{$\scriptscriptstyle+\;\,$}}}% {-\hspace{-.16em}\triangleright}}} % Commands are defined to produce the upper-case keywords. % Note that some have space after them. \newcommand{\ASSUME}{\textsc{assume }} \newcommand{\ASSUMPTION}{\textsc{assumption }} \newcommand{\AXIOM}{\textsc{axiom }} \newcommand{\BOOLEAN}{\textsc{boolean }} \newcommand{\CASE}{\textsc{case }} \newcommand{\CONSTANT}{\textsc{constant }} \newcommand{\CONSTANTS}{\textsc{constants }} \newcommand{\ELSE}{\settowidth{\symlength}{\THEN}% \makebox[\symlength][l]{\textsc{ else}}} \newcommand{\EXCEPT}{\textsc{ except }} \newcommand{\EXTENDS}{\textsc{extends }} \newcommand{\FALSE}{\textsc{false}} \newcommand{\IF}{\textsc{if }} \newcommand{\IN}{\settowidth{\symlength}{\LET}% \makebox[\symlength][l]{\textsc{in}}} \newcommand{\INSTANCE}{\textsc{instance }} \newcommand{\LET}{\textsc{let }} \newcommand{\LOCAL}{\textsc{local }} \newcommand{\MODULE}{\textsc{module }} \newcommand{\OTHER}{\textsc{other }} \newcommand{\STRING}{\textsc{string}} \newcommand{\THEN}{\textsc{ then }} \newcommand{\THEOREM}{\textsc{theorem }} \newcommand{\LEMMA}{\textsc{lemma }} \newcommand{\PROPOSITION}{\textsc{proposition }} \newcommand{\COROLLARY}{\textsc{corollary }} \newcommand{\TRUE}{\textsc{true}} \newcommand{\VARIABLE}{\textsc{variable }} \newcommand{\VARIABLES}{\textsc{variables }} \newcommand{\WITH}{\textsc{ with }} \newcommand{\WF}{\textrm{WF}} \newcommand{\SF}{\textrm{SF}} \newcommand{\CHOOSE}{\textsc{choose }} \newcommand{\ENABLED}{\textsc{enabled }} \newcommand{\UNCHANGED}{\textsc{unchanged }} \newcommand{\SUBSET}{\textsc{subset }} \newcommand{\UNION}{\textsc{union }} \newcommand{\DOMAIN}{\textsc{domain }} % Added for tla2tex \newcommand{\BY}{\textsc{by }} \newcommand{\OBVIOUS}{\textsc{obvious }} \newcommand{\HAVE}{\textsc{have }} \newcommand{\QED}{\textsc{qed }} \newcommand{\TAKE}{\textsc{take }} \newcommand{\DEF}{\textsc{ def }} \newcommand{\HIDE}{\textsc{hide }} \newcommand{\RECURSIVE}{\textsc{recursive }} \newcommand{\USE}{\textsc{use }} \newcommand{\DEFINE}{\textsc{define }} \newcommand{\PROOF}{\textsc{proof }} \newcommand{\WITNESS}{\textsc{witness }} \newcommand{\PICK}{\textsc{pick }} \newcommand{\DEFS}{\textsc{defs }} \newcommand{\PROVE}{\settowidth{\symlength}{\ASSUME}% \makebox[\symlength][l]{\textsc{prove}}\@s{-4.1}}% %% The \@s{-4.1) is a kludge added on 24 Oct 2009 [happy birthday, Ellen] %% so the correct alignment occurs if the user types %% ASSUME X %% PROVE Y %% because it cancels the extra 4.1 pts added because of the %% extra space after the PROVE. This seems to works OK. %% However, the 4.1 equals Parameters.LaTeXLeftSpace(1) and %% should be changed if that method ever changes. \newcommand{\SUFFICES}{\textsc{suffices }} \newcommand{\NEW}{\textsc{new }} \newcommand{\LAMBDA}{\textsc{lambda }} \newcommand{\STATE}{\textsc{state }} \newcommand{\ACTION}{\textsc{action }} \newcommand{\TEMPORAL}{\textsc{temporal }} \newcommand{\ONLY}{\textsc{only }} %% added by LL on 2 Oct 2009 \newcommand{\OMITTED}{\textsc{omitted }} %% added by LL on 31 Oct 2009 \newcommand{\@pfstepnum}[2]{\ensuremath{\langle#1\rangle}\textrm{#2}} \newcommand{\bang}{\@s{1}\mbox{\small !}\@s{1}} %% We should format || differently in PlusCal code than in TLA+ formulas. \newcommand{\p@barbar}{\ifpcalsymbols \,\,\rule[-.25em]{.075em}{1em}\hspace*{.2em}\rule[-.25em]{.075em}{1em}\,\,% \else \,||\,\fi} %% PlusCal keywords \newcommand{\p@fair}{\textbf{fair }} \newcommand{\p@semicolon}{\textbf{\,; }} \newcommand{\p@algorithm}{\textbf{algorithm }} \newcommand{\p@mmfair}{\textbf{-{}-fair }} \newcommand{\p@mmalgorithm}{\textbf{-{}-algorithm }} \newcommand{\p@assert}{\textbf{assert }} \newcommand{\p@await}{\textbf{await }} \newcommand{\p@begin}{\textbf{begin }} \newcommand{\p@end}{\textbf{end }} \newcommand{\p@call}{\textbf{call }} \newcommand{\p@define}{\textbf{define }} \newcommand{\p@do}{\textbf{ do }} \newcommand{\p@either}{\textbf{either }} \newcommand{\p@or}{\textbf{or }} \newcommand{\p@goto}{\textbf{goto }} \newcommand{\p@if}{\textbf{if }} \newcommand{\p@then}{\,\,\textbf{then }} \newcommand{\p@else}{\ifcsyntax \textbf{else } \else \,\,\textbf{else }\fi} \newcommand{\p@elsif}{\,\,\textbf{elsif }} \newcommand{\p@macro}{\textbf{macro }} \newcommand{\p@print}{\textbf{print }} \newcommand{\p@procedure}{\textbf{procedure }} \newcommand{\p@process}{\textbf{process }} \newcommand{\p@return}{\textbf{return}} \newcommand{\p@skip}{\textbf{skip}} \newcommand{\p@variable}{\textbf{variable }} \newcommand{\p@variables}{\textbf{variables }} \newcommand{\p@while}{\textbf{while }} \newcommand{\p@when}{\textbf{when }} \newcommand{\p@with}{\textbf{with }} \newcommand{\p@lparen}{\textbf{(\,\,}} \newcommand{\p@rparen}{\textbf{\,\,) }} \newcommand{\p@lbrace}{\textbf{\{\,\,}} \newcommand{\p@rbrace}{\textbf{\,\,\} }} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % REDEFINE STANDARD COMMANDS TO MAKE THEM FORMAT BETTER % % % % We redefine \in and \notin % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \renewcommand{\_}{\rule{.4em}{.06em}\hspace{.05em}} \newlength{\equalswidth} \let\oldin=\in \let\oldnotin=\notin \renewcommand{\in}{% {\settowidth{\equalswidth}{$\.{=}$}\makebox[\equalswidth][c]{$\oldin$}}} \renewcommand{\notin}{% {\settowidth{\equalswidth}{$\.{=}$}\makebox[\equalswidth]{$\oldnotin$}}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % HORIZONTAL BARS: % % % % \moduleLeftDash |~~~~~~~~~~ % % \moduleRightDash ~~~~~~~~~~| % % \midbar |----------| % % \bottombar |__________| % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newlength{\charwidth}\settowidth{\charwidth}{{\small\tt M}} \newlength{\boxrulewd}\setlength{\boxrulewd}{.4pt} \newlength{\boxlineht}\setlength{\boxlineht}{.5\baselineskip} \newcommand{\boxsep}{\charwidth} \newlength{\boxruleht}\setlength{\boxruleht}{.5ex} \newlength{\boxruledp}\setlength{\boxruledp}{-\boxruleht} \addtolength{\boxruledp}{\boxrulewd} \newcommand{\boxrule}{\leaders\hrule height \boxruleht depth \boxruledp \hfill\mbox{}} \newcommand{\@computerule}{% \setlength{\boxruleht}{.5ex}% \setlength{\boxruledp}{-\boxruleht}% \addtolength{\boxruledp}{\boxrulewd}} \newcommand{\bottombar}{\hspace{-\boxsep}% \raisebox{-\boxrulewd}[0pt][0pt]{\rule[.5ex]{\boxrulewd}{\boxlineht}}% \boxrule \raisebox{-\boxrulewd}[0pt][0pt]{% \rule[.5ex]{\boxrulewd}{\boxlineht}}\hspace{-\boxsep}\vspace{0pt}} \newcommand{\moduleLeftDash}% {\hspace*{-\boxsep}% \raisebox{-\boxlineht}[0pt][0pt]{\rule[.5ex]{\boxrulewd }{\boxlineht}}% \boxrule\hspace*{.4em }} \newcommand{\moduleRightDash}% {\hspace*{.4em}\boxrule \raisebox{-\boxlineht}[0pt][0pt]{\rule[.5ex]{\boxrulewd }{\boxlineht}}\hspace{-\boxsep}}%\vspace{.2em} \newcommand{\midbar}{\hspace{-\boxsep}\raisebox{-.5\boxlineht}[0pt][0pt]{% \rule[.5ex]{\boxrulewd}{\boxlineht}}\boxrule\raisebox{-.5\boxlineht% }[0pt][0pt]{\rule[.5ex]{\boxrulewd}{\boxlineht}}\hspace{-\boxsep}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % FORMATING COMMANDS % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % PLUSCAL SHADING % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % The TeX pcalshading switch is set on to cause PlusCal shading to be % performed. This changes the behavior of the following commands and % environments to cause full-width shading to be performed on all lines. % % \tstrut \@x cpar mcom \@pvspace % % The TeX pcalsymbols switch is turned on when typesetting a PlusCal algorithm, % whether or not shading is being performed. It causes symbols (other than % parentheses and braces and PlusCal-only keywords) that should be typeset % differently depending on whether they are in an algorithm to be typeset % appropriately. Currently, the only such symbol is "||". % % The TeX csyntax switch is turned on when typesetting a PlusCal algorithm in % c-syntax. This allows symbols to be format differently in the two syntaxes. % The "else" keyword is the only one that is. \newif\ifpcalshading \pcalshadingfalse \newif\ifpcalsymbols \pcalsymbolsfalse \newif\ifcsyntax \csyntaxtrue % The \@pvspace command makes a vertical space. It uses \vspace % except with \ifpcalshading, in which case it sets \pvcalvspace % and the space is added by a following \@x command. % \newlength{\pcalvspace}\setlength{\pcalvspace}{0pt}% \newcommand{\@pvspace}[1]{% \ifpcalshading \par\global\setlength{\pcalvspace}{#1}% \else \par\vspace{#1}% \fi } % The lcom environment was changed to set \lcomindent equal to % the indentation it produces. This length is used by the % cpar environment to make shading extend for the full width % of the line. This assumes that lcom environments are not % nested. I hope TLATeX does not nest them. % \newlength{\lcomindent}% \setlength{\lcomindent}{0pt}% %\tstrut: A strut to produce inter-paragraph space in a comment. %\rstrut: A strut to extend the bottom of a one-line comment so % there's no break in the shading between comments on % successive lines. \newcommand\tstrut% {\raisebox{\vshadelen}{\raisebox{-.25em}{\rule{0pt}{1.15em}}}% \global\setlength{\vshadelen}{0pt}} \newcommand\rstrut{\raisebox{-.25em}{\rule{0pt}{1.15em}}% \global\setlength{\vshadelen}{0pt}} % \.{op} formats operator op in math mode with empty boxes on either side. % Used because TeX otherwise vary the amount of space it leaves around op. \renewcommand{\.}[1]{\ensuremath{\mbox{}#1\mbox{}}} % \@s{n} produces an n-point space \newcommand{\@s}[1]{\hspace{#1pt}} % \@x{txt} starts a specification line in the beginning with txt % in the final LaTeX source. \newlength{\@xlen} \newcommand\xtstrut% {\setlength{\@xlen}{1.05em}% \addtolength{\@xlen}{\pcalvspace}% \raisebox{\vshadelen}{\raisebox{-.25em}{\rule{0pt}{\@xlen}}}% \global\setlength{\vshadelen}{0pt}% \global\setlength{\pcalvspace}{0pt}} \newcommand{\@x}[1]{\par \ifpcalshading \makebox[0pt][l]{\shadebox{\xtstrut\hspace*{\textwidth}}}% \fi \mbox{$\mbox{}#1\mbox{}$}} % \@xx{txt} continues a specification line with the text txt. \newcommand{\@xx}[1]{\mbox{$\mbox{}#1\mbox{}$}} % \@y{cmt} produces a one-line comment. \newcommand{\@y}[1]{\mbox{\footnotesize\hspace{.65em}% \ifthenelse{\boolean{shading}}{% \shadebox{#1\hspace{-\the\lastskip}\rstrut}}% {#1\hspace{-\the\lastskip}\rstrut}}} % \@z{cmt} produces a zero-width one-line comment. \newcommand{\@z}[1]{\makebox[0pt][l]{\footnotesize \ifthenelse{\boolean{shading}}{% \shadebox{#1\hspace{-\the\lastskip}\rstrut}}% {#1\hspace{-\the\lastskip}\rstrut}}} % \@w{str} produces the TLA+ string "str". \newcommand{\@w}[1]{\textsf{``{#1}''}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % SHADING % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \def\graymargin{1} % The number of points of margin in the shaded box. % \definecolor{boxshade}{gray}{.85} % Defines the darkness of the shading: 1 = white, 0 = black % Added by TLATeX only if needed. % \shadebox{txt} puts txt in a shaded box. \newlength{\templena} \newlength{\templenb} \newsavebox{\tempboxa} \newcommand{\shadebox}[1]{{\setlength{\fboxsep}{\graymargin pt}% \savebox{\tempboxa}{#1}% \settoheight{\templena}{\usebox{\tempboxa}}% \settodepth{\templenb}{\usebox{\tempboxa}}% \hspace*{-\fboxsep}\raisebox{0pt}[\templena][\templenb]% {\colorbox{boxshade}{\usebox{\tempboxa}}}\hspace*{-\fboxsep}}} % \vshade{n} makes an n-point inter-paragraph space, with % shading if the `shading' flag is true. \newlength{\vshadelen} \setlength{\vshadelen}{0pt} \newcommand{\vshade}[1]{\ifthenelse{\boolean{shading}}% {\global\setlength{\vshadelen}{#1pt}}% {\vspace{#1pt}}} \newlength{\boxwidth} \newlength{\multicommentdepth} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % THE cpar ENVIRONMENT % % ^^^^^^^^^^^^^^^^^^^^ % % The LaTeX input % % % % \begin{cpar}{pop}{nest}{isLabel}{d}{e}{arg6} % % XXXXXXXXXXXXXXX % % XXXXXXXXXXXXXXX % % XXXXXXXXXXXXXXX % % \end{cpar} % % % % produces one of two possible results. If isLabel is the letter "T", % % it produces the following, where [label] is the result of typesetting % % arg6 in an LR box, and d is is a number representing a distance in % % points. % % % % prevailing |<-- d -->[label]<- e ->XXXXXXXXXXXXXXX % % left | XXXXXXXXXXXXXXX % % margin | XXXXXXXXXXXXXXX % % % % If isLabel is the letter "F", then it produces % % % % prevailing |<-- d -->XXXXXXXXXXXXXXXXXXXXXXX % % left | <- e ->XXXXXXXXXXXXXXXX % % margin | XXXXXXXXXXXXXXXX % % % % where d and e are numbers representing distances in points. % % % % The prevailing left margin is the one in effect before the most recent % % pop (argument 1) cpar environments with "T" as the nest argument, where % % pop is a number \geq 0. % % % % If the nest argument is the letter "T", then the prevailing left % % margin is moved to the left of the second (and following) lines of % % X's. Otherwise, the prevailing left margin is left unchanged. % % % % An \unnest{n} command moves the prevailing left margin to where it was % % before the most recent n cpar environments with "T" as the nesting % % argument. % % % % The environment leaves no vertical space above or below it, or between % % its paragraphs. (TLATeX inserts the proper amount of vertical space.) % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newcounter{pardepth} \setcounter{pardepth}{0} % \setgmargin{txt} defines \gmarginN to be txt, where N is \roman{pardepth}. % \thegmargin equals \gmarginN, where N is \roman{pardepth}. \newcommand{\setgmargin}[1]{% \expandafter\xdef\csname gmargin\roman{pardepth}\endcsname{#1}} \newcommand{\thegmargin}{\csname gmargin\roman{pardepth}\endcsname} \newcommand{\gmargin}{0pt} \newsavebox{\tempsbox} \newlength{\@cparht} \newlength{\@cpardp} \newenvironment{cpar}[6]{% \addtocounter{pardepth}{-#1}% \ifthenelse{\boolean{shading}}{\par\begin{lrbox}{\tempsbox}% \begin{minipage}[t]{\linewidth}}{}% \begin{list}{}{% \edef\temp{\thegmargin} \ifthenelse{\equal{#3}{T}}% {\settowidth{\leftmargin}{\hspace{\temp}\footnotesize #6\hspace{#5pt}}% \addtolength{\leftmargin}{#4pt}}% {\setlength{\leftmargin}{#4pt}% \addtolength{\leftmargin}{#5pt}% \addtolength{\leftmargin}{\temp}% \setlength{\itemindent}{-#5pt}}% \ifthenelse{\equal{#2}{T}}{\addtocounter{pardepth}{1}% \setgmargin{\the\leftmargin}}{}% \setlength{\labelwidth}{0pt}% \setlength{\labelsep}{0pt}% \setlength{\itemindent}{-\leftmargin}% \setlength{\topsep}{0pt}% \setlength{\parsep}{0pt}% \setlength{\partopsep}{0pt}% \setlength{\parskip}{0pt}% \setlength{\itemsep}{0pt} \setlength{\itemindent}{#4pt}% \addtolength{\itemindent}{-\leftmargin}}% \ifthenelse{\equal{#3}{T}}% {\item[\tstrut\footnotesize \hspace{\temp}{#6}\hspace{#5pt}] }% {\item[\tstrut\hspace{\temp}]% }% \footnotesize} {\hspace{-\the\lastskip}\tstrut \end{list}% \ifthenelse{\boolean{shading}}% {\end{minipage}% \end{lrbox}% \ifpcalshading \setlength{\@cparht}{\ht\tempsbox}% \setlength{\@cpardp}{\dp\tempsbox}% \addtolength{\@cparht}{.15em}% \addtolength{\@cpardp}{.2em}% \addtolength{\@cparht}{\@cpardp}% % I don't know what's going on here. I want to add a % \pcalvspace high shaded line, but I don't know how to % do it. A little trial and error shows that the following % does a reasonable job approximating that, eliminating % the line if \pcalvspace is small. \addtolength{\@cparht}{\pcalvspace}% \ifdim \pcalvspace > .8em \addtolength{\pcalvspace}{-.2em}% \hspace*{-\lcomindent}% \shadebox{\rule{0pt}{\pcalvspace}\hspace*{\textwidth}}\par \global\setlength{\pcalvspace}{0pt}% \fi \hspace*{-\lcomindent}% \makebox[0pt][l]{\raisebox{-\@cpardp}[0pt][0pt]{% \shadebox{\rule{0pt}{\@cparht}\hspace*{\textwidth}}}}% \hspace*{\lcomindent}\usebox{\tempsbox}% \par \else \shadebox{\usebox{\tempsbox}}\par \fi}% {}% } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % THE ppar ENVIRONMENT % % ^^^^^^^^^^^^^^^^^^^^ % % The environment % % % % \begin{ppar} ... \end{ppar} % % % % is equivalent to % % % % \begin{cpar}{0}{F}{F}{0}{0}{} ... \end{cpar} % % % % The environment is put around each line of the output for a PlusCal % % algorithm. % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %\newenvironment{ppar}{% % \ifthenelse{\boolean{shading}}{\par\begin{lrbox}{\tempsbox}% % \begin{minipage}[t]{\linewidth}}{}% % \begin{list}{}{% % \edef\temp{\thegmargin} % \setlength{\leftmargin}{0pt}% % \addtolength{\leftmargin}{\temp}% % \setlength{\itemindent}{0pt}% % \setlength{\labelwidth}{0pt}% % \setlength{\labelsep}{0pt}% % \setlength{\itemindent}{-\leftmargin}% % \setlength{\topsep}{0pt}% % \setlength{\parsep}{0pt}% % \setlength{\partopsep}{0pt}% % \setlength{\parskip}{0pt}% % \setlength{\itemsep}{0pt} % \setlength{\itemindent}{0pt}% % \addtolength{\itemindent}{-\leftmargin}}% % \item[\tstrut\hspace{\temp}]}% % {\hspace{-\the\lastskip}\tstrut % \end{list}% % \ifthenelse{\boolean{shading}}{\end{minipage} % \end{lrbox}% % \shadebox{\usebox{\tempsbox}}\par}{}% % } %%% TESTING \newcommand{\xtest}[1]{\par \makebox[0pt][l]{\shadebox{\xtstrut\hspace*{\textwidth}}}% \mbox{$\mbox{}#1\mbox{}$}} % \newcommand{\xxtest}[1]{\par % \makebox[0pt][l]{\shadebox{\xtstrut{#1}\hspace*{\textwidth}}}% % \mbox{$\mbox{}#1\mbox{}$}} %\newlength{\pcalvspace} %\setlength{\pcalvspace}{0pt} % \newlength{\xxtestlen} % \setlength{\xxtestlen}{0pt} % \newcommand\xtstrut% % {\setlength{\xxtestlen}{1.15em}% % \addtolength{\xxtestlen}{\pcalvspace}% % \raisebox{\vshadelen}{\raisebox{-.25em}{\rule{0pt}{\xxtestlen}}}% % \global\setlength{\vshadelen}{0pt}% % \global\setlength{\pcalvspace}{0pt}} %%%% TESTING %% The xcpar environment %% Note: overloaded use of \pcalvspace for testing. %% % \newlength{\xcparht}% % \newlength{\xcpardp}% % \newenvironment{xcpar}[6]{% % \addtocounter{pardepth}{-#1}% % \ifthenelse{\boolean{shading}}{\par\begin{lrbox}{\tempsbox}% % \begin{minipage}[t]{\linewidth}}{}% % \begin{list}{}{% % \edef\temp{\thegmargin}% % \ifthenelse{\equal{#3}{T}}% % {\settowidth{\leftmargin}{\hspace{\temp}\footnotesize #6\hspace{#5pt}}% % \addtolength{\leftmargin}{#4pt}}% % {\setlength{\leftmargin}{#4pt}% % \addtolength{\leftmargin}{#5pt}% % \addtolength{\leftmargin}{\temp}% % \setlength{\itemindent}{-#5pt}}% % \ifthenelse{\equal{#2}{T}}{\addtocounter{pardepth}{1}% % \setgmargin{\the\leftmargin}}{}% % \setlength{\labelwidth}{0pt}% % \setlength{\labelsep}{0pt}% % \setlength{\itemindent}{-\leftmargin}% % \setlength{\topsep}{0pt}% % \setlength{\parsep}{0pt}% % \setlength{\partopsep}{0pt}% % \setlength{\parskip}{0pt}% % \setlength{\itemsep}{0pt}% % \setlength{\itemindent}{#4pt}% % \addtolength{\itemindent}{-\leftmargin}}% % \ifthenelse{\equal{#3}{T}}% % {\item[\xtstrut\footnotesize \hspace{\temp}{#6}\hspace{#5pt}]% % }% % {\item[\xtstrut\hspace{\temp}]% % }% % \footnotesize} % {\hspace{-\the\lastskip}\tstrut % \end{list}% % \ifthenelse{\boolean{shading}}{\end{minipage} % \end{lrbox}% % \setlength{\xcparht}{\ht\tempsbox}% % \setlength{\xcpardp}{\dp\tempsbox}% % \addtolength{\xcparht}{.15em}% % \addtolength{\xcpardp}{.2em}% % \addtolength{\xcparht}{\xcpardp}% % \hspace*{-\lcomindent}% % \makebox[0pt][l]{\raisebox{-\xcpardp}[0pt][0pt]{% % \shadebox{\rule{0pt}{\xcparht}\hspace*{\textwidth}}}}% % \hspace*{\lcomindent}\usebox{\tempsbox}% % \par}{}% % } % % \newlength{\xmcomlen} %\newenvironment{xmcom}[1]{% % \setcounter{pardepth}{0}% % \hspace{.65em}% % \begin{lrbox}{\alignbox}\sloppypar% % \setboolean{shading}{false}% % \setlength{\boxwidth}{#1pt}% % \addtolength{\boxwidth}{-.65em}% % \begin{minipage}[t]{\boxwidth}\footnotesize % \parskip=0pt\relax}% % {\end{minipage}\end{lrbox}% % \setlength{\xmcomlen}{\textwidth}% % \addtolength{\xmcomlen}{-\wd\alignbox}% % \settodepth{\alignwidth}{\usebox{\alignbox}}% % \global\setlength{\multicommentdepth}{\alignwidth}% % \setlength{\boxwidth}{\alignwidth}% % \global\addtolength{\alignwidth}{-\maxdepth}% % \addtolength{\boxwidth}{.1em}% % \raisebox{0pt}[0pt][0pt]{% % \ifthenelse{\boolean{shading}}% % {\hspace*{-\xmcomlen}\shadebox{\rule[-\boxwidth]{0pt}{0pt}% % \hspace*{\xmcomlen}\usebox{\alignbox}}}% % {\usebox{\alignbox}}}% % \vspace*{\alignwidth}\pagebreak[0]\vspace{-\alignwidth}\par} % % a multi-line comment, whose first argument is its width in points. % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % THE lcom ENVIRONMENT % % ^^^^^^^^^^^^^^^^^^^^ % % A multi-line comment with no text to its left is typeset in an lcom % % environment, whose argument is a number representing the indentation % % of the left margin, in points. All the text of the comment should be % % inside cpar environments. % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newenvironment{lcom}[1]{% \setlength{\lcomindent}{#1pt} % Added for PlusCal handling. \par\vspace{.2em}% \sloppypar \setcounter{pardepth}{0}% \footnotesize \begin{list}{}{% \setlength{\leftmargin}{#1pt} \setlength{\labelwidth}{0pt}% \setlength{\labelsep}{0pt}% \setlength{\itemindent}{0pt}% \setlength{\topsep}{0pt}% \setlength{\parsep}{0pt}% \setlength{\partopsep}{0pt}% \setlength{\parskip}{0pt}} \item[]}% {\end{list}\vspace{.3em}\setlength{\lcomindent}{0pt}% } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % THE mcom ENVIRONMENT AND \mutivspace COMMAND % % ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ % % % % A part of the spec containing a right-comment of the form % % % % xxxx (*************) % % yyyy (* ccccccccc *) % % ... (* ccccccccc *) % % (* ccccccccc *) % % (* ccccccccc *) % % (*************) % % % % is typeset by % % % % XXXX \begin{mcom}{d} % % CCCC ... CCC % % \end{mcom} % % YYYY ... % % \multivspace{n} % % % % where the number d is the width in points of the comment, n is the % % number of xxxx, yyyy, ... lines to the left of the comment. % % All the text of the comment should be typeset in cpar environments. % % % % This puts the comment into a single box (so no page breaks can occur % % within it). The entire box is shaded iff the shading flag is true. % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newlength{\xmcomlen}% \newenvironment{mcom}[1]{% \setcounter{pardepth}{0}% \hspace{.65em}% \begin{lrbox}{\alignbox}\sloppypar% \setboolean{shading}{false}% \setlength{\boxwidth}{#1pt}% \addtolength{\boxwidth}{-.65em}% \begin{minipage}[t]{\boxwidth}\footnotesize \parskip=0pt\relax}% {\end{minipage}\end{lrbox}% \setlength{\xmcomlen}{\textwidth}% % For PlusCal shading \addtolength{\xmcomlen}{-\wd\alignbox}% % For PlusCal shading \settodepth{\alignwidth}{\usebox{\alignbox}}% \global\setlength{\multicommentdepth}{\alignwidth}% \setlength{\boxwidth}{\alignwidth}% % For PlusCal shading \global\addtolength{\alignwidth}{-\maxdepth}% \addtolength{\boxwidth}{.1em}% % For PlusCal shading \raisebox{0pt}[0pt][0pt]{% \ifthenelse{\boolean{shading}}% {\ifpcalshading \hspace*{-\xmcomlen}% \shadebox{\rule[-\boxwidth]{0pt}{0pt}\hspace*{\xmcomlen}% \usebox{\alignbox}}% \else \shadebox{\usebox{\alignbox}} \fi }% {\usebox{\alignbox}}}% \vspace*{\alignwidth}\pagebreak[0]\vspace{-\alignwidth}\par} % a multi-line comment, whose first argument is its width in points. % \multispace{n} produces the vertical space indicated by "|"s in % this situation % % xxxx (*************) % xxxx (* ccccccccc *) % | (* ccccccccc *) % | (* ccccccccc *) % | (* ccccccccc *) % | (*************) % % where n is the number of "xxxx" lines. \newcommand{\multivspace}[1]{\addtolength{\multicommentdepth}{-#1\baselineskip}% \addtolength{\multicommentdepth}{1.2em}% \ifthenelse{\lengthtest{\multicommentdepth > 0pt}}% {\par\vspace{\multicommentdepth}\par}{}} %\newenvironment{hpar}[2]{% % \begin{list}{}{\setlength{\leftmargin}{#1pt}% % \addtolength{\leftmargin}{#2pt}% % \setlength{\itemindent}{-#2pt}% % \setlength{\topsep}{0pt}% % \setlength{\parsep}{0pt}% % \setlength{\partopsep}{0pt}% % \setlength{\parskip}{0pt}% % \addtolength{\labelsep}{0pt}}% % \item[]\footnotesize}{\end{list}} % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % Typesets a sequence of paragraphs like this: % % % % % % left |<-- d1 --> XXXXXXXXXXXXXXXXXXXXXXXX % % % margin | <- d2 -> XXXXXXXXXXXXXXX % % % | XXXXXXXXXXXXXXX % % % | % % % | XXXXXXXXXXXXXXX % % % | XXXXXXXXXXXXXXX % % % % % % where d1 = #1pt and d2 = #2pt, but with no vspace between % % % paragraphs. % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Commands for repeated characters that produce dashes. % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % \raisedDash{wd}{ht}{thk} makes a horizontal line wd characters wide, % raised a distance ht ex's above the baseline, with a thickness of % thk em's. \newcommand{\raisedDash}[3]{\raisebox{#2ex}{\setlength{\alignwidth}{.5em}% \rule{#1\alignwidth}{#3em}}} % The following commands take a single argument n and produce the % output for n repeated characters, as follows % \cdash: - % \tdash: ~ % \ceqdash: = % \usdash: _ \newcommand{\cdash}[1]{\raisedDash{#1}{.5}{.04}} \newcommand{\usdash}[1]{\raisedDash{#1}{0}{.04}} \newcommand{\ceqdash}[1]{\raisedDash{#1}{.5}{.08}} \newcommand{\tdash}[1]{\raisedDash{#1}{1}{.08}} \newlength{\spacewidth} \setlength{\spacewidth}{.2em} \newcommand{\e}[1]{\hspace{#1\spacewidth}} %% \e{i} produces space corresponding to i input spaces. %% Alignment-file Commands \newlength{\alignboxwidth} \newlength{\alignwidth} \newsavebox{\alignbox} % \al{i}{j}{txt} is used in the alignment file to put "%{i}{j}{wd}" % in the log file, where wd is the width of the line up to that point, % and txt is the following text. \newcommand{\al}[3]{% \typeout{\%{#1}{#2}{\the\alignwidth}}% \cl{#3}} %% \cl{txt} continues a specification line in the alignment file %% with text txt. \newcommand{\cl}[1]{% \savebox{\alignbox}{\mbox{$\mbox{}#1\mbox{}$}}% \settowidth{\alignboxwidth}{\usebox{\alignbox}}% \addtolength{\alignwidth}{\alignboxwidth}% \usebox{\alignbox}} % \fl{txt} in the alignment file begins a specification line that % starts with the text txt. \newcommand{\fl}[1]{% \par \savebox{\alignbox}{\mbox{$\mbox{}#1\mbox{}$}}% \settowidth{\alignwidth}{\usebox{\alignbox}}% \usebox{\alignbox}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Ordinarily, TeX typesets letters in math mode in a special math italic % % font. This makes it typeset "it" to look like the product of the % % variables i and t, rather than like the word "it". The following % % commands tell TeX to use an ordinary italic font instead. % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \ifx\documentclass\undefined \else \DeclareSymbolFont{tlaitalics}{\encodingdefault}{cmr}{m}{it} \let\itfam\symtlaitalics \fi \makeatletter \newcommand{\tlx@c}{\c@tlx@ctr\advance\c@tlx@ctr\@ne} \newcounter{tlx@ctr} \c@tlx@ctr=\itfam \multiply\c@tlx@ctr"100\relax \advance\c@tlx@ctr "7061\relax \mathcode`a=\tlx@c \mathcode`b=\tlx@c \mathcode`c=\tlx@c \mathcode`d=\tlx@c \mathcode`e=\tlx@c \mathcode`f=\tlx@c \mathcode`g=\tlx@c \mathcode`h=\tlx@c \mathcode`i=\tlx@c \mathcode`j=\tlx@c \mathcode`k=\tlx@c \mathcode`l=\tlx@c \mathcode`m=\tlx@c \mathcode`n=\tlx@c \mathcode`o=\tlx@c \mathcode`p=\tlx@c \mathcode`q=\tlx@c \mathcode`r=\tlx@c \mathcode`s=\tlx@c \mathcode`t=\tlx@c \mathcode`u=\tlx@c \mathcode`v=\tlx@c \mathcode`w=\tlx@c \mathcode`x=\tlx@c \mathcode`y=\tlx@c \mathcode`z=\tlx@c \c@tlx@ctr=\itfam \multiply\c@tlx@ctr"100\relax \advance\c@tlx@ctr "7041\relax \mathcode`A=\tlx@c \mathcode`B=\tlx@c \mathcode`C=\tlx@c \mathcode`D=\tlx@c \mathcode`E=\tlx@c \mathcode`F=\tlx@c \mathcode`G=\tlx@c \mathcode`H=\tlx@c \mathcode`I=\tlx@c \mathcode`J=\tlx@c \mathcode`K=\tlx@c \mathcode`L=\tlx@c \mathcode`M=\tlx@c \mathcode`N=\tlx@c \mathcode`O=\tlx@c \mathcode`P=\tlx@c \mathcode`Q=\tlx@c \mathcode`R=\tlx@c \mathcode`S=\tlx@c \mathcode`T=\tlx@c \mathcode`U=\tlx@c \mathcode`V=\tlx@c \mathcode`W=\tlx@c \mathcode`X=\tlx@c \mathcode`Y=\tlx@c \mathcode`Z=\tlx@c \makeatother %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % THE describe ENVIRONMENT % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % It is like the description environment except it takes an argument % ARG that should be the text of the widest label. It adjusts the % indentation so each item with label LABEL produces %% LABEL blah blah blah %% <- width of ARG ->blah blah blah %% blah blah blah \newenvironment{describe}[1]% {\begin{list}{}{\settowidth{\labelwidth}{#1}% \setlength{\labelsep}{.5em}% \setlength{\leftmargin}{\labelwidth}% \addtolength{\leftmargin}{\labelsep}% \addtolength{\leftmargin}{\parindent}% \def\makelabel##1{\rm ##1\hfill}}% \setlength{\topsep}{0pt}}%% % Sets \topsep to 0 to reduce vertical space above % and below embedded displayed equations {\end{list}} % For tlatex.TeX \usepackage{verbatim} \makeatletter \def\tla{\let\%\relax% \@bsphack \typeout{\%{\the\linewidth}}% \let\do\@makeother\dospecials\catcode`\^^M\active \let\verbatim@startline\relax \let\verbatim@addtoline\@gobble \let\verbatim@processline\relax \let\verbatim@finish\relax \verbatim@} \let\endtla=\@esphack \let\pcal=\tla \let\endpcal=\endtla \let\ppcal=\tla \let\endppcal=\endtla % The tlatex environment is used by TLATeX.TeX to typeset TLA+. % TLATeX.TLA starts its files by writing a \tlatex command. This % command/environment sets \parindent to 0 and defines \% to its % standard definition because the writing of the log files is messed up % if \% is defined to be something else. It also executes % \@computerule to determine the dimensions for the TLA horizonatl % bars. \newenvironment{tlatex}{\@computerule% \setlength{\parindent}{0pt}% \makeatletter\chardef\%=`\%}{} % The notla environment produces no output. You can turn a % tla environment to a notla environment to prevent tlatex.TeX from % re-formatting the environment. \def\notla{\let\%\relax% \@bsphack \let\do\@makeother\dospecials\catcode`\^^M\active \let\verbatim@startline\relax \let\verbatim@addtoline\@gobble \let\verbatim@processline\relax \let\verbatim@finish\relax \verbatim@} \let\endnotla=\@esphack \let\nopcal=\notla \let\endnopcal=\endnotla \let\noppcal=\notla \let\endnoppcal=\endnotla %%%%%%%%%%%%%%%%%%%%%%%% end of tlatex.sty file %%%%%%%%%%%%%%%%%%%%%%% % last modified on Fri 3 August 2012 at 14:23:49 PST by lamport
latex/sty.txt · Last modified: 2019/09/02 16:50 by jonathan
