lib/Tools/display
author wenzelm
Tue, 04 Jun 2019 19:51:45 +0200
changeset 70324 005c1cdbfd3f
parent 54683 cf48ddc266e5
permissions -rwxr-xr-x
backout 34bc296374ee -- affects the raw_induct rule, e.g. relevant for AFP/Imperative_Insertion_Sort;

#!/usr/bin/env bash
#
# Author: Makarius
#
# DESCRIPTION: display document (in DVI or PDF format)


PRG="$(basename "$0")"

function usage()
{
  echo
  echo "Usage: isabelle $PRG DOCUMENT"
  echo
  echo "  Display DOCUMENT (in DVI or PDF format)."
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}


## main

[ "$#" -ne 1 -o "$1" = "-?" ] && usage

DOCUMENT="$1"; shift

[ -f "$DOCUMENT" ] || fail "Bad document: \"$DOCUMENT\""

case "$DOCUMENT" in
  *.dvi)
    exec "$DVI_VIEWER" "$DOCUMENT"
    ;;
  *.pdf)
    exec "$PDF_VIEWER" "$DOCUMENT"
    ;;
  *)
    fail "Unknown document type: \"$DOCUMENT\"";
esac