diff -r 9362fcd0318c -r 892061142ba6 lib/Tools/mkdir
--- a/lib/Tools/mkdir	Fri May 17 17:45:51 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,288 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# DESCRIPTION: prepare logic session directory
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: isabelle $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 "    -q           quiet mode"
-  echo
-  echo "  Prepare session directory, including IsaMakefile and document source"
-  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=""
-QUIET=""
-
-while getopts "I:Pbq" OPT
-do
-  case "$OPT" in
-    I)
-      ISAMAKEFILE="$OPTARG"
-      ;;
-    P)
-      PARENT=true
-      ;;
-    b)
-      BUILD=true
-      ;;
-    q)
-      QUIET=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
-
-[ -z "$QUIET" ] && echo "Preparing session \"$NAME\" ..."
-
-
-# IsaMakefile
-
-mkdir -p "$DIR" || fail "Bad directory: $DIR"
-cd "$DIR"
-
-DOCUMENT_ROOT=""
-VERBOSE=""
-[ -z "$QUIET" ] && VERBOSE="-v true "
-
-if [ -n "$BUILD" ]; then
-  IMAGES="$NAME"
-  TEST=""
-  TARGET="\$(OUT)/$NAME"
-  ROOT_ML="ROOT.ML"
-  SOURCES="*.thy"
-  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"
-  DOCUMENT_ROOT="$NAME/document/root.tex"
-  USEDIR="\$(USEDIR)"
-fi
-
-if [ "$ISAMAKEFILE" != - -a -f "$ISAMAKEFILE" ]; then
-  echo "keeping $DIR/$ISAMAKEFILE" >&2
-else
-  [ -z "$QUIET" -a -n "$ISAMAKEFILE" -a "$ISAMAKEFILE" != - ] && \
-    echo "creating $DIR/$ISAMAKEFILE" >&2
-  { 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
-    echo "USEDIR = \$(ISABELLE_TOOL) usedir ${VERBOSE}-i true -d $ISABELLE_DOC_FORMAT  ## -D generated"
-    echo
-    echo
-    echo "## $NAME"
-    echo ""
-    if [ -n "$PARENT" ]; then
-      echo "$NAME: $LOGIC $TARGET"
-      echo
-      echo "$LOGIC:"
-      echo -e "\t@cd \$(SRC)/$LOGIC; \$(ISABELLE_TOOL) 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"
-  } | {
-    if [ -z "$ISAMAKEFILE" -o "$ISAMAKEFILE" = - ]; then
-      cat
-    else
-      cat > "$ISAMAKEFILE"
-    fi
-  }
-fi
-
-
-# base directory
-
-if [ -z "$BUILD" ]; then
-  mkdir -p "$NAME" || fail "Bad directory: $DIR/$NAME"
-  cd "$NAME"
-  PREFIX="$DIR/$NAME"
-else
-  PREFIX="$DIR"
-fi
-
-if [ -f ROOT.ML ]; then
-  echo "keeping $PREFIX/ROOT.ML" >&2
-else
-  [ -z "$QUIET" ] && echo "creating $PREFIX/ROOT.ML" >&2
-  cat >ROOT.ML <<EOF
-(*
-  no_document use_thys ["This_Theory1", "This_Theory2"];
-  use_thys ["That_Theory1", "That_Theory2", "That_Theory3"];
-*)
-EOF
-fi
-
-
-# document directory
-
-if [ -e document ]; then
-  echo "keeping $PREFIX/document" >&2
-else
-  [ -z "$QUIET" ] && echo "creating $PREFIX/document" >&2
-  mkdir document || fail "Bad directory: $PREFIX/document"
-
-  [ -z "$QUIET" ] && echo "creating $PREFIX/document/root.tex" >&2
-  TITLE=$(echo "$NAME" | tr _ - | tr -d '\\')
-  AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\')
-  cat >document/root.tex <<EOF
-\documentclass[11pt,a4paper]{article}
-\usepackage{isabelle,isabellesym}
-
-% further packages required for unusual symbols (see also
-% isabellesym.sty), use only when needed
-
-%\usepackage{amssymb}
-  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
-  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
-  %\<triangleq>, \<yen>, \<lozenge>
-
-%\usepackage{eurosym}
-  %for \<euro>
-
-%\usepackage[only,bigsqcap]{stmaryrd}
-  %for \<Sqinter>
-
-%\usepackage{eufrak}
-  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
-
-%\usepackage{textcomp}
-  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
-  %\<currency>
-
-% this should be the last package used
-\usepackage{pdfsetup}
-
-% urls in roman style, theory text in math-similar italics
-\urlstyle{rm}
-\isabellestyle{it}
-
-% for uniform font size
-%\renewcommand{\isastyle}{\isastyleminor}
-
-
-\begin{document}
-
-\title{$TITLE}
-\author{$AUTHOR}
-\maketitle
-
-\tableofcontents
-
-% sane default for proof documents
-\parindent 0pt\parskip 0.5ex
-
-% generated text of all theories
-\input{session}
-
-% optional bibliography
-%\bibliographystyle{abbrv}
-%\bibliography{root}
-
-\end{document}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End:
-EOF
-fi
-
-
-# notes
-
-if [ -z "$QUIET" ]; then
-  cat >&2 <<EOF
-
-Notes:
-
-  * 'isabelle make' processes the session (including document preparation)
-
-  * $DIR/IsaMakefile contains compilation options and file dependencies
-
-  * $PREFIX/document/root.tex contains the LaTeX master document setup
-
-  * $PREFIX/ROOT.ML needs to contain ML code to load all theories
-
-EOF
-fi