Re-organised to perform the tests independently. Now test
is defined in terms of separate targets IMP, ex, etc. If ISABELLECOMP is set
wrongly then "exit 1" causes the Make to fail. Defines the macro "LOGIC" to
refer to the right command for running the object-logic. Uses "suffix
substitution" to shorten macro definitions.
#! /bin/sh
#
#sedindex - shell script to create indexes, preprocessing LaTeX's .idx file
#
# puts strings prefixed by * into \tt font
# terminator characters for strings are |!@{}
#
# uses \ptt instead of \tt since that happens to explicit \tt's
# a space terminates the \tt part to allow \index{*NE theorem}, etc.
#
# change *"X"Y"Z"W to "X"Y"Z"W@{\ptt "X"Y"Z"W}
# change *"X"Y"Z to "X"Y"Z@{\ptt "X"Y"Z}
# change *"X"Y to "X"Y@{\ptt "X"Y}
# change *"X to "X@{\ptt "X}
# change *IDENT to IDENT@{\ptt IDENT}
# where IDENT is any string not containing | ! or @
# FOUR backslashes: to escape the shell AND sed
sed -e "s~\*\(\".\".\".\".\)~\1@{\\\\ptt \1}~g
s~\*\(\".\".\".\)~\1@{\\\\ptt \1}~g
s~\*\(\".\".\)~\1@{\\\\ptt \1}~g
s~\*\(\".\)~\1@{\\\\ptt \1}~g
s~\*\([^ |!@{}][^ |!@{}]*\)~\1@{\\\\ptt \1}~g" $1.idx | makeindex -c -q -o $1.ind