# HG changeset patch
# User wenzelm
# Date 1003245944 -7200
# Node ID 9505bd5e9a3602c445196e68807e245a3ce3b174
# Parent  5f84c687ba06cc10036dbd9801ddd22a1935b2ab
option -o FILE --output to FILE (ps, eps, pdf);

diff -r 5f84c687ba06 -r 9505bd5e9a36 lib/Tools/browser
--- a/lib/Tools/browser	Tue Oct 16 17:24:33 2001 +0200
+++ b/lib/Tools/browser	Tue Oct 16 17:25:44 2001 +0200
@@ -16,22 +16,34 @@
   echo
   echo "  Options are:"
   echo "    -d           delete file after use"
+  echo "    -o FILE      output to FILE (ps, eps, pdf)"
   echo
   exit 1
 }
 
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+
 ## process command line
 
 # options
 
 DELETE=""
+OUTFILE=""
 
-while getopts "d" OPT
+while getopts "do:" OPT
 do
   case "$OPT" in
     d)
       DELETE=true
       ;;
+    o)
+      OUTFILE="$OPTARG"
+      ;;
     \?)
       usage
       ;;
@@ -55,7 +67,23 @@
   cd "$ISABELLE_BROWSER_INFO"
   exec java GraphBrowser.GraphBrowser
 else
-  java GraphBrowser.GraphBrowser "$GRAPHFILE"
+  case "$OUTFILE" in
+    *.pdf)
+      TMPOUTFILE="${OUTFILE%.pdf}.eps"
+      PDF=true
+      ;;
+    *)
+      TMPOUTFILE="$OUTFILE"
+      PDF=""
+      ;;
+  esac
+
+  java GraphBrowser.GraphBrowser "$GRAPHFILE" "$TMPOUTFILE"
+
+  if [ -n "$PDF" ]; then
+    "$ISABELLE_EPSTOPDF" "$TMPOUTFILE" || fail "Failed to produce pdf output"
+    rm -f "$TMPOUTFILE"
+  fi
+
   [ -n "$DELETE" ] && rm -f "$GRAPHFILE"
 fi
-