src/Tools/jEdit/makedist
author wenzelm
Thu Sep 02 00:48:07 2010 +0200 (2010-09-02)
changeset 38980 af73cf0dc31f
parent 37355 1255ba99ed1e
child 41513 0ffd5ea44078
permissions -rwxr-xr-x
turned show_question_marks into proper configuration option;
show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;
tuned;
wenzelm@34332
     1
#!/usr/bin/env bash
wenzelm@34332
     2
#
wenzelm@34332
     3
# makedist -- make Isabelle/jEdit distribution
wenzelm@34332
     4
wenzelm@34332
     5
## self references
wenzelm@34332
     6
wenzelm@34332
     7
PRG=$(basename "$0")
wenzelm@34332
     8
THIS=$(cd "$(dirname "$0")"; pwd)
wenzelm@34332
     9
SUPER=$(cd "$THIS/.."; pwd)
wenzelm@34332
    10
wenzelm@34332
    11
wenzelm@34332
    12
## diagnostics
wenzelm@34332
    13
wenzelm@37355
    14
JEDIT_HOME=""
wenzelm@34332
    15
wenzelm@34332
    16
function usage()
wenzelm@34332
    17
{
wenzelm@34332
    18
  echo
wenzelm@34332
    19
  echo "Usage: $PRG [OPTIONS]"
wenzelm@34332
    20
  echo
wenzelm@34332
    21
  echo "  Options are:"
wenzelm@34332
    22
  echo "    -j DIR       specify original jEdit distribution"
wenzelm@34332
    23
  echo
wenzelm@34332
    24
  echo "  Produce Isabelle/jEdit distribution from Netbeans build"
wenzelm@34332
    25
  echo "  in $THIS/dist"
wenzelm@34332
    26
  echo
wenzelm@34332
    27
  exit 1
wenzelm@34332
    28
}
wenzelm@34332
    29
wenzelm@34332
    30
fail()
wenzelm@34332
    31
{
wenzelm@34332
    32
  echo "$1" >&2
wenzelm@34332
    33
  exit 2
wenzelm@34332
    34
}
wenzelm@34332
    35
wenzelm@34332
    36
wenzelm@34332
    37
## process command line
wenzelm@34332
    38
wenzelm@34332
    39
# options
wenzelm@34332
    40
wenzelm@34332
    41
while getopts "j:s:" OPT
wenzelm@34332
    42
do
wenzelm@34332
    43
  case "$OPT" in
wenzelm@34332
    44
    j)
wenzelm@34332
    45
      JEDIT_HOME="$OPTARG"
wenzelm@34332
    46
      ;;
wenzelm@34332
    47
    \?)
wenzelm@34332
    48
      usage
wenzelm@34332
    49
      ;;
wenzelm@34332
    50
  esac
wenzelm@34332
    51
done
wenzelm@34332
    52
wenzelm@34332
    53
shift $(($OPTIND - 1))
wenzelm@34332
    54
wenzelm@34332
    55
wenzelm@34332
    56
# args
wenzelm@34332
    57
wenzelm@34332
    58
[ "$#" -ne 0 ] && usage
wenzelm@34332
    59
wenzelm@34332
    60
wenzelm@34332
    61
## main
wenzelm@34332
    62
wenzelm@34332
    63
cd "$THIS/dist" || fail "Bad directory: $THIS/dist"
wenzelm@34332
    64
wenzelm@34332
    65
wenzelm@34332
    66
# target name
wenzelm@34332
    67
wenzelm@37355
    68
[ -z "$JEDIT_HOME" ] && fail "Unknown JEDIT_HOME"
wenzelm@37355
    69
wenzelm@34332
    70
VERSION=$(basename "$JEDIT_HOME")
wenzelm@34332
    71
JEDIT="jedit-${VERSION}"
wenzelm@34332
    72
wenzelm@34332
    73
rm -rf "$JEDIT" jedit
wenzelm@34332
    74
mkdir "$JEDIT"
wenzelm@34332
    75
wenzelm@34332
    76
wenzelm@34332
    77
# copy stuff
wenzelm@34332
    78
wenzelm@34332
    79
[ "$JEDIT_HOME/jedit.jar" ] || fail "Bad original jEdit directory: $JEDIT_HOME"
wenzelm@34332
    80
cp -R "$JEDIT_HOME/." "$JEDIT/."
wenzelm@34478
    81
rm -rf "$JEDIT/jEdit" "$JEDIT/build-support"
wenzelm@34332
    82
wenzelm@34519
    83
mkdir -p "$JEDIT/jars"
wenzelm@34519
    84
cp -R jars/. "$JEDIT/jars/."
wenzelm@34332
    85
wenzelm@34332
    86
cp -R "$THIS/dist-template/." "$JEDIT/."
wenzelm@37218
    87
cp "$THIS/README" "$JEDIT/."
wenzelm@34332
    88
wenzelm@34419
    89
perl -i -e 'while (<>) { if (m/NAME="javacc"/) {
wenzelm@34798
    90
  print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,;
wenzelm@34801
    91
  print qq,<MODE NAME="isabelle-session" FILE="isabelle-session.xml" FILE_NAME_GLOB="session.root"/>\n\n,; }
wenzelm@34419
    92
  print; }' "$JEDIT/modes/catalog"
wenzelm@34419
    93
wenzelm@34646
    94
wenzelm@34332
    95
# build archive
wenzelm@34332
    96
wenzelm@34332
    97
echo "${JEDIT}.tar.gz"
wenzelm@37355
    98
tar czf "${JEDIT}.tar.gz" "$JEDIT"