Removed scala converter.

This commit is contained in:
Achim D. Brucker 2018-09-18 14:28:06 +01:00
parent 1382d7c600
commit 85f332fe5e
2 changed files with 2 additions and 33 deletions

View File

@ -34,7 +34,7 @@ set -e
ROOT_NAME="root_$NAME"
[ ! -f "$DIR/$ROOT_NAME.tex" ] && ROOT_NAME="root"
if [ ! -f $ISABELLE_HOME_USER/DOF/lib/dof_latex_converter.jar ]; then
if [ ! -f $ISABELLE_HOME_USER/DOF/latex/DOF-core.sty ]; then
echo ""
echo "Warning: Isabelle DOF not installed"
echo "========"
@ -49,26 +49,6 @@ if [ ! -f $ISABELLE_HOME_USER/DOF/lib/dof_latex_converter.jar ]; then
exit 1
fi
VERSION=$($ISABELLE_TOOL scala $ISABELLE_HOME_USER/DOF/lib/dof_latex_converter.jar -v) || true
if [ "$VERSION" != "<VERSION>" ]; then
echo ""
echo "Warning: Isabelle DOF version mismatch"
echo "========"
echo " Build script version: <VERSION>"
echo " DOF LaTeX Converter version: $VERSION"
echo " Please take one of the following actions:"
echo " * If the build script is more recent than the converter, "
echo " then update the build script from your your Isabelle DOF"
echo " installation:"
echo " $ISABELLE_HOME_USER/DOF/document-template/build"
echo " * If the converter is more recent than the build script,"
echo " please update your Isabelle DOF installation."
exit 1
fi
$ISABELLE_TOOL scala $ISABELLE_HOME_USER/DOF/lib/dof_latex_converter.jar .
cp $ISABELLE_HOME_USER/DOF/latex/*.sty .
$ISABELLE_TOOL latex -o sty "$ROOT_NAME.tex" && \

13
install
View File

@ -57,21 +57,10 @@ else
echo "Registering tools in Tools already registered in $DIR/settings"
fi
# Build Scala lib
(cd $GEN_DIR/converter; ./build $ISABELLE)
DIR="$ISABELLE_HOME_USER/DOF/lib"
echo "Installing library in $DIR"
mkdir -p "$DIR"
cp $GEN_DIR/converter/bin/*.jar "$DIR"
VERSION=$($ISABELLE scala $GEN_DIR/converter/bin/*.jar -v) || true
DIR="$ISABELLE_HOME_USER/DOF/document-template"
echo "Installing document templates in $DIR"
mkdir -p "$DIR"
cp $GEN_DIR/document-template/* "$DIR"
sed -i -e "s/<VERSION>/$VERSION/" "$DIR"/build
DIR="$ISABELLE_HOME_USER/DOF/latex"
@ -79,4 +68,4 @@ echo "Installing LaTeX styles in $DIR"
mkdir -p "$DIR"
cp $GEN_DIR/latex/*.sty "$DIR"
echo "Installation of $VERSION successful."
echo "Installation successful."