diff --git a/document-generator/Tools/DOF_mkroot b/document-generator/Tools/DOF_mkroot new file mode 100755 index 00000000..de3958a3 --- /dev/null +++ b/document-generator/Tools/DOF_mkroot @@ -0,0 +1,103 @@ +#/usr/bin/env bash +# Copyright (c) 2018 The University of Sheffield. All rights reserved. +# 2018 The University of Paris-Sud. All rights reserved. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions +# are met: +# 1. Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# 2. Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in +# the documentation and/or other materials provided with the +# distribution. +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS +# FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE +# COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, +# INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, +# BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; +# LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER +# CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT +# LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN +# ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE +# POSSIBILITY OF SUCH DAMAGE. +# +# SPDX-License-Identifier: BSD-2-Clause +# +# DESCRIPTION: prepare session root directory with DOF setup + +## diagnostics + +PRG="$(basename "$0")" + +function usage() +{ + echo + echo "Usage: isabelle $PRG [OPTIONS] [DIR]" + echo + echo " Options are:" + echo " -d enable document preparation" + echo " -n NAME alternative session name (default: DIR base name)" + echo + echo " Prepare session root DIR (default: current directory)." + echo + exit 1 +} + +function fail() +{ + echo "$1" >&2 + exit 2 +} + + +## process command line + +# options + +DOC="" +NAME="" + +while getopts "n:d" OPT +do + case "$OPT" in + d) + DOC="true" + ;; + n) + NAME="$OPTARG" + ;; + \?) + usage + ;; + esac +done + +shift $(($OPTIND - 1)) + + +# args + +if [ "$#" -eq 0 ]; then + DIR="." +elif [ "$#" -eq 1 ]; then + DIR="$1" + shift +else + usage +fi + + +[ -z "$NAME" ] && NAME="$(basename "$(cd "$DIR"; pwd -P)")" + +if [ "$DOC" = true ]; then + $ISABELLE_TOOL mkroot -d -n "$NAME" + TITLE=$(echo "$NAME" | tr _ - | tr -d '\\') + AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\') + cp "$ISABELLE_HOME_USER/DOF/document-template"/* document/ + sed -i -e "s//$AUTHOR/" -e "s//$TITLE/" document/root.tex +else + $ISABELLE_TOOL mkroot -n "$NAME" +fi