lib/Tools/yxml
author wenzelm
Tue Oct 21 20:18:07 2008 +0200 (2008-10-21)
changeset 28650 a7ba12e0d3b7
parent 26575 042617a1c86c
child 29143 72c960b2b83e
permissions -rwxr-xr-x
tuned usage line;
wenzelm@26575
     1
#!/usr/bin/env bash
wenzelm@26575
     2
#
wenzelm@26575
     3
# $Id$
wenzelm@26575
     4
# Author: Makarius
wenzelm@26575
     5
#
wenzelm@26575
     6
# DESCRIPTION: simple XML to YXML converter
wenzelm@26575
     7
wenzelm@26575
     8
wenzelm@26575
     9
PRG="$(basename "$0")"
wenzelm@26575
    10
wenzelm@26575
    11
function usage()
wenzelm@26575
    12
{
wenzelm@26575
    13
  echo
wenzelm@28650
    14
  echo "Usage: isabelle $PRG"
wenzelm@26575
    15
  echo
wenzelm@26575
    16
  echo "  Convert XML (stdin) to YXML (stdout)."
wenzelm@26575
    17
  echo
wenzelm@26575
    18
  exit 1
wenzelm@26575
    19
}
wenzelm@26575
    20
wenzelm@26575
    21
function fail()
wenzelm@26575
    22
{
wenzelm@26575
    23
  echo "$1" >&2
wenzelm@26575
    24
  exit 2
wenzelm@26575
    25
}
wenzelm@26575
    26
wenzelm@26575
    27
wenzelm@26575
    28
## process command line
wenzelm@26575
    29
wenzelm@26575
    30
[ "$#" -ne 0 ] && usage
wenzelm@26575
    31
wenzelm@26575
    32
wenzelm@26575
    33
## main
wenzelm@26575
    34
wenzelm@26575
    35
exec perl -w "$ISABELLE_HOME/lib/scripts/yxml.pl"