doc-src/TutorialI/isa-index
author wenzelm
Wed Jul 25 12:38:54 2012 +0200 (2012-07-25)
changeset 48497 ba61aceaa18a
parent 11404 280436a346ca
permissions -rwxr-xr-x
some updates on "Building a repository version of Isabelle";
paulson@11400
     1
#! /bin/sh
paulson@11400
     2
#
paulson@11400
     3
#sedindex - shell script to create indexes, preprocessing LaTeX's .idx file
paulson@11400
     4
#
paulson@11400
     5
#  puts strings prefixed by * into \tt font
paulson@11400
     6
#    terminator characters for strings are |!@{}
paulson@11400
     7
#
paulson@11400
     8
# a space terminates the \tt part to allow \index{*notE theorem}, etc.
paulson@11400
     9
#
paulson@11400
    10
# note that makeindex uses a dboule quote (") to delimit special characters.
paulson@11400
    11
#
paulson@11400
    12
# change *"X"Y"Z"W  to  "X"Y"Z"W@{\tt "X"Y"Z"W}
paulson@11400
    13
# change *"X"Y"Z    to  "X"Y"Z@{\tt "X"Y"Z}
paulson@11400
    14
# change *"X"Y      to  "X"Y@{\tt "X"Y}
paulson@11400
    15
# change *"X        to  "X@{\tt "X}
paulson@11400
    16
# change *IDENT  to  IDENT@{\tt IDENT}  
paulson@11400
    17
#    where IDENT is any string not containing | ! or @
paulson@11400
    18
# FOUR backslashes: to escape the shell AND sed
paulson@11404
    19
sed -e "s~\*\(\".\".\".\".\)~\1@\\\\isa {\1}~g
paulson@11404
    20
s~\*\(\".\".\".\)~\1@\\\\isa {\1}~g
paulson@11404
    21
s~\*\(\".\".\)~\1@\\\\isa {\1}~g
paulson@11404
    22
s~\*\(\".\)~\1@\\\\isa {\1}~g
paulson@11404
    23
s~\*\([^ |!@{}][^ |!@{}]*\)~\1@\\\\isa {\1}~g" $1.idx | makeindex -c -q -o $1.ind