#!/bin/sh

# delete theories named on command line

GLOBAL=global.erg
TMP=delt.tmp.$$

if [ "$#" -lt 1 ]
then
	echo "Usage: $0 theories..."
	echo "       (theories must be ordered with leaf theories first)"
	exit 2
fi

for thy
do
  # check that $thy is a valid theory
  if egrep -s "^ancestor.*\[$thy," $GLOBAL
  then
    echo "Deleting theory: $thy..."
    if egrep "parent.*\[.*, *$thy" $GLOBAL
    then
      echo "Sorry, can't delete '$thy' because it has children"
      exit 1
    else
      grep -v "$thy," $GLOBAL > $TMP
      mv $TMP $GLOBAL
    fi
  else
    echo "Theory '$thy' not found in $GLOBAL"
  fi
done
