lib/Tools/display
author haftmann
Sun, 16 Oct 2016 09:31:04 +0200
changeset 64240 eabf80376aab
parent 54683 cf48ddc266e5
permissions -rwxr-xr-x
more standardized names
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14930
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
     2
#
54683
cf48ddc266e5 clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents: 50197
diff changeset
     3
# Author: Makarius
14930
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
     4
#
15218
39747a9e3c37 display pdf as well as dvi
kleing
parents: 15010
diff changeset
     5
# DESCRIPTION: display document (in DVI or PDF format)
14930
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
     6
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
     7
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
     8
PRG="$(basename "$0")"
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
     9
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    10
function usage()
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    11
{
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    12
  echo
54683
cf48ddc266e5 clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents: 50197
diff changeset
    13
  echo "Usage: isabelle $PRG DOCUMENT"
14930
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    14
  echo
54683
cf48ddc266e5 clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents: 50197
diff changeset
    15
  echo "  Display DOCUMENT (in DVI or PDF format)."
14930
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    16
  echo
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    17
  exit 1
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    18
}
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    19
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    20
function fail()
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    21
{
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    22
  echo "$1" >&2
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    23
  exit 2
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    24
}
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    25
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    26
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    27
## main
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    28
54683
cf48ddc266e5 clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents: 50197
diff changeset
    29
[ "$#" -ne 1 -o "$1" = "-?" ] && usage
cf48ddc266e5 clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents: 50197
diff changeset
    30
cf48ddc266e5 clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents: 50197
diff changeset
    31
DOCUMENT="$1"; shift
cf48ddc266e5 clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents: 50197
diff changeset
    32
cf48ddc266e5 clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents: 50197
diff changeset
    33
[ -f "$DOCUMENT" ] || fail "Bad document: \"$DOCUMENT\""
14930
24a0b2dd9be6 display document (in DVI format)
wenzelm
parents:
diff changeset
    34
54683
cf48ddc266e5 clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents: 50197
diff changeset
    35
case "$DOCUMENT" in
cf48ddc266e5 clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents: 50197
diff changeset
    36
  *.dvi)
cf48ddc266e5 clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents: 50197
diff changeset
    37
    exec "$DVI_VIEWER" "$DOCUMENT"
cf48ddc266e5 clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents: 50197
diff changeset
    38
    ;;
cf48ddc266e5 clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents: 50197
diff changeset
    39
  *.pdf)
cf48ddc266e5 clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents: 50197
diff changeset
    40
    exec "$PDF_VIEWER" "$DOCUMENT"
cf48ddc266e5 clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents: 50197
diff changeset
    41
    ;;
cf48ddc266e5 clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents: 50197
diff changeset
    42
  *)
cf48ddc266e5 clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents: 50197
diff changeset
    43
    fail "Unknown document type: \"$DOCUMENT\"";
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15223
diff changeset
    44
esac
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15223
diff changeset
    45