# HG changeset patch
# User wenzelm
# Date 939292064 -7200
# Node ID c7b2f68c79fb75513ebb6c1061b91e7733d8c661
# Parent  cc8e2263be65e4e3be1e0b6066cc579d77295965
Isabelle wrapper for LaTeX (and friends);

diff -r cc8e2263be65 -r c7b2f68c79fb lib/Tools/latex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/latex	Thu Oct 07 12:27:44 1999 +0200
@@ -0,0 +1,92 @@
+#!/bin/bash
+#
+# $Id$
+#
+# DESCRIPTION: Isabelle wrapper for LaTeX (and friends)
+
+
+PRG=$(basename $0)
+
+function usage()
+{
+  echo
+  echo "Usage: $PRG [OPTIONS] FILE"
+  echo
+  echo "  Options are:"
+  echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz, pdf"
+  echo
+  echo
+  echo "  Run LaTeX (and related tools) within the Isabelle environment."
+  echo
+  exit 1
+}
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+
+## process command line
+
+# options
+
+OUTFORMAT=dvi
+
+while getopts "o:" OPT
+do
+  case "$OPT" in
+    o)
+      OUTFORMAT="$OPTARG"
+      ;;
+    \?)
+      usage
+      ;;
+  esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+FILE=""
+[ $# -ge 1 ] && { FILE="$1"; shift; }
+
+[ $# -ne 0 -o -z "$FILE" ] && usage
+
+
+## main
+
+DIR=$(dirname "$FILE")
+if [ "$DIR" = "." ]; then
+  FILEBASE=$(basename "$FILE" .tex)
+else
+  FILEBASE=$(dirname "$FILE")/$(basename "$FILE" .tex)
+fi
+
+case "$OUTFORMAT" in
+  dvi)
+    $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"
+    ;;
+  dvi.gz)
+    $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"
+    gzip -f "$FILEBASE.dvi"
+    ;;
+  ps)
+    $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"
+    $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi"
+    ;;
+  ps.gz)
+    $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"
+    $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi"
+    gzip -f "$FILEBASE.ps"
+    ;;
+  pdf)
+    $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"
+    ;;
+  *)
+    fail "Bad output format '$OUTFORMAT'"
+    ;;
+esac