1 2;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 3;; 4;; MODULE : latex-command-drd.scm 5;; DESCRIPTION : Formal specification of standard LaTeX commands 6;; COPYRIGHT : (C) 1999 Joris van der Hoeven 7;; 8;; This software falls under the GNU general public license version 3 or later. 9;; It comes WITHOUT ANY WARRANTY WHATSOEVER. For details, see the file LICENSE 10;; in the root directory or <http://www.gnu.org/licenses/gpl-3.0.html>. 11;; 12;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 13 14(texmacs-module (convert latex latex-command-drd)) 15 16;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 17;; Any LaTeX tag 18;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 19 20(logic-rules 21 ((latex-tag% 'x) (latex-arity% 'x 'y)) 22 ((latex-supports-option% 'x #t) (latex-optional-arg% 'x))) 23 24;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 25;; LaTeX commands 26;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 27 28(logic-group latex-command-0% 29 ,(string->symbol " ") ,(string->symbol ";") 30 ,(string->symbol ",") ,(string->symbol ":") 31 - / [ ] ! * ,(string->symbol "|") i j ss SS oe OE ae AE 32 AA DH L NG O S TH aa dh dj l ng o P th pounds colon and lq rq 33 quad qquad enspace thinspace par smallskip medskip bigskip 34 noindent newline linebreak nobreak nolinebreak strut 35 pagebreak nopagebreak newpage newdoublepage clearpage cleardoublepage 36 newblock bgroup egroup protect cr hfil hfill hfilll appendix limits nolimits 37 dots maketitle tableofcontents TeX LaTeX onecolumn twocolumn 38 begingroup endgroup printindex today bmod toprule midrule bottomrule 39 40 ;; AMS commands 41 dotsc dotsb dotsm dotsi dotso qed 42 ;; temporarily 43 hline hrulefill 44 ;; rewritten 45 notin vert Vert addots 46 implies iff gets 47 ;; wikipedia 48 infin rang 49 ;; bibtex 50 bysame 51 52 ;; Algorithms 53 AND BlankLine Ensure ENSURE FALSE GLOBALS NOT OR PRINT Require REQUIRE RETURN 54 State STATE TO KwTo TRUE XOR Else ENDBODY EndFor ENDFOR EndFunction EndIf 55 ENDIF ENDINPUTS EndLoop ENDLOOP ENDOUTPUTS EndProcedure ENDWHILE EndWhile 56 Loop) 57 58(logic-group latex-command-1% 59 part* chapter* section* subsection* subsubsection* paragraph* subparagraph* 60 nextbib geometry 61 footnote overline underline <sub> <sup> not left middle right 62 big Big bigg Bigg bigl Bigl biggl Biggl 63 bigm Bigm biggm Biggm bigr Bigr biggr Biggr 64 bar Bar hat Hat tilde Tilde widehat widetilde vec Vec bm 65 grave Grave acute Acute check Check breve Breve invbreve abovering mathring 66 dot Dot ddot Ddot dddot ddddot mod pod pmod 67 label ref pageref index hspace hspace* vspace vspace* 68 mbox hbox textnormal text not substack 69 ,(string->symbol "'") ,(string->symbol "`") ,(string->symbol "\"") 70 ^ over atop choose ~ = u v H t c d b k r textsuperscript textsubscript 71 thispagestyle ensuremath 72 mathord mathbin mathopen mathpunct mathop mathrel mathclose mathalpha 73 arabic alph Alph roman Roman fnsymbol displaylines cases underbrace overbrace 74 phantom hphantom vphantom smash date terms 75 newcounter stepcounter refstepcounter value 76 citealt citealt* citealp* 77 citetext citeauthor citeauthor* citeyear onlinecite 78 epsfig url penalty centerline fbox framebox cline cmidrule 79 enlargethispage 80 newlength newdimen newskip 81 Comment COMMENT For ForAll If Input KwData KwResult KwRet lnl nllabel 82 lElse uElse Output Repeat Until UNTIL While 83 etalchar MR listpart) 84 85(logic-group latex-command-1% ;; . needs a special treatment 86 ,(string->symbol ".")) 87 88(logic-group latex-command-2% 89 binom tbinom dbinom cfrac tfrac equal href 90 sideset stackrel citeauthoryear 91 setcounter addtocounter setlength addtolength 92 colorbox scalebox texorpdfstring raisebox foreignlanguage 93 Call Function Procedure SetKw SetKwData SetKwFunction SetKwInOut 94 ifthispageodd) 95 96(logic-group latex-command-3% 97 ifthenelse resizebox fcolorbox @setfontsize eIf multicolumn) 98 99(logic-group latex-command-4% 100 mathchoice) 101 102(logic-group latex-command-6% 103 genfrac @startsection) 104 105(logic-rules 106 ((latex-command% 'x) (latex-command-0% 'x)) 107 ((latex-arity% 'x 0) (latex-command-0% 'x)) 108 ((latex-command% 'x) (latex-command-1% 'x)) 109 ((latex-arity% 'x 1) (latex-command-1% 'x)) 110 ((latex-command% 'x) (latex-command-2% 'x)) 111 ((latex-arity% 'x 2) (latex-command-2% 'x)) 112 ((latex-command% 'x) (latex-command-3% 'x)) 113 ((latex-arity% 'x 3) (latex-command-3% 'x)) 114 ((latex-command% 'x) (latex-command-4% 'x)) 115 ((latex-arity% 'x 4) (latex-command-4% 'x)) 116 ((latex-command% 'x) (latex-command-6% 'x)) 117 ((latex-arity% 'x 6) (latex-command-6% 'x))) 118 119;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 120;; LaTeX commands with optional arguments 121;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 122 123(logic-group latex-command-0*% 124 item ,(string->symbol "\\") 125 BODY ELSE INPUTS LOOP OUTPUTS REPEAT) 126 127(logic-group latex-command-1*% 128 usepackage documentclass documentstyle sqrt bibitem cite caption 129 title author thanks marginpar 130 part chapter section subsection subsubsection paragraph subparagraph 131 includegraphics includegraphics* 132 subjclass declaretheorem footnotetext 133 xleftarrow xrightarrow xleftrightarrow xminus 134 xLeftarrow xRightarrow xLeftrightarrow xequal 135 xmapsto xmapsfrom citealp citet citep citet* citep* 136 Begin ELSIF FORALL FOR IF WHILE tcp tcp* tcc tcc*) 137 138(logic-group latex-command-2*% 139 def newcommand renewcommand newtheorem newtheorem* frac parbox 140 ElseIf uElseIf lElseIf ForEach lForEach lForAll lFor) 141 142(logic-group latex-command-3*% 143 category newenvironment renewenvironment multirow) 144 145(logic-rules 146 ((latex-command-0% 'x) (latex-command-0*% 'x)) 147 ((latex-optional-arg% 'x) (latex-command-0*% 'x)) 148 ((latex-command-1% 'x) (latex-command-1*% 'x)) 149 ((latex-optional-arg% 'x) (latex-command-1*% 'x)) 150 ((latex-command-2% 'x) (latex-command-2*% 'x)) 151 ((latex-optional-arg% 'x) (latex-command-2*% 'x)) 152 ((latex-command-3% 'x) (latex-command-3*% 'x)) 153 ((latex-optional-arg% 'x) (latex-command-3*% 'x))) 154 155;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 156;; Environments 157;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 158 159(logic-group latex-environment-0% 160 begin-document begin-abstract begin-verbatim begin-proof 161 begin-matrix begin-pmatrix begin-bmatrix begin-vmatrix begin-smallmatrix 162 begin-cases 163 begin-center begin-flushleft begin-flushright 164 begin-picture) 165 166(logic-group latex-environment-0*% 167 begin-figure begin-table begin-figure* begin-table* 168 begin-algorithmic begin-algorithm begin-algorithm2e) 169 170(logic-group latex-environment-1% 171 begin-otherlanguage begin-otherlanguage* 172 begin-tabbing begin-thebibliography begin-multicols) 173 174(logic-group latex-environment-1*% 175 begin-array begin-tabular begin-minipage) 176 177(logic-group latex-environment-2*% 178 begin-tabular* begin-tabularx) 179 180(logic-rules 181 ((latex-environment% 'x) (latex-environment-0% 'x)) 182 ((latex-arity% 'x 0) (latex-environment-0% 'x)) 183 ((latex-environment% 'x) (latex-environment-1% 'x)) 184 ((latex-arity% 'x 1) (latex-environment-1% 'x)) 185 ((latex-environment% 'x) (latex-environment-2% 'x)) 186 ((latex-arity% 'x 2) (latex-environment-2% 'x)) 187 ((latex-environment% 'x) (latex-environment-3% 'x)) 188 ((latex-arity% 'x 3) (latex-environment-3% 'x)) 189 ((latex-environment-0% 'x) (latex-environment-0*% 'x)) 190 ((latex-optional-arg% 'x) (latex-environment-0*% 'x)) 191 ((latex-environment-1% 'x) (latex-environment-1*% 'x)) 192 ((latex-optional-arg% 'x) (latex-environment-1*% 'x)) 193 ((latex-environment-2% 'x) (latex-environment-2*% 'x)) 194 ((latex-optional-arg% 'x) (latex-environment-2*% 'x))) 195 196;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 197;; Enunciations 198;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 199 200(logic-group latex-enunciation% 201 begin-theorem begin-proposition begin-lemma begin-corollary begin-proof 202 begin-axiom begin-definition begin-notation begin-conjecture begin-remark 203 begin-note begin-example begin-exercise begin-problem begin-warning 204 begin-convention begin-quote-begin-env begin-quotation begin-verse 205 begin-solution begin-question begin-answer begin-acknowledgments) 206 207(logic-rules 208 ((latex-environment-0*% 'x) (latex-enunciation% 'x))) 209 210;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 211;; Modifiers 212;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 213 214(logic-group latex-modifier-0% 215 normalfont rm tt sf md bf it em sl sc rmfamily ttfamily sffamily 216 mdseries bfseries upshape itshape slshape scshape 217 displaystyle textstyle scriptstyle scriptscriptstyle cal frak Bbb boldmath 218 tiny scriptsize footnotesize small normalsize 219 large Large LARGE huge Huge 220 black white grey red blue yellow green orange magenta brown pink 221 centering raggedleft raggedright flushleft flushright) 222 223(logic-group latex-modifier-1% 224 textnormalfont 225 textrm texttt textsf textmd textbf textup textit textsl textsc emph 226 mathrm mathtt mathsf mathmd mathbf mathup mathit mathsl mathnormal 227 mathcal mathfrak mathbb mathbbm mathscr operatorname boldsymbol 228 lowercase MakeLowercase uppercase MakeUppercase selectlanguage) 229 230(logic-group latex-modifier-1*% 231 color) 232 233(logic-group latex-modifier-2*% 234 textcolor) 235 236(logic-rules 237 ((latex-modifier% 'x) (latex-modifier-0% 'x)) 238 ((latex-arity% 'x 0) (latex-modifier-0% 'x)) 239 ((latex-modifier% 'x) (latex-modifier-1% 'x)) 240 ((latex-arity% 'x 1) (latex-modifier-1% 'x)) 241 ((latex-optional-arg% 'x) (latex-modifier-1*% 'x)) 242 ((latex-modifier% 'x) (latex-modifier-1*% 'x)) 243 ((latex-arity% 'x 1) (latex-modifier-1*% 'x)) 244 ((latex-optional-arg% 'x) (latex-modifier-2*% 'x)) 245 ((latex-modifier% 'x) (latex-modifier-2*% 'x)) 246 ((latex-arity% 'x 2) (latex-modifier-2*% 'x))) 247 248;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 249;; Special types of LaTeX primitives 250;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 251 252(logic-group latex-control% 253 $ & % ,(string->symbol "#") _ { } <less> <gtr>) 254 255(logic-group latex-operator% 256 arccos arcsin arctan arg cos cosh cot coth csc deg det dim exp gcd hom 257 inf ker lg lim liminf limsup ln log max min Pr sec sin sinh sup tan tanh) 258 259(logic-group latex-list% 260 begin-itemize begin-enumerate begin-description 261 begin-asparaitem begin-inparaitem begin-compactitem 262 begin-asparaenum begin-inparaenum begin-compactenum) 263 264(logic-group latex-math-environment-0% 265 begin-formula begin-equation* 266 begin-math begin-displaymath begin-equation 267 begin-eqnarray begin-eqnarray* 268 begin-flalign begin-flalign* 269 begin-align begin-align* 270 begin-multline begin-multline* 271 begin-gather begin-gather* 272 begin-eqsplit begin-eqsplit*) 273 274(logic-group latex-math-environment-1% 275 begin-alignat begin-alignat*) 276 277(logic-rules 278 ((latex-arity% 'x 0) (latex-control% 'x)) 279 ((latex-arity% 'x 0) (latex-operator% 'x)) 280 ((latex-environment-0*% 'x) (latex-list% 'x)) 281 ((latex-math-environment% 'x) (latex-math-environment-0% 'x)) 282 ((latex-math-environment% 'x) (latex-math-environment-1% 'x)) 283 ((latex-environment-1% 'x) (latex-math-environment-1% 'x)) 284 ((latex-environment-0% 'x) (latex-math-environment-0% 'x))) 285 286;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 287;; Counters 288;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 289 290(logic-group latex-counter% 291 badness enumi enumii enumiii enumiv equation figure inputlineno 292 mpfootnote page setlanguage table) 293 294(logic-rules 295 ((latex-arity% 'x 0) (latex-counter% 'x))) 296 297;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 298;; Names 299;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 300 301(logic-group latex-name% 302 abstractname appendixname contentname figurename indexname 303 litfigurename littablename partname refname tablename) 304 305(logic-rules 306 ((latex-arity% 'x 0) (latex-name% 'x))) 307 308;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 309;; Lengths 310;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 311 312(logic-group latex-length% 313 ;; From latex.ltx 314 ;; -- lengths 315 @textfloatsheight arraycolsep arrayrulewidth columnsep columnseprule 316 columnwidth doublerulesep emergencystretch evensidemargin fboxrule 317 fboxsep footnotesep footskip headheight headsep itemindent labelsep 318 labelwidth leftmargin leftmargini leftmarginii leftmarginiii 319 leftmarginiv leftmarginv leftmarginvi linewidth listparindent 320 marginparpush marginparsep marginparwidth oddsidemargin p@ paperheight 321 paperwidth rightmargin tabbingsep tabcolsep textheight textwidth 322 topmargin unitlength z@ @bls @vpt @vipt @viipt @viiipt @ixpt @xpt @xipt 323 @xiipt @xivpt @xviipt @xxpt @xxvpt 324 ;; -- skips 325 topsep partopsep itemsep parsep floatsep textfloatsep intextsep 326 dblfloatsep dbltextfloatsep 327 ;; From latex classes 328 abovecaptionskip belowcaptionskip bibindent 329 ;; From fleqn 330 mathindent 331 ;; Plain TeX 332 maxdimen hfuzz vfuzz overfullrule hsize vsize maxdepth lineskiplimit 333 delimitershortfall nulldelimiterspace scriptspace mathsurround 334 predisplaysize displaywidth displayindent parindent hangindent hoffset 335 voffset baselineskip lineskip parskip abovedisplayskip 336 abovedisplayshortskip belowdisplayskip belowdisplayshortskip leftskip 337 rightskip topskip splittopskip tabskip spaceskip xspaceskip parfillskip 338 thinmuskip medmuskip thickmuskip hideskip smallskipamount medskipamount 339 bigskipamount normalbaselineskip normallineskip normallineskiplimit jot 340 ) 341 342(logic-rules 343 ((latex-arity% 'x 0) (latex-length% 'x))) 344 345;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 346;; To be imported as pictures 347;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 348 349(logic-group latex-as-pic-0% 350 begin-pspicture begin-pspicture* begin-tikzpicture) 351 352(logic-group latex-as-pic-1% 353 xymatrix) 354 355(logic-rules 356 ((latex-as-pic% 'x) (latex-as-pic-0% 'x)) 357 ((latex-as-pic% 'x) (latex-as-pic-1% 'x)) 358 ((latex-arity% 'x 0) (latex-as-pic-0% 'x)) 359 ((latex-arity% 'x 1) (latex-as-pic-1% 'x))) 360 361;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 362;; To be ignored 363;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 364 365(logic-group latex-ignore-0% 366 allowbreak notag xspace break sloppy makeatother makeatletter relax 367 qedhere 368 ignorespacesafterend ignorespaces balancecolumns) 369 370(logic-group latex-ignore-0*% 371 displaybreak allowdisplaybreaks) 372 373(logic-group latex-ignore-1% 374 tag hyphenation) 375 376(logic-group latex-ignore-2% 377 newdir) 378 379(logic-rules 380 ((latex-ignore% 'x) (latex-ignore-0% 'x)) 381 ((latex-ignore% 'x) (latex-ignore-0*% 'x)) 382 ((latex-ignore% 'x) (latex-ignore-1% 'x)) 383 ((latex-ignore% 'x) (latex-ignore-2% 'x)) 384 ((latex-arity% 'x 0) (latex-ignore-0% 'x)) 385 ((latex-arity% 'x 0) (latex-ignore-0*% 'x)) 386 ((latex-arity% 'x 1) (latex-ignore-1% 'x)) 387 ((latex-arity% 'x 2) (latex-ignore-2% 'x)) 388 ((latex-optional-arg% 'x) (latex-ignore-1*% 'x))) 389