# HG changeset patch
# User kleing
# Date 1319351841 -39600
# Node ID e41c679c9d823ed29c5367da3cc1671df1e99b17
# Parent  b57523021938fa126340f9aeb49348730a9c9161
script for exporting filtered IMP files as tar.gz

diff -r b57523021938 -r e41c679c9d82 src/HOL/IMP/export.sh
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/export.sh	Sun Oct 23 17:37:21 2011 +1100
@@ -0,0 +1,42 @@
+#!/bin/bash
+#
+# Author: Gerwin Klein
+#
+#  make a copy of IMP with isaverbatimwrite lines in thy files removed
+
+## diagnostics
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+## main
+
+EXPORT=IMP
+
+rm -rf "$EXPORT"
+
+# make directories
+
+DIRS=$(find . -type d)
+for D in $DIRS; do
+    mkdir -p "$EXPORT/$D" || fail "could not create directory $EXPORT/$D"
+done
+
+# filter thy files
+
+FILES=$(find . -name "*.thy")
+for F in $FILES; do
+    grep -v isaverbatimwrite "$F" > "$EXPORT/$F"
+done
+
+# copy rest
+
+cp ROOT.ML "$EXPORT"
+cp -r document "$EXPORT"
+
+# tar and clean up
+tar cvzf "$EXPORT.tar.gz" "$EXPORT"
+rm -r "$EXPORT"