Software Engineering Documentation

User Tools

Site Tools

You are here: start » tla » latex
tla:latex

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision 		Previous revision
tla:latex [2019/09/02 16:48]
jonathan 		tla:latex [2019/09/02 17:00] (current)
jonathan [More Documentation]
Line 26: Line 26:
  
 <​code>​ <​code>​
-tla2tex ​model.tex ​+tlaintex ​model.tex ​
 </​code>​ </​code>​
  
Line 46: Line 46:
 \end{document} \end{document}
 </​code>​ </​code>​
 +
 +The style file ''​tlatex.sty''​ must be available. The above produces a LaTeX file ''​model.tex''​ where the tla environment is set to mathematics. The original''​ model.tex''​ file is renamed ''​model.old''​.
  
 ==== Style file ==== ==== Style file ====
  
-The style file ''​tlatex.sty''​ is available [:latex:sty\here]+The style file ''​tlatex.sty''​ is available ​[[:latex:sty|here]].
  
-<code latex> +==== More Documentation ==== 
-\usepackage{latexsym} +If you are not using the JAR file, you will probably run TLATeX by typing ​
-\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. +   ​java ​tla2tex.TeX [options] fileName
-% 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{\,​\,​\} }}+
  
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +where [options] is an optional list of options, ​and ''​fileName''​ is the 
-% REDEFINE STANDARD COMMANDS TO MAKE THEM FORMAT BETTER % +name of the input file.  (If ''​fileName''​ does not contain an extension, 
-%                                                       % +then the input file is ''​fileName.tex''​.)  Running TLATeX with the -help 
-% We redefine \in and \notin ​                           % +option produces a list of all options.  ​Running it with the -info 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +option produces what you are now reading.  (The fileName can be 
-\renewcommand{\_}{\rule{.4em}{.06em}\hspace{.05em}} +omitted when using the -help or -info option.)
-\newlength{\equalswidth} +
-\let\oldin=\in +
-\let\oldnotin=\notin +
-\renewcommand{\in}{% +
-   ​{\settowidth{\equalswidth}{$\.{=}$}\makebox[\equalswidth][c]{$\oldin$}}} +
-\renewcommand{\notin}{% +
-   ​{\settowidth{\equalswidth}{$\.{=}$}\makebox[\equalswidth]{$\oldnotin$}}}+
  
 +The running time of tla2tex.TeX is roughly proportional to the number
 +of separate `tla' environments. ​ You can speed things up by not
 +having tla2tex.TeX reprocess `tla' environments that haven'​t changed
 +since the last time it was run.  To do this, just change those
 +`tla' environments to `notla'​ environments. ​ Similarly, you can change
 +`pcal' and `ppcal'​ to `nopcal'​ or `noppcal'​ environments.
  
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +Read [[https://lamport.azurewebsites.net/​tla/​texinfo.txt|here]] for more. 
-%                                                  % +
-% 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 +
- +
-</​code>​+
tla/latex.1567442923.txt.gz · Last modified: 2019/09/02 16:48 by jonathan

Page Tools

Donate Powered by PHP Valid HTML5 Valid CSS Driven by DokuWiki