summaryrefslogtreecommitdiff
path: root/support/splint/tex/yytexlex.sty
diff options
context:
space:
mode:
authorNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
committerNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
commite0c6872cf40896c7be36b11dcc744620f10adf1d (patch)
tree60335e10d2f4354b0674ec22d7b53f0f8abee672 /support/splint/tex/yytexlex.sty
Initial commit
Diffstat (limited to 'support/splint/tex/yytexlex.sty')
-rw-r--r--support/splint/tex/yytexlex.sty1145
1 files changed, 1145 insertions, 0 deletions
diff --git a/support/splint/tex/yytexlex.sty b/support/splint/tex/yytexlex.sty
new file mode 100644
index 0000000000..a7e7dc3250
--- /dev/null
+++ b/support/splint/tex/yytexlex.sty
@@ -0,0 +1,1145 @@
+% Copyright 2012-2015, Alexander Shibakov
+% This file is part of SPLinT
+%
+% SPLinT is free software: you can redistribute it and/or modify
+% it under the terms of the GNU General Public License as published by
+% the Free Software Foundation, either version 3 of the License, or
+% (at your option) any later version.
+%
+% SPLinT is distributed in the hope that it will be useful,
+% but WITHOUT ANY WARRANTY; without even the implied warranty of
+% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+% GNU General Public License for more details.
+%
+% You should have received a copy of the GNU General Public License
+% along with SPLinT. If not, see <http://www.gnu.org/licenses/>.
+
+% parsing \TeX\ input for pretty-printing;
+% scanning and parsing are both done by using a low-level
+% finite automaton;
+
+\def\yygetchar{% single buffered input
+ \ifyytextbackup
+ \yybyte\yytextseen
+ \yycp@\yytextseenlastchar
+ \yytextbackupfalse
+ \let\next\yyreturn
+ \else
+ \let\next\yyinput
+ \fi
+ \next
+}
+
+% \TeX\ input
+
+\def\texdefaultstate{%
+<>+-()^~!?*[]:.,`'\%\$\_
+\raw digit letter \raw
+{%
+ \putother\yycp@\in\yybyte
+ \appendyybyte}
+=
+{%
+ \appendr\texlinetoks{{}${}={}${}}%
+ \yygetchar
+}
+\{
+{%
+ \putother\yycp@\in\yybyte
+ \appendl\yybyte{\noexpand\bbal[\the\bbalance]}%
+ \advance\bbalance1\relax
+ \appendyybyte}
+\}
+{%
+ \putother\yycp@\in\yybyte
+ \advance\bbalance-1\relax
+ \appendl\yybyte{\noexpand\bbal[\the\bbalance]}%
+ \appendyybyte}
+0123456789
+{%
+ \expandafter\ifcat\expandafter\noexpand\the\yybyte1%
+ \def\next{digit}%
+ \else
+ \def\next{^^A}%
+ \fi
+ \action\next\in\texdefaultstate
+}
+^^A % \yycp@==1
+{%
+ \edef\next{\noexpand\noexpand\the\yybyte}%
+ \action\next\in\texdefaultstate}
+\raw\hbox\raw
+{%
+ \appendnext}
+\raw\end\raw
+{%
+ \relax}
+\raw\\ \_ \raw
+{%
+ \appendyybyte}
+\ \
+{%
+ \appendyybyte}
+\\
+{%
+ \getcescape
+}
+/
+\raw escape \raw
+{%
+ \let\currentstate\texcsname
+ \yygetchar}
+}%
+
+\def\texcsname{%
+<>+-()^~!?*\{\}[]:.,`'=\%\$\_/
+0123456789
+^^A
+\ \
+\raw \end \\ \_ \ \raw
+\raw escape \raw
+{%
+ \let\currentstate\texdefaultstate
+ \putother\yycp@\in\yytext
+ \outputtexcs
+ \yygetchar}
+%
+\\
+{%
+ \getcescape
+}
+\raw letter \raw
+{%
+ \let\currentstate\texcsnamelong
+ \yytext\yybyte
+ \yygetchar}
+}%
+
+\def\texcsnamelong{%
+<>+-()^~!?*\{\}[]:.,`'=\%\$\_\&
+0123456789
+^^A
+\ \
+\raw \end \\ \_ \raw
+{%
+ \let\currentstate\texdefaultstate
+ \yytextseenlastchar=\yycp@
+ \yytextseen=\yybyte
+ \yytextbackuptrue
+ \outputtexcs
+ \yygetchar}
+\\
+{%
+ \getcescape
+}
+/
+\raw escape \raw
+{%
+ \let\currentstate\texcsname
+ \outputtexcs
+ \yygetchar}
+\raw letter \raw
+{%
+ \concat\yytext\yybyte
+ \yygetchar}
+}%
+
+\def\texcescape{%
+\\
+{%
+ \let\currentstate\esccurrentstate
+ \yycp@=`\\%
+ \putother\yycp@\in\yybyte
+ \def\next{escape}%
+ \action\next\in\currentstate}
+}
+
+\def\texescdefault{%
+ \let\currentstate\esccurrentstate
+ \yycp@=`\ %
+ \yybyte{\ }%
+ \action\yycp@\in\currentstate
+}
+
+\def\getcescape{%
+ \let\esccurrentstate\currentstate
+ \let\currentstate\texcescape
+ \let\default\texescdefault
+ \yygetchar
+}
+
+\setspecialcharsfrom\texdefaultstate
+\setspecialcharsfrom\texcsname
+\setspecialcharsfrom\texcsnamelong
+\setspecialcharsfrom\texcescape
+
+\newtoks\texlinetoks % parsed \TeX\ tokens
+\newtoks\texidxtoks % indexing commands
+
+\def\texlexer{%
+ \let\default\yygetchar
+ \let\next\yycp@
+ \ifnum\yycp@>"20 %
+ \ifnum\yycp@<"7F % a character
+ \expandafter\ifcat\expandafter\noexpand\the\yybyte a%
+ % this test allows one some control over what constitutes a control
+ % sequence name (by saying, for example, \let\$a or manipulating \catcodes)
+ % this is bordering on a bug
+ \def\next{letter}%
+ \fi
+ \fi
+ \fi
+ \action\next\in\currentstate
+}
+
+\def\outputtexcs{%
+ \expandafter\ifx\csname\the\yytext\defTpostfix\endcsname\relax
+ \putother{`\\}\in\toksa
+ \concat\texlinetoks\toksa
+ \concat\texlinetoks\yytext
+ \appendr\texlinetoks{\noexpand\hbox{$\noexpand\,$}}%
+ \else
+ \appendr\texlinetoks{\expandafter\expandafter\expandafter\noexpand\expandafter\csname\the\yytext xTeXmode\endcsname}%
+ \fi
+ \appendr\texidxtoks{%
+ \termindex{{\nx\nx\nx\texcsstring{\expandafter\charstonumberse\the\yytext\end}}{\texnspace}{\nx\the\pageno}{\secno}}%
+ }%
+}
+
+% the `calling conventions' for indexing \TeX\ control sequences are too different to use canned indexing macros
+% (the second parameter is a register so it has to be expanded before the \charstonumberse processes it)
+% we therefore invoke the macros by hand
+
+\def\texidxdomain{T}
+
+\def\texcsidxrank{2}
+
+\def\writetexidxentry#1{\iftermindex\write\gindex{\nx\nx\expandafter\nx\csname\texidxdomain TI\endcsname\texcsidxrank#1}\fi}
+
+\def\appendyybyte{\concat\texlinetoks\yybyte\yygetchar}
+\def\appendnext#1{\toksa{#1}\concat\texlinetoks\toksa\yygetchar}
+
+\def\defTpostfix{xTeXmode}
+
+\def\stripyybyte{%
+ \expandafter\stripyyb@te\the\yybyte
+}
+
+\def\stripyyb@te#1#2{\noexpand#2}
+
+% TODO:
+% the macros below are in their present shape due to the forces of `historical evolution':
+% \TeX\ pretty printing needs to be completely rewritten, however, the existing macros
+% do a passable job so they remain in this rather random shape.
+% the items below need more urgent attention:
+%
+% o introduce TeXn_ that take a number and a string argument
+
+\newcount\bbalance
+\newif\iftracetexpp
+\newtoks\textoks
+
+\def\TeXx(#1)#2;{% TODO
+ \let\oldttdot\.\relaxcweb
+ \textoks{}\let\.\dotcollect
+ #1%
+ \restorecweb\let\.\oldttdot
+ \expandafter\T@Xx\the\textoks}
+
+\def\mypar{\par}
+
+\def\TeXb(#1)#2;{% TeX material begin
+ {}$%
+ \let\oldsix\6%
+ \let\6\ignorespaces
+ \let\oldC\C
+ \let\C\saveCcomments
+ \let\oldttdot\.\relaxcweb
+ \textoks{}\toksa{}\let\.\dotcollectb
+ #1%
+ \restorecweb\let\.\oldttdot
+ \dotcollectstripquotes
+ ${}}
+
+\def\TeXa(#1)#2;{% TeX material add
+ {}$%
+ \let\oldttdot\.\relaxcweb
+ \toksa{}\let\.\dotcollectb
+ #1%
+ \restorecweb\let\.\oldttdot
+ \dotcollectstripquotes
+ ${}}
+
+\def\TeXf(#1)#2;{% TeX material add
+ {}$%
+ \let\oldttdot\.\relaxcweb
+ \toksa{}\let\.\dotcollectb
+ \textoks\expandafter{\the\textoks\hbox{\6}}%
+ #1%
+ \restorecweb\let\.\oldttdot
+ \dotcollectstripquotes
+ ${}}
+
+\def\TeXo(#1)#2;{% TeX material output
+ \let\oldttdot\.\relaxcweb
+ \let\.\dotcollect
+ \let\6\oldsix
+ \let\C\oldC
+ #1%
+ \restorecweb\let\.\oldttdot
+ $\expandafter\T@Xx\expandafter"\the\textoks"$}
+
+\def\TeXao(#1)#2;{% TeX material output
+ {}$\let\oldttdot\.\relaxcweb
+ \toksa{}\let\.\dotcollectb
+ \let\6\oldsix
+ \let\C\oldC
+ #1%
+ \restorecweb\let\.\oldttdot
+ \dotcollectstripquotes
+ $\expandafter\T@Xx\expandafter"\the\textoks"${}${}}
+
+\def\TeXfo(#1)#2;{% TeX material output
+ {}$\let\oldttdot\.\relaxcweb
+ \toksa{}\let\.\dotcollectb
+ \textoks\expandafter{\the\textoks\hbox{\6}}%
+ \let\6\oldsix
+ \let\C\oldC
+ #1%
+ \restorecweb\let\.\oldttdot
+ \dotcollectstripquotes
+ $\expandafter\T@Xx\expandafter"\the\textoks"${}${}}
+
+\let\TeXxi\TeXx
+\def\inlineTeXx#1{$\TeXxi(\.{"#1"});$} % for indexing macros
+
+\def\dotcollect#1{\toksa{#1}\concat\textoks\toksa}
+\def\dotcollectb#1{\toksb{#1}\concat\toksa\toksb}
+\def\dotcollectstripquotes{\expandafter\d@tcollectstripquotes\the\toksa}
+\def\d@tcollectstripquotes"#1"{\toksa{#1}\concat\textoks\toksa}
+\def\saveCcomments#1{\toksc{\hbox{\oldC{#1}}}\concat\textoks\toksc}
+\def\relaxcweb{\savehcs{local-namespace}{\)}}
+\def\restorecweb{\restorecs{local-namespace}{\)}}
+
+\def\T@Xx"#1"{%
+ {}${}%$
+ \iffalse{\fi % alignment!
+ \begingroup
+ % tune up the standard input routines
+ \let\yyreturn\texlexer
+ \let\multicharswitch\empty
+ \let\onecharswitch\empty
+ \setspecialcharsfrom\multicharswitch % debugging
+ \setspecialcharsfrom\onecharswitch
+ %
+ \let\currentstate\texdefaultstate
+ \texlinetoks{}\texidxtoks{}\bbalance\z@
+ \let\bbal\bbalempty
+ \yytextbackupfalse
+ \restorecsxlist\texnspace\alltexsymbols
+ \let\termindex\writetexidxentry
+ \yygetchar#1\end
+ \toksc{#1}%
+ \iftracetexpp{\newlinechar=`^^J%
+ \errmessage{TeX_ input: \the\toksc^^JTeX_ first pass: \the\texlinetoks}}\fi
+ \ifnum\bbalance=\z@
+ \else
+ \bbbalance
+ \fi
+ \iftracetexpp\errmessage{TeX_ final pass: \the\texlinetoks}\fi
+ \concat\texlinetoks\texidxtoks
+ \expandafter
+ \endgroup
+ \expandafter
+ \begingroup
+% the actual typesetting must happen outside the group
+% otherwise there is a risk that an output routine is called before
+% the group is complete and \yyreturn definition is wrong so \yyparse
+% will not be able to function
+ \expandafter\texlinetoks\expandafter{\the\texlinetoks}%
+ \let\bbal\bbalempty\bbalance\z@
+ \restorecsxlist\texnspace\alltexsymbols
+ \let\termindex\writetexidxentry\tt\chardef\_=`\_\the\texlinetoks
+ \endgroup
+ \iffalse}\fi
+ {}${}%$
+}
+
+\def\alltexsymbols{%
+ \space\toksa\toksb\toksc\tokse\toksf\the\ifx\ifnum\fi\else
+ \def\edef\let\empty\next\switchon\in\concat\appendr\default
+ \noexpand\emptyterm\print\relax\yy\inmath\omit\hfil\getfirst
+ \getsecond\getthird\getfourth\getfifth\nx\to\hspace\toksd\rhscont
+ \rhscnct\rhsbool\table\ifrhsfull\rhsfulltrue\rhsfullfalse
+ \yyval\tempca\tempcb\z@\@ne\tw@\m@ne\advance\ifcat\iftracebadchars
+ \bb\yylexreturnptr\yylexreturn\yylexreturnval\yylexreturnchar
+ \yylexreturntext\yylexnext
+}
+
+\def\collectspaces#1{%
+ \def\next{#1}%
+ \ifx#1\endcontainer
+ \let\next\relax
+ \else
+ \ifx\next\spacecontainer
+ \appendr\toksa\next
+ \let\next\collectspaces
+ \else
+ \let\next\eattoend
+ \fi
+ \fi
+ \next
+}
+
+\def\spacecontainer{\ }
+
+\def\texnspace{texline}
+
+\let\defpostfix\defTpostfix
+\let\defprefix\empty
+
+\let\defypreamble\empty % for indexing macros
+\def\defypostamble{ {\rm(\.{\\\thisnamex})}}
+
+\let\settgroup\relax
+
+\defx\space{\hbox{$\,$\char`\ $\,$}}{texline}
+
+\defx\hspace{\hbox{$\,$\char`\ $\,$}}{texline}
+
+\defy\hspace{\hbox{$\,$\char`\ $\,$}}{index}
+
+\defx\advance{%
+ $\mathop{\hbox{\bf add}}{}$%
+}{texline}
+
+\defy\advance{%
+ {\bf add}%
+}{index}
+
+\defx\z@{%
+ $\,0_{\rm R}\,$%
+}{texline}
+
+\defy\z@{%
+ $0_{\rm R}$%
+}{index}
+
+\defx\@ne{%
+ $\,1_{\rm R}\,$%
+}{texline}
+
+\defy\@ne{%
+ $1_{\rm R}$%
+}{index}
+
+\defx\tw@{%
+ $\,2_{\rm R}\,$%
+}{texline}
+
+\defy\tw@{%
+ $2_{\rm R}$%
+}{index}
+
+\defx\m@ne{%
+ $\,-1_{\rm R}\,$%
+}{texline}
+
+\defy\m@ne{%
+ $-1_{\rm R}$%
+}{index}
+
+\defx\tempca{%
+ ${}t_a{}$%
+}{texline}
+
+\defy\tempca{%
+ $t_a$%
+}{index}
+
+\defx\tempcb{%
+ ${}t_b{}$%
+}{texline}
+
+\defy\tempcb{%
+ $t_b$%
+}{index}
+
+\defx\toksa{%
+ {}${}v_a{}${}%
+ \def\setegroup{}%
+ \def\setpgroup{%
+ $\leftarrow\langle\,\hbox{\the\toksa}%
+ \if\next]%
+ \else
+ \rangle%
+ \fi
+ $}\grabbalanced
+}{texline}
+
+\defy\toksa{%
+ ${}v_a{}$%
+}{index}
+
+\defx\toksb{%
+ {}${}v_b{}${}%
+ \def\setegroup{}%
+ \def\setpgroup{%
+ $\leftarrow\langle\,\hbox{\the\toksa}%
+ \if\next]%
+ \else
+ \rangle%
+ \fi
+ $}\grabbalanced
+}{texline}
+
+\defy\toksb{%
+ ${}v_b{}$%
+}{index}
+
+\defx\toksc{%
+ {}${}v_c{}${}%
+ \def\setegroup{}%
+ \def\setpgroup{%
+ $\leftarrow\langle\,\hbox{\the\toksa}%
+ \if\next]%
+ \else
+ \rangle%
+ \fi
+ $}\grabbalanced
+}{texline}
+
+\defy\toksc{%
+ ${}v_c{}$%
+}{index}
+
+\defx\toksd{%
+ {}${}v_d{}${}%
+ \def\setegroup{}%
+ \def\setpgroup{%
+ $\leftarrow\langle\,\hbox{\the\toksa}%
+ \if\next]%
+ \else
+ \rangle%
+ \fi
+ $}\grabbalanced
+}{texline}
+
+\defy\toksd{%
+ ${}v_d{}$%
+}{index}
+
+\defx\tokse{%
+ {}${}v_e{}${}%
+ \def\setegroup{}%
+ \def\setpgroup{%
+ $\leftarrow\langle\,\hbox{\the\toksa}%
+ \if\next]%
+ \else
+ \rangle%
+ \fi
+ $}\grabbalanced
+}{texline}
+
+\defy\tokse{%
+ ${}v_e{}$%
+}{index}
+
+\defx\toksf{%
+ {}${}v_f{}${}%
+ \def\setegroup{}%
+ \def\setpgroup{%
+ $\leftarrow\langle\,\hbox{\the\toksa}%
+ \if\next]%
+ \else
+ \rangle%
+ \fi
+ $}\grabbalanced
+}{texline}
+
+\defy\toksf{$v_f$}{index}
+
+\defx\yyval{%
+ {}${}\Upsilon{}${}%
+ \def\setegroup{}%
+ \def\setpgroup{%
+ $\leftarrow\langle\,\the\toksa
+ \if\next]%
+ \else
+ \rangle%
+ \fi
+ $}\grabbalanced
+}{texline}
+
+\defy\yyval{%
+ ${}\Upsilon{}$%
+}{index}
+
+\def\setflexreturn#1{%
+ \def\setegroup{{\bf return}#1}%
+ \def\setpgroup{%
+ {%
+ \let\texidxdomain\bisonidxdomain
+ \tokse\toksa
+ \expandafter\nameproc\expandafter{\the\toksa}%
+ \ifyyparsefail
+ \edef\next{\toksa{\termmetastyle{%
+ \expandafter\gidxentry\expandafter{\expandafter\termvstring\expandafter}\expandafter{\the\toksa}%
+ \let\nx\idxfont\nx\empty\nx\tt\the\toksa\nx\/%
+ }}}\next
+ \else
+ \expandafter\settermstyle\expandafter{\the\tokse}%
+ \fi
+ {}$\mathop{\hbox{{\bf return}#1}}\hbox{\the\toksa}${}}%
+ }\grabbalanced
+}
+
+\defx\yylexreturnptr{%
+ \setflexreturn{$_p${}}%
+}{texline}
+
+\defy\yylexreturnptr{%
+ {\bf return$_p$}%
+}{index}
+
+\defx\yylexreturnchar{%
+ {\bf return$_c$}%
+}{texline}
+
+\defy\yylexreturnchar{%
+ {\bf return$_c$}%
+}{index}
+
+\defx\yylexnext{%
+ {\bf continue}%
+}{texline}
+
+\defy\yylexnext{%
+ {\bf continue}%
+}{index}
+
+\defx\yylexreturn{%
+ \setflexreturn{$_l${}}%
+}{texline}
+
+\defy\yylexreturn{%
+ {\bf return$_l$}%
+}{index}
+
+\defx\yylexreturnval{%
+ \setflexreturn{$_v${}}%
+}{texline}
+
+\defy\yylexreturnval{%
+ {\bf return$_v$}%
+}{index}
+
+\defx\yylexreturntext{%
+ {\bf return$_t$}%
+}{texline}
+
+\defy\yylexreturntext{%
+ {\bf return$_t$}%
+}{index}
+
+\defx\table{{}${}\Omega{}${}}{texline}
+
+\defy\table{$\Omega$}{index}
+
+\defx\relax{\hbox{$\circ$}}{texline}
+
+\defy\relax{\hbox{$\circ$}}{index}
+
+\defx\the#1{%
+ \toksa{#1}%
+ \let\prevdefault\default
+ \def\default{\let\default\prevdefault{}$\mathop{\rm val}\,${}#1}%
+ \taction{\the\toksa}\in\thecomaction
+}{texline}
+
+\defy\the{%
+ $\mathop{\rm val}\cdot$ {\rm or }%
+ \lcenclose{$\cdot$}%
+}{index}
+
+\def\thecomaction{%
+\raw \toksaxTeXmode\toksbxTeXmode\tokscxTeXmode\toksdxTeXmode\toksexTeXmode\toksfxTeXmode \raw
+{%
+ \let\default\prevdefault
+ \lcenclose{\the\toksa}%
+}%
+}
+
+\setspecialcharsfrom\thecomaction
+
+\def\lcenclose#1{%
+ {}$\llcorner\hbox{#1}\lrcorner${}%
+}
+
+\defx\inmath{%
+ {}$^\bullet${}%
+ \def\setegroup{}%
+ \def\setpgroup{%
+ $(\,\hbox{\the\toksa}%
+ \if\next]%
+ \else
+ )%
+ \fi
+ $}\grabbalanced
+}{texline}
+
+\defy\inmath{%
+ $^\bullet(\,\cdot\,)$%
+}{index}
+
+\defx\ifx{%
+ {\bf if$_{\rm x}\;$}%
+}{texline}
+
+\defy\ifx{%
+ {\bf if$_{\rm x}$}%
+}{index}
+
+\defx\ifnum{%
+ {\bf if$_\omega\;$}%
+}{texline}
+
+\defy\ifnum{%
+ {\bf if$_\omega$}%
+}{index}
+
+\defx\ifcat{%
+ {\bf if$_{\rm cat}\;$}%
+}{texline}
+
+\defy\ifcat{%
+ {\bf if$_{\rm cat}$}%
+}{index}
+
+\defx\iftracebadchars{%
+ {\bf if$_t$ {\rm[{\tt bad char}]}$\;$}%
+}{texline}
+
+\defy\iftracebadchars{%
+ {\bf if$_t$ {\rm[{\tt bad char}]}}%
+}{index}
+
+\defx\else{%
+ {\bf else$\;$}%
+}{texline}
+
+\defx\fi{%
+ {\bf fi$\;$}%
+}{texline}
+
+\defx\def{%
+ {\bf def$\;$}%
+}{texline}
+
+\defy\def{%
+ {\bf def}%
+}{index}
+
+\defx\edef{%
+ {\bf def$_{\rm x}\;$}%
+}{texline}
+
+\defy\edef{%
+ {\bf def$_{\rm x}$}%
+}{index}
+
+\defx\let{%
+ {\bf let$\;$}%
+}{texline}
+
+\defx\next{%
+ {\bf next$\;$}%
+}{texline}
+
+\defx\empty{%
+ $\emptyset$%
+}{texline}
+
+\defy\empty{%
+ $\emptyset$%
+}{index}
+
+\defx\ifrhsfull{%
+ {\bf if {\rm ($\,$rhs${}={}$full$\,$)}$\;$}%
+}{texline}
+
+\defy\ifrhsfull{%
+ {\bf if {\rm ($\,$rhs${}={}$full$\,$)}}%
+}{index}
+
+\defx\rhsfulltrue{%
+ {\rm rhs${}={}$full$\,$}%
+}{texline}
+
+\defy\rhsfulltrue{%
+ {\rm rhs${}={}$full}%
+}{index}
+
+\defx\rhsfullfalse{%
+ {\rm rhs${}={}$not full$\,$}%
+}{texline}
+
+\defy\rhsfullfalse{%
+ {\rm rhs${}={}$not full}%
+}{index}
+
+\defx\noexpand{%
+ $^{\rm nox}$%
+}{texline}
+
+\defx\nx{%
+ $^{\rm nx}$%
+}{texline}
+
+\defy\noexpand{%
+ $^{\rm nox}$%
+}{index}
+
+\defy\nx{%
+ $^{\rm nx}$%
+}{index}
+
+\defx\to{%
+ ${}\mapsto{}$%
+}{texline}
+
+\defx\emptyterm{%
+ \hbox{$\ulcorner\ldots\urcorner$}%
+}{texline}
+
+\defy\emptyterm{%
+ \hbox{$\ulcorner\ldots\urcorner$}%
+}{index}
+
+\defx\hfil{\hbox{$\,\Leftrightarrow\,$}}{texline}
+\defx\omit{\hbox{$\,{\times\atop\times}$}}{texline}
+
+\defx\yy#1{%
+ \if\noexpand#1]%
+ \let\next\seeksymtt
+ \else
+ \if\noexpand#1[%
+ \let\next\seeksymts
+ \else
+ \if\noexpand#1(%
+ \let\next\seeknott
+ \else
+ \def\next{\seeknots#1}%
+ \fi
+ \fi
+ \fi
+ \next
+}{texline}
+
+\defy\yy{%
+ $\Upsilon\kern-1pt{}_{\rm?}$%
+}{index}
+
+\def\seeknots#1\bbal{%
+ \let\setegroup\relax
+ \ifnum#1>0\relax
+ \def\setpgroup{%
+ \edef\next{\the\toksa}%
+ \ifx\next\empty
+ $\Upsilon\kern-1pt{}_{\number\tempca}$%
+ \else
+ $\Upsilon\kern-1pt{}_{\number\tempca}\rightarrow[{}${\tt\the\toksa}]$\;$%
+ \fi}%
+ \else
+ \def\setpgroup{%
+ $\Upsilon\leftarrow\langle{}${\tt\the\toksa}%${}%
+ \if\next]%
+ \else
+ $\rangle\;$%
+ \fi}%
+ \fi
+ \tempca#1\relax\printtermt
+}
+
+\def\seeksymts#1]{%
+ \let\setegroup\relax
+ \def\setpgroup{$\Upsilon\kern-1pt{}_{\rm#1}\langle{}${\tt\the\toksa}${}\rangle\;$}\grabbalanced
+}
+
+\def\seeksymtt#1[{{$\Upsilon\kern-1pt{}_{\rm#1}$}}
+
+\def\seeknott#1){{$\Upsilon\kern-1pt{}_{\rm#1}$}}
+
+\def\printtermt{\grabbalanced\bbal}
+
+\defx\print{%
+ \hbox{\it print$\;$}%
+ \def\setpgroup{{\tt"}\the\toksa{\tt"}$\,$}%
+ \def\setegroup{}%
+ \grabbalanced
+}{texline}
+
+\defx\bb#1\bbal{%
+ \let\setegroup\relax
+ \ifnum#1>0\relax
+ \def\setpgroup{%
+ \edef\next{\the\toksa}%
+ \ifx\next\empty
+ ${}_{\number\tempca}\kern-1.5pt\Upsilon$%
+ \else
+ ${}_{\number\tempca}\kern-1.5pt\Upsilon\rightarrow[{}${\tt\the\toksa}$]\;$%
+ \fi}%
+ \else
+ \def\setpgroup{%
+ $\Upsilon\leftarrow\langle{}${\tt\the\toksa}%${}%
+ \if\next]%
+ \else
+ $\rangle\;$%
+ \fi}%
+ \fi
+ \tempca#1\relax\printtermt
+}{texline}
+
+\defy\bb{%
+ ${}_{\rm?}\kern-2pt\Upsilon$%
+}{index}
+
+\defx\switchon{%
+ \hbox{\bf switch$\;$}%
+ \def\setpgroup{{$($}\the\toksa{$)$}$\,$}%
+ \def\setegroup{}%
+ \grabbalanced
+}{texline}
+
+\defy\switchon{%
+ \hbox{\bf switch$\;$}%
+}{index}
+
+\defx\in{%
+ $\,\varepsilon\,$%
+}{texline}
+
+\defy\in{%
+ $\,\varepsilon\,$%
+}{index}
+
+\defx\concat#1#2{%
+ \hbox{#1${}\leftarrow{}$#1${}+_{\rm s}{}$#2$\;$}%
+}{texline}
+
+\defy\concat{%
+ \hbox{$A\leftarrow A+_{\rm s}B$}%
+}{index}
+
+\defx\appendr#1{%
+ \hbox{#1${}\leftarrow{}$#1${}+_{\rm sx}{}$}%
+ \def\setpgroup{{$[\,$}\the\toksa{$\,]$}$\,$}%
+ \def\setegroup{}%
+ \grabbalanced
+}{texline}
+
+\defy\appendr{%
+ \hbox{$A\leftarrow A+_{\rm sx}B$}%
+}{index}
+
+\defx\default{%
+ {\tt default}$\;$%
+}{texline}
+
+
+\defx\getfirst{%
+ {}${}\pi_1${}%
+ \def\setegroup{\relax}%
+ \def\setpgroup{%
+ ${}(\hbox{\the\toksa}%
+ \if\next]%
+ \else
+ )%
+ \fi
+ $}\grabbalanced
+}{texline}
+
+\defy\getfirst{%
+ ${}\pi_1$%
+}{index}
+
+\defx\getsecond{%
+ {}${}\pi_2${}%
+ \def\setegroup{\relax}%
+ \def\setpgroup{%
+ ${}(\hbox{\the\toksa}%
+ \if\next]%
+ \else
+ )%
+ \fi
+ $}\grabbalanced
+}{texline}
+
+\defy\getsecond{%
+ ${}\pi_2$%
+}{index}
+
+\defx\getthird{%
+ {}${}\pi_3${}%
+ \def\setegroup{\relax}%
+ \def\setpgroup{%
+ ${}(\hbox{\the\toksa}%
+ \if\next]%
+ \else
+ )%
+ \fi
+ $}\grabbalanced
+}{texline}
+
+\defy\getthird{%
+ ${}\pi_3$%
+}{index}
+
+\defx\getfourth{%
+ {}${}\pi_4${}%
+ \def\setegroup{\relax}%
+ \def\setpgroup{%
+ ${}(\hbox{\the\toksa}%
+ \if\next]%
+ \else
+ )%
+ \fi
+ $}\grabbalanced
+}{texline}
+
+\defy\getfourth{%
+ ${}\pi_4$%
+}{index}
+
+\defx\getfifth{%
+ {}${}\pi_5${}%
+ \def\setegroup{\relax}%
+ \def\setpgroup{%
+ ${}(\hbox{\the\toksa}%
+ \if\next]%
+ \else
+ )%
+ \fi
+ $}\grabbalanced
+}{texline}
+
+\defy\getfifth{%
+ ${}\pi_5$%
+}{index}
+
+\defx\rhscont{%
+ {}${}\pi_{\{\}}${}%
+ \def\setegroup{\relax}%
+ \def\setpgroup{%
+ ${}(\hbox{\the\toksa}%
+ \if\next]%
+ \else
+ )%
+ \fi
+ $}\grabbalanced
+}{texline}
+
+\defy\rhscont{%
+ ${}\pi_{\{\}}$%
+}{index}
+
+\defx\rhscnct{%
+ {}${}\pi_{\leftrightarrow}${}%
+ \def\setegroup{\relax}%
+ \def\setpgroup{%
+ ${}(\hbox{\the\toksa}%
+ \if\next]%
+ \else
+ )%
+ \fi
+ $}\grabbalanced
+}{texline}
+
+\defy\rhscnct{%
+ ${}\pi_{\leftrightarrow}$%
+}{index}
+
+\defx\rhsbool{%
+ {}${}\pi_{\vdash}${}%
+ \def\setegroup{\relax}%
+ \def\setpgroup{%
+ ${}(\hbox{\the\toksa}%
+ \if\next]%
+ \else
+ )%
+ \fi
+ $}\grabbalanced
+}{texline}
+
+\defy\rhsbool{%
+ ${}\pi_{\vdash}$%
+}{index}
+
+\def\bbalempty[#1]#2{%
+ \ifx#2]\relax
+ \else
+ \ifx#2[\relax
+ \else
+ \ifnum`#2=`\{%
+ #2\hbox{$\,$}%
+ \else
+ \unskip\hbox{$\,$}#2%
+ \fi
+ \fi
+ \fi
+}%
+
+\def\bbbalance{%
+ \ifnum\bbalance>0
+ \loop
+ \advance\bbalance-1\relax
+ \appendr\texlinetoks{\noexpand\bbal[\the\bbalance]]}%
+ \ifnum\bbalance>0
+ \repeat
+ \else
+ \tempca-\bbalance
+ \toksd{}%
+ \loop
+ \advance\tempca-1\relax
+ \appendl\toksd{\noexpand\bbal[\the\tempca][}%
+ \ifnum\tempca>0
+ \repeat
+ \tempca-\bbalance
+ \bbalance\tempca
+ \texlinetoks{}\texidxtoks{}%
+ \expandafter\yygetchar\the\toksc\end
+% \errmessage{\the\texlinetoks...\the\toksd...\the\bbalance}%
+ \appendl\texlinetoks{\the\toksd}%
+ \fi
+}
+
+\def\grabbalanced{%
+ \futurelet\next\gr@bbalanced
+}
+
+\def\gr@bbalanced{%
+ \ifx\next\bbal
+ \let\next\gr@bb@lanced
+ \else
+ \let\next\settgroup
+ \fi
+ \next
+}
+
+\def\gr@bb@lanced\bbal[#1]#2{%
+ \ifnum`#2=`\}% this is a closing parenthesis we are inside a group
+ \def\next{\setegroup\bbal[#1]#2}%
+ \toksa{#2}%
+ \else
+ \ifnum`#2=`]%
+ \def\next{\setegroup\bbal[#1]#2}%
+ \toksa{#2}%
+ \else
+ \def\next##1\bbal[#1]##2{%
+ \toksa{##1}\let\next##2%
+ \setpgroup
+ }%
+ \fi
+ \fi
+ \next
+}