13.1 介绍

TLATeX 使用 LaTeX 作为排版引擎由 tla 文件输出 PDF 等更易读的文件。TLATeX 提供了显示行号、传递 LaTeX 命令等功能，详见文档。

13.2 注释阴影化

TLATeX 可以控制注释区域的阴影深度，或者结合其他工具调整阴影。

13.3 对规范进行排版

规范的排版不会破坏跨行对齐。符号之间不使用空格与使用一个空格的排版相同。排版会将模块前后的文字一同处理，这种特性也可以被屏蔽。排版会检查部分词法错误。

13.4 对注释进行排版

TLATeX 会区分单行注释与多行注释。多行注释有如下三种写法：

(**************)  \*************  (* This
(* This is    *)  \* This is         is a
(* a comment. *)  \* a comment.      comment. *)
(**************)  \************* 

其中前两种需要注意对齐。

多行注释的排版会自动检测段落、表格等多种情况进行折行，但不会进行跨行对齐。

注释的一些语法：

`这部分注释应用规范的样式（包括规范中的字符串样式）'
`^这部分注释应用注释的样式，交给 LaTeX 进行排版^'
`.这部分注释不进行排版，以 ASCII 形式输出.'
``本行首末是左右引号''
`~这部分注释不会显示~'

13.5 调整输出格式

TLATeX 可以调整字号、文字高度宽度、偏移量。

13.6 输出文件

TLATeX 可以配置输出文件的文件名、ASCII 版本的输出、LaTeX 样式。

13.7 故障诊断

TLATeX 会依次产生一些中间文件，并最终输出 PDF 等阅读文件。命令行输出和中间文件日志有助于定位问题。

13.8 使用 LaTeX 命令

通过

`^这部分注释应用注释的样式，交给 LaTeX 进行排版^'

这种方式使用 LaTeX 进行排版。由于 LaTeX 代码的可读性差，因此推荐使用如下方式同时维护一份 ASCII 可读的注释

\*************************************
\* `^ \begin{describe}{gnat:}
\*     \item[gnat:] A tiny insect.
\*     \item[gnu:]  A short word.
\*    \end{describe} ^'
\* `~ gnat: A tiny insect.
\*
\*    gnu:  A short word. ~'
\*************************************