: Filter for converting a MATHS document into HTML. LOCALHOSTDOMAIN=.csci.csusb.edu; export LOCALHOSTDOMAIN LOCALHOST=www$LOCALHOSTDOMAIN; export LOCALHOST if [ $# -eq 0 ]; then echo Usage: $0 input_file\[.mth\]; exit 1; fi if expr $1 : '.*\.mth$' >/dev/null then mthfile=$1; name=`expr $mthfile : '\(.*\)\.mth$`; htmlfile=$name.html else name=$1; mthfile=$1.mth; htmlfile=$1.html fi if expr $mthfile : ".*/" >/dev/null then source=expr $name : ".*/\([^/]*\)$" else source=$name fi tmp=/tmp/mth2html$$; index=$tmp.index; contents=$tmp.contents trap "rm $tmp*" 1 2 3 # # extract contents list and index sed -n '/^\.[ OC]/p' $mthfile| ascii2html| awk 'BEGIN{n=0; } /^\.Open/{ for(i=1;i<=n;i++)$2=": " $2;n++; print} /^\. ./{ for(i=1;i<=n;i++)$2=": " $2; print} /^\.Close/{n--; if(n<0)n=0; }'| sed 's/^\.Open *\([: ]*\)\(.*\)$/
  • \1\2<\/A>/ s/^\. *\([: ]*\)\(.*\)$/
  • \1\2<\/A>/' >$contents # ascii2html <$mthfile | sed -n ' /::/{/^[ ]*\([A-Za-z0-9_]*\)[ ]*::[ ]*.*$/s//
  • \1 <\/A>(Definition)/p /^[ ]*\([A-Za-z0-9_]*\)([^)]*)::[ ]*.*$/s//
  • \1 <\/A>(Declaration)/p bdone } /|-/{ s/^.*|-[ ]*(\([^)]*\)):.*$/
  • \1 <\/A>(Theorem)/p bdone } s/^[ ][ ]*(\([^)][^)]*\)):.*$/
  • \1 <\/A>(Axiom)/p s/.*(\([^)][^)]*\)):.*$/
  • \1 <\/A>(Label)/p s/--(\([^)]*\))$/
  • \1 <\/A>(Label)/p :done' |sort >$index # cat $mthfile|br 127|awk 'BEGIN{n=2; } /^\.Open/{ $1=$1 n;n++; if(n>6)n=6;} /^\. ./{ $1=$1 n; } /^\.Close/{n--; if(n<2)n=2; } {print}'|ascii2html| sed '/^\.As_is/bend s/`\([^`]*\)`/\1<\/i>/g :end'| ( echo "$name on "`date`"" if [ -x standard.include.sh ] then standard.include.sh $source.mth else if [ -r standard.include.html ] then cat standard.include.html fi fi echo 'There is an alphabetical index.' echo '

    Contents

    ' echo "
      " sed '/^\.Close/d /^\.As_is/{ s/^\.As_is\(.*\)/<\/ol>
      \1<\/pre>
        /
bdone
}
s/^$/
        /
s/^[ 	]*For /
        For /
/::/bnwff
/|-/{
s/^[ 	]*(\([^),]*\)\([^)]*\))[ 	]*|-[ 	]*/
      1. (\1<\/X>\2)|-/
:whileX
/<.X>/{
s/<.X>,[ 	]*\([^),]*\)/<\/A>, \1<\/X>/
s/<.X>[ 	]*)/<\/A>) /
bwhileX
}
s/^[ 	]*|-[ 	]*/
      2. (above)|-/
s/|-[ 	]*(\(.*\)):/|-<\/A>(\1): /
s/^[ 	][ 	]*(\([^)][^)]*\)):[ 	]*/
      3. (\1): /
s/(\([^)][^)]*\)):/(\1<\/A>): /
bnwff
}
s/(\([^)][^)]*\)):[ 	]*/(\1<\/A>): /
s/^[ 	][ 	]*/
      4. /
:nwff
/{.*}/!{
s/^[ 	]*Let[ 	]*{/
      5. Let{
          /
s/^[ 	]*[pP]o[ 	]*{/
        1. Po{
            /
s/^[ 	]*Case[ 	]*{/
          1. Case{
              /
s/^[ 	]*Else[ 	]*/
            1. Else/
s/^[ 	]*Consider[ 	]*{/
            2. Consider{
                /
s/^\(.*\)Net[ 	]*{[ 	]*/\1 Net{
                  /
}
:ends
/{.*}/!{
s/^
                  \(}[.,]*\)[ 	]*$/
                  \1<\/ol>/
s/^[ 	]*\(}[.,]*\)[ 	]*$/
                  \1<\/ol>/
/^[ 	]*}=::.*$/{
s/^[ 	]*\(}=::.*\)$/<\/ol>
                  \1/
bdone
}
}
/^\.See /{
s/\/\/www\//\/\/'$LOCALHOST'\//
s/^\.See \(.*\):\(\/\/.*\)\/\([^/]*\)\.\([^.][^.]*\)#\(.*\)$/\5\[\3<\/cite>\]<\/A>/
s/^\.See \(.*\):\(\/\/.*\)\/$/ \[\1:\2\/<\/cite>\] <\/A>/
s/^\.See \(.*\):\(\/\/.*\)\/\([^/]*\)$/ \[\3<\/cite>\] <\/A>/
s/^\.See \(.*\):\(\/\/.*\)\/\([^/]*\)\.\([^.]*\)$/ \[\3<\/cite>\] <\/A>/
s/^\.See \(.*\):\(\/[^/].*\)$/ [\2] <\/A>/
s/^\.See \(.*\)$/ \[\1<\/cite>\] <\/A>/
bdone
}
/::/bdefs
/^[ 	]/{ s/^[ 	]\(.*\)$/
                  \1/
bdone
}
/^\./{
s/^\.Open\(.\) *\(.*\)$/                  \2<\/H\1><\/A>/
s/^\.Source *\(.*\)$/\1<\/cite>/
s/^\.Address *\(.*\)$/
                  \1<\/address>/
s/^\.Image *\([^ 	]*\)[ 	]\(.*\)$/\2/
s/^\.\([1-6]\) \(.*\)$/\2<\/H\1><\/A>/
bdone
}
:defs
/::/{
/^[ 	]*\([\\A-Za-z0-9_.!@#$%^&*-+|<>=~ ]*\)[ 	]*::\([^=]*\)=\(.*\)$/s//
                1. \1<\/A>::\2=\3/
/^[ 	]*\([\\A-Za-z0-9_.!@#$%^&*-+|<>=~ ]*\)[ 	]*::[ 	]*\([^=]*\)$/s//
                2. \1<\/A>::\2/
/^[ 	]*\([\\A-Za-z0-9_.!@#$%^&*-+|<>=~ ]*\)[ 	]*\(([^)]*)\)::\([^=]*\)=\(.*\)$/s//
                3. \1<\/A>\2::\3=\4/
/^[ 	]*\([\\A-Za-z0-9_.!@#$%^&*-+|<>=~ ]*\)[ 	]*\(([^)]*)\)::\([^=]*\)$/s//
                4. \1<\/A>\2::\3/
/^[ 	]*\([\\A-Za-z0-9_.!@#$%^&*-+|<>=~ ]*\)[ 	]*\(([^)]*)\)::\([^=]*\)$/s//
                5. \1<\/A>\2::\3/
/^[ 	]*\([\\A-Za-z0-9_.!@#$%^&*-+|<>=~ ]*\)[ 	]*\(([^)]*)\)::\([^=]*\)$/s//
                6. \1<\/A>\2::>\3/
/^
                7. /!s/\(.*\)::\([^=]*\)$/
                8. \1::\2/
/^
                9. /!s/\(.*\)::\([^=]*\)=/
                10. \1::\2=/
}
:done
'
echo "
                "
echo "
                "
echo '
                Labels and Definitions in Alphabetical Order
                '
echo "
                  "
cat $index
echo "
                "
[ -r $HOME/.signature.html ] && ( echo '
                '; cat $HOME/.signature.html)
echo ""
) >$htmlfile 
rm $tmp*