src/Tools/jEdit/makedist
author wenzelm
Tue, 21 Oct 2008 21:47:49 +0200
changeset 34332 545a73fee0e3
child 34379 c80f42933ac6
permissions -rwxr-xr-x
make Isabelle/jEdit distribution;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34332
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
     2
#
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
     3
# makedist -- make Isabelle/jEdit distribution
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
     4
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
     5
## self references
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
     6
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
     7
PRG=$(basename "$0")
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
     8
THIS=$(cd "$(dirname "$0")"; pwd)
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
     9
SUPER=$(cd "$THIS/.."; pwd)
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    10
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    11
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    12
## diagnostics
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    13
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    14
JEDIT_HOME="/home/isajedit/jedit-orig/4.3pre15"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    15
SCALA_HOME="/home/scala/current"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    16
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    17
function usage()
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    18
{
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    19
  echo
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    20
  echo "Usage: $PRG [OPTIONS]"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    21
  echo
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    22
  echo "  Options are:"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    23
  echo "    -j DIR       specify original jEdit distribution"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    24
  echo "                 (default: $JEDIT_HOME)"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    25
  echo "    -s DIR       specify Scala distribution"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    26
  echo "                 (default: $SCALA_HOME)"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    27
  echo
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    28
  echo "  Produce Isabelle/jEdit distribution from Netbeans build"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    29
  echo "  in $THIS/dist"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    30
  echo
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    31
  exit 1
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    32
}
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    33
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    34
fail()
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    35
{
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    36
  echo "$1" >&2
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    37
  exit 2
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    38
}
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    39
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    40
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    41
## process command line
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    42
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    43
# options
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    44
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    45
while getopts "j:s:" OPT
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    46
do
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    47
  case "$OPT" in
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    48
    j)
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    49
      JEDIT_HOME="$OPTARG"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    50
      ;;
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    51
    s)
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    52
      SCALA_HOME="$OPTARG"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    53
      ;;
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    54
    \?)
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    55
      usage
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    56
      ;;
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    57
  esac
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    58
done
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    59
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    60
shift $(($OPTIND - 1))
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    61
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    62
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    63
# args
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    64
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    65
[ "$#" -ne 0 ] && usage
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    66
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    67
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    68
## main
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    69
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    70
cd "$THIS/dist" || fail "Bad directory: $THIS/dist"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    71
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    72
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    73
# target name
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    74
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    75
VERSION=$(basename "$JEDIT_HOME")
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    76
JEDIT="jedit-${VERSION}"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    77
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    78
rm -rf "$JEDIT" jedit
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    79
mkdir "$JEDIT"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    80
ln -s "$JEDIT" jedit
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    81
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    82
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    83
# copy stuff
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    84
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    85
[ "$JEDIT_HOME/jedit.jar" ] || fail "Bad original jEdit directory: $JEDIT_HOME"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    86
cp -R "$JEDIT_HOME/." "$JEDIT/."
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    87
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    88
[ "$SCALA_HOME/lib/scala-library.jar" ] || fail "Bad Scala directory: $SCALA_HOME"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    89
cp "$SCALA_HOME/lib/scala-library.jar" "$JEDIT/jars/"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    90
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    91
cp -R "$THIS/dist-template/." "$JEDIT/."
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    92
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    93
cp Isabelle-jEdit.jar "$JEDIT/jars/isabelle.jar"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    94
cp lib/Pure.jar "$JEDIT/jars/isabelle-Pure.jar"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    95
cp lib/core-renderer.jar "$JEDIT/jars/"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    96
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    97
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    98
# build archive
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    99
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
   100
echo "${JEDIT}.tar.gz"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
   101
tar czf "${JEDIT}.tar.gz" "$JEDIT" jedit
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
   102
ln -sf "${JEDIT}.tar.gz" jedit.tar.gz