lib/Tools/yxml
author Lars Hupel <lars.hupel@mytum.de>
Thu, 06 Mar 2014 17:55:39 +0100
changeset 55946 5163ed3a38f5
parent 35022 c844b93dd147
permissions -rwxr-xr-x
tuned
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
26575
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
     2
#
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
     3
# Author: Makarius
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
     4
#
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
     5
# DESCRIPTION: simple XML to YXML converter
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
     6
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
     7
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
     8
PRG="$(basename "$0")"
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
     9
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
    10
function usage()
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
    11
{
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
    12
  echo
28650
a7ba12e0d3b7 tuned usage line;
wenzelm
parents: 26575
diff changeset
    13
  echo "Usage: isabelle $PRG"
26575
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
    14
  echo
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
    15
  echo "  Convert XML (stdin) to YXML (stdout)."
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
    16
  echo
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
    17
  exit 1
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
    18
}
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
    19
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
    20
function fail()
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
    21
{
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
    22
  echo "$1" >&2
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
    23
  exit 2
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
    24
}
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
    25
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
    26
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
    27
## process command line
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
    28
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
    29
[ "$#" -ne 0 ] && usage
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
    30
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
    31
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
    32
## main
042617a1c86c support for YXML notation -- XML done right;
wenzelm
parents:
diff changeset
    33
35022
c844b93dd147 modernized perl scripts: prefer standalone executables;
wenzelm
parents: 29143
diff changeset
    34
exec "$ISABELLE_HOME/lib/scripts/yxml"