forked from Isabelle_DOF/Isabelle_DOF
Support for local styles and templates.
This commit is contained in:
parent
e5874396c4
commit
d80d5b0538
|
@ -43,14 +43,14 @@ function usage()
|
||||||
echo " -n NAME alternative session name (default: DIR base name)"
|
echo " -n NAME alternative session name (default: DIR base name)"
|
||||||
echo " -o ONTOLOGY (default: $DEFAULT_ONTOLOGY)"
|
echo " -o ONTOLOGY (default: $DEFAULT_ONTOLOGY)"
|
||||||
echo " Available ontologies:"
|
echo " Available ontologies:"
|
||||||
for t in "$ISABELLE_HOME_USER/DOF/latex/"*.sty; do
|
for t in "$ISABELLE_DOF_HOME/src/ontologies"/*/*.sty; do
|
||||||
if [[ $t =~ DOF-(.*).sty$ ]]; then
|
if [[ $t =~ DOF-(.*).sty$ ]]; then
|
||||||
echo " * ${BASH_REMATCH[1]}"
|
echo " * ${BASH_REMATCH[1]}"
|
||||||
fi
|
fi
|
||||||
done
|
done
|
||||||
echo " -t TEMPLATE (default: $DEFAULT_TEMPLATE)"
|
echo " -t TEMPLATE (default: $DEFAULT_TEMPLATE)"
|
||||||
echo " Available document templates:"
|
echo " Available document templates:"
|
||||||
for t in "$ISABELLE_HOME_USER/DOF/document-template/"*.tex; do
|
for t in "$ISABELLE_DOF_HOME/src/document-templates/"*.tex; do
|
||||||
if [[ $t =~ root-(.*).tex$ ]]; then
|
if [[ $t =~ root-(.*).tex$ ]]; then
|
||||||
echo " * ${BASH_REMATCH[1]}"
|
echo " * ${BASH_REMATCH[1]}"
|
||||||
fi
|
fi
|
||||||
|
@ -90,7 +90,7 @@ do
|
||||||
NAME="$OPTARG"
|
NAME="$OPTARG"
|
||||||
;;
|
;;
|
||||||
o)
|
o)
|
||||||
if [ ! -f "$ISABELLE_HOME_USER/DOF/latex/DOF-$OPTARG.sty" ]; then
|
if [ ! -f "$ISABELLE_DOF_HOME/src/ontologies/*//DOF-$OPTARG.sty" ]; then
|
||||||
echo "ERROR: Ontology $OPTARG not available!"
|
echo "ERROR: Ontology $OPTARG not available!"
|
||||||
exit 1
|
exit 1
|
||||||
fi
|
fi
|
||||||
|
@ -98,7 +98,7 @@ do
|
||||||
;;
|
;;
|
||||||
t)
|
t)
|
||||||
TEMPLATE="$OPTARG"
|
TEMPLATE="$OPTARG"
|
||||||
if [ ! -f "$ISABELLE_HOME_USER/DOF/document-template/root-$TEMPLATE.tex" ]; then
|
if [ ! -f "$ISABELLE_DOF_HOME/src/document-templates/root-$TEMPLATE.tex" ]; then
|
||||||
echo "ERROR: Template $TEMPLATE not available!"
|
echo "ERROR: Template $TEMPLATE not available!"
|
||||||
exit 1
|
exit 1
|
||||||
fi
|
fi
|
||||||
|
|
Loading…
Reference in New Issue