lib/Tools/mkdir

val rev_eq_reflection = def_imp_eq;

#!/bin/bash
#
# $Id$
#
# DESCRIPTION: prepare logic session directory


## diagnostics

PRG=$(basename $0)

function usage()
{
  echo
  echo "Usage: $PRG [OPTIONS] [LOGIC] NAME"
  echo
  echo "  Options are:"
  echo "    -I FILE      alternative IsaMakefile output"
  echo "    -P           include parent logic target"
  echo "    -b           setup build mode (session outputs heap image)"
  echo "    -d           setup document"
  echo
  echo "  Prepare session directory, including IsaMakefile, document etc."
  echo "  with parent LOGIC (default ISABELLE_LOGIC=$ISABELLE_LOGIC)"
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}


## process command line

# options

ISAMAKEFILE="IsaMakefile"
PARENT=""
BUILD=""
DOCUMENT=""

while getopts "I:Pbd" OPT
do
  case "$OPT" in
    I)
      ISAMAKEFILE="$OPTARG"
      ;;
    P)
      PARENT=true
      ;;
    b)
      BUILD=true
      ;;
    d)
      DOCUMENT=true
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


# args


if [ $# -eq 1 ]; then
  LOGIC="$ISABELLE_LOGIC"
  DIR_NAME="$1"; shift
elif [ $# -eq 2 ]; then
  LOGIC="$1"; shift
  DIR_NAME="$1"; shift
else
  usage
fi

DIR=$(dirname "$DIR_NAME")
NAME=$(basename "$DIR_NAME")


## main

# IsaMakefile

mkdir -p "$DIR" || fail "Bad directory: $DIR"
cd "$DIR"


DOCUMENT_ROOT=""

if [ -n "$BUILD" ]; then
  IMAGES="$NAME"
  TEST=""
  TARGET="\$(OUT)/$NAME"
  ROOT_ML="ROOT.ML"
  SOURCES="*.thy"
  [ -n "$DOCUMENT" ] && DOCUMENT_ROOT="document/root.tex"
  USEDIR="\$(USEDIR) -b -P http://isabelle.in.tum.de/library"
else
  IMAGES=""
  TEST="$NAME"
  TARGET="\$(LOG)/$LOGIC-$NAME.gz"
  ROOT_ML="$NAME/ROOT.ML"
  SOURCES="$NAME/*.thy"
  [ -n "$DOCUMENT" ] && DOCUMENT_ROOT="$NAME/document/root.tex"
  USEDIR="\$(USEDIR)"
fi

if [ "$ISAMAKEFILE" != - -a -f "$ISAMAKEFILE" ]; then
  echo "keeping $PWD/$ISAMAKEFILE" >&2
else
  { echo
    echo "## targets"
    echo
    echo "default: $NAME"
    echo "images: $IMAGES"
    echo "test: $TEST"
    echo
    echo "all: images test"
    echo
    echo
    echo "## global settings"
    echo
    echo "SRC = \$(ISABELLE_HOME)/src"
    echo "OUT = \$(ISABELLE_OUTPUT)"
    echo "LOG = \$(OUT)/log"
    echo "USEDIR = \$(ISATOOL) usedir -i true -d dvi  ## -D document"
    echo
    echo
    echo "## $NAME"
    echo ""
    if [ -n "$PARENT" ]; then
      echo "$NAME: $LOGIC $TARGET"
      echo
      echo "$LOGIC:"
      echo -e "\t@cd \$(SRC)/$LOGIC; \$(ISATOOL) make $LOGIC"
      echo
      echo "$TARGET: \$(OUT)/$LOGIC $ROOT_ML $DOCUMENT_ROOT  ## $SOURCES"
      echo -e "\t@$USEDIR \$(OUT)/$LOGIC $NAME"
    else
      echo "$NAME: $TARGET"
      echo
      echo "$TARGET: $ROOT_ML $DOCUMENT_ROOT  ## $SOURCES"
      echo -e "\t@$USEDIR $LOGIC $NAME"
    fi
    echo
    echo
    echo "## clean"
    echo
    echo "clean:"
    echo -e "\t@rm -f $TARGET"
    echo
  } | {
    if [ -z "$ISAMAKEFILE" -o "$ISAMAKEFILE" = - ]; then
      cat
    else
      cat > "$ISAMAKEFILE"
    fi
  }
fi


# base directory

if [ -z "$BUILD" ]; then
  mkdir -p "$NAME" || fail "Bad directory: $PWD/$NAME"
  cd "$NAME"
fi

if [ -f ROOT.ML ]; then
  echo "keeping $PWD/ROOT.ML" >&2
else
  echo -e "\n(* use_thy \"YourTheory\"; *)\n" >ROOT.ML
fi


# document directory

if [ -n "$DOCUMENT" ]; then
  if [ -e document ]; then
    echo "keeping $PWD/document" >&2
  else
    mkdir document || fail "Bad directory: $PWD/document"
    cat >document/root.tex <<EOF

\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym,pdfsetup}

\begin{document}
\input{session}
\end{document}

EOF
  fi
fi