1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/IMP/export.sh	Sun Oct 23 17:37:21 2011 +1100
     1.3 @@ -0,0 +1,42 @@
     1.4 +#!/bin/bash
     1.5 +#
     1.6 +# Author: Gerwin Klein
     1.7 +#
     1.8 +#  make a copy of IMP with isaverbatimwrite lines in thy files removed
     1.9 +
    1.10 +## diagnostics
    1.11 +
    1.12 +function fail()
    1.13 +{
    1.14 +  echo "$1" >&2
    1.15 +  exit 2
    1.16 +}
    1.17 +
    1.18 +## main
    1.19 +
    1.20 +EXPORT=IMP
    1.21 +
    1.22 +rm -rf "$EXPORT"
    1.23 +
    1.24 +# make directories
    1.25 +
    1.26 +DIRS=$(find . -type d)
    1.27 +for D in $DIRS; do
    1.28 +    mkdir -p "$EXPORT/$D" || fail "could not create directory $EXPORT/$D"
    1.29 +done
    1.30 +
    1.31 +# filter thy files
    1.32 +
    1.33 +FILES=$(find . -name "*.thy")
    1.34 +for F in $FILES; do
    1.35 +    grep -v isaverbatimwrite "$F" > "$EXPORT/$F"
    1.36 +done
    1.37 +
    1.38 +# copy rest
    1.39 +
    1.40 +cp ROOT.ML "$EXPORT"
    1.41 +cp -r document "$EXPORT"
    1.42 +
    1.43 +# tar and clean up
    1.44 +tar cvzf "$EXPORT.tar.gz" "$EXPORT"
    1.45 +rm -r "$EXPORT"