equal
deleted
inserted
replaced
8 \definecolor{darkblue}{rgb}{0,0,0.6} |
8 \definecolor{darkblue}{rgb}{0,0,0.6} |
9 \usepackage[colorlinks=true,urlcolor=darkblue,linkcolor=darkblue]{hyperref} |
9 \usepackage[colorlinks=true,urlcolor=darkblue,linkcolor=darkblue]{hyperref} |
10 |
10 |
11 \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% |
11 \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% |
12 \definecolor{codegray}{gray}{0.9} |
12 \definecolor{codegray}{gray}{0.9} |
|
13 |
|
14 \newcommand\grid[1]{% |
|
15 \begin{tikzpicture}[baseline=(char.base)] |
|
16 \path[use as bounding box] |
|
17 (0,0) rectangle (1em,1em); |
|
18 \draw[red!50, fill=red!20] |
|
19 (0,0) rectangle (1em,1em); |
|
20 \node[inner sep=1pt,anchor=base west] |
|
21 (char) at (0em,\gridraiseamount) {#1}; |
|
22 \end{tikzpicture}} |
|
23 \newcommand\gridraiseamount{0.12em} |
|
24 |
|
25 \makeatletter |
|
26 \newcommand\Grid[1]{% |
|
27 \@tfor\z:=#1\do{\grid{\z}}} |
|
28 \makeatother |