doc-src/TutorialI/isa-index
author huffman
Thu Apr 19 10:49:47 2012 +0200 (2012-04-19)
changeset 47579 28f6f4ad69bf
parent 11404 280436a346ca
permissions -rwxr-xr-x
tuned lemmas (v)image_id;
removed duplicate of vimage_id
     1 #! /bin/sh
     2 #
     3 #sedindex - shell script to create indexes, preprocessing LaTeX's .idx file
     4 #
     5 #  puts strings prefixed by * into \tt font
     6 #    terminator characters for strings are |!@{}
     7 #
     8 # a space terminates the \tt part to allow \index{*notE theorem}, etc.
     9 #
    10 # note that makeindex uses a dboule quote (") to delimit special characters.
    11 #
    12 # change *"X"Y"Z"W  to  "X"Y"Z"W@{\tt "X"Y"Z"W}
    13 # change *"X"Y"Z    to  "X"Y"Z@{\tt "X"Y"Z}
    14 # change *"X"Y      to  "X"Y@{\tt "X"Y}
    15 # change *"X        to  "X@{\tt "X}
    16 # change *IDENT  to  IDENT@{\tt IDENT}  
    17 #    where IDENT is any string not containing | ! or @
    18 # FOUR backslashes: to escape the shell AND sed
    19 sed -e "s~\*\(\".\".\".\".\)~\1@\\\\isa {\1}~g
    20 s~\*\(\".\".\".\)~\1@\\\\isa {\1}~g
    21 s~\*\(\".\".\)~\1@\\\\isa {\1}~g
    22 s~\*\(\".\)~\1@\\\\isa {\1}~g
    23 s~\*\([^ |!@{}][^ |!@{}]*\)~\1@\\\\isa {\1}~g" $1.idx | makeindex -c -q -o $1.ind