lib/Tools/doc
author blanchet
Wed May 21 14:09:42 2014 +0200 (2014-05-21)
changeset 57037 c51132be8e16
parent 52444 2cfe6656d6d6
child 62438 42e13a4f52f5
permissions -rwxr-xr-x
avoid markup-generating @{make_string}
     1 #!/usr/bin/env bash
     2 #
     3 # Author: Markus Wenzel, TU Muenchen
     4 #
     5 # DESCRIPTION: view Isabelle documentation
     6 
     7 
     8 PRG="$(basename "$0")"
     9 
    10 function usage()
    11 {
    12   echo
    13   echo "Usage: isabelle $PRG [DOC ...]"
    14   echo
    15   echo "  View Isabelle documentation."
    16   echo
    17   exit 1
    18 }
    19 
    20 function fail()
    21 {
    22   echo "$1" >&2
    23   exit 2
    24 }
    25 
    26 
    27 ## args
    28 
    29 [ "$#" -eq 1 -a "$1" = "-?" ] && usage
    30 
    31 
    32 ## main
    33 
    34 isabelle_admin_build jars || exit $?
    35 
    36 "$ISABELLE_TOOL" java isabelle.Doc "$@"
    37