lib/Tools/mkdir

default for \<euro> is now based on eurosym package, instead of slightly exotic babel/greek (which causes problems with the Gentoo installation on lxbroy2);

+
−#!/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