doc-src/isar.sty
changeset 28214 1e6d71cd4bf3
parent 26868 60058b050c58
child 28761 9ec4482c9201
equal deleted inserted replaced
28213:b52f9205a02d 28214:1e6d71cd4bf3
     4 \usepackage{ifthen}
     4 \usepackage{ifthen}
     5 
     5 
     6 \newcommand{\indexdef}[3]%
     6 \newcommand{\indexdef}[3]%
     7 {\ifthenelse{\equal{}{#1}}{\index{#3 (#2)|bold}}{\index{#3 (#1\ #2)|bold}}}
     7 {\ifthenelse{\equal{}{#1}}{\index{#3 (#2)|bold}}{\index{#3 (#1\ #2)|bold}}}
     8 \newcommand{\indexref}[3]{\ifthenelse{\equal{}{#1}}{\index{#3 (#2)}}{\index{#3 (#1\ #2)}}}
     8 \newcommand{\indexref}[3]{\ifthenelse{\equal{}{#1}}{\index{#3 (#2)}}{\index{#3 (#1\ #2)}}}
       
     9 
       
    10 \newcommand{\isatt}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\tt #1}}
     9 
    11 
    10 \newcommand{\indexoutertoken}[1]{\indexdef{}{syntax}{#1}}
    12 \newcommand{\indexoutertoken}[1]{\indexdef{}{syntax}{#1}}
    11 \newcommand{\indexouternonterm}[1]{\indexdef{}{syntax}{#1}}
    13 \newcommand{\indexouternonterm}[1]{\indexdef{}{syntax}{#1}}
    12 \newcommand{\indexisarelem}[1]{\indexdef{}{element}{#1}}
    14 \newcommand{\indexisarelem}[1]{\indexdef{}{element}{#1}}
    13 
    15