src/Tools/jEdit/makedist
author wenzelm
Mon, 07 Jun 2010 13:20:05 +0200
changeset 37355 1255ba99ed1e
parent 37218 ffd587207d5d
child 41513 0ffd5ea44078
permissions -rwxr-xr-x
no symlinks; tuned;
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
37355
1255ba99ed1e no symlinks;
wenzelm
parents: 37218
diff changeset
    14
JEDIT_HOME=""
34332
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    15
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    16
function usage()
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    17
{
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    18
  echo
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    19
  echo "Usage: $PRG [OPTIONS]"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    20
  echo
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    21
  echo "  Options are:"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    22
  echo "    -j DIR       specify original jEdit distribution"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    23
  echo
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    24
  echo "  Produce Isabelle/jEdit distribution from Netbeans build"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    25
  echo "  in $THIS/dist"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    26
  echo
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    27
  exit 1
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    28
}
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    29
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    30
fail()
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    31
{
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    32
  echo "$1" >&2
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    33
  exit 2
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    34
}
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    35
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    36
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    37
## process command line
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    38
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    39
# options
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    40
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    41
while getopts "j:s:" OPT
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    42
do
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    43
  case "$OPT" in
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    44
    j)
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    45
      JEDIT_HOME="$OPTARG"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    46
      ;;
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    47
    \?)
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    48
      usage
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    49
      ;;
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    50
  esac
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    51
done
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    52
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    53
shift $(($OPTIND - 1))
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    54
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    55
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    56
# args
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    57
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    58
[ "$#" -ne 0 ] && usage
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    59
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    60
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    61
## main
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    62
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    63
cd "$THIS/dist" || fail "Bad directory: $THIS/dist"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    64
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    65
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    66
# target name
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    67
37355
1255ba99ed1e no symlinks;
wenzelm
parents: 37218
diff changeset
    68
[ -z "$JEDIT_HOME" ] && fail "Unknown JEDIT_HOME"
1255ba99ed1e no symlinks;
wenzelm
parents: 37218
diff changeset
    69
34332
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    70
VERSION=$(basename "$JEDIT_HOME")
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    71
JEDIT="jedit-${VERSION}"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    72
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    73
rm -rf "$JEDIT" jedit
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    74
mkdir "$JEDIT"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    75
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    76
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    77
# copy stuff
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    78
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    79
[ "$JEDIT_HOME/jedit.jar" ] || fail "Bad original jEdit directory: $JEDIT_HOME"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    80
cp -R "$JEDIT_HOME/." "$JEDIT/."
34478
095e5cae6656 removed jEdit/build-support (belongs to src distribution);
wenzelm
parents: 34469
diff changeset
    81
rm -rf "$JEDIT/jEdit" "$JEDIT/build-support"
34332
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    82
34519
92f50a3b4a6a more robust copying of jars;
wenzelm
parents: 34512
diff changeset
    83
mkdir -p "$JEDIT/jars"
92f50a3b4a6a more robust copying of jars;
wenzelm
parents: 34512
diff changeset
    84
cp -R jars/. "$JEDIT/jars/."
34332
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    85
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    86
cp -R "$THIS/dist-template/." "$JEDIT/."
37218
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents: 34801
diff changeset
    87
cp "$THIS/README" "$JEDIT/."
34332
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    88
34419
30e49efdd4e3 basic isabelle mode setup;
wenzelm
parents: 34414
diff changeset
    89
perl -i -e 'while (<>) { if (m/NAME="javacc"/) {
34798
db0da30bca26 added isabelle-session mode for session.info files;
wenzelm
parents: 34646
diff changeset
    90
  print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,;
34801
89fa7e0e8e69 renamed session.info to session.root;
wenzelm
parents: 34798
diff changeset
    91
  print qq,<MODE NAME="isabelle-session" FILE="isabelle-session.xml" FILE_NAME_GLOB="session.root"/>\n\n,; }
34419
30e49efdd4e3 basic isabelle mode setup;
wenzelm
parents: 34414
diff changeset
    92
  print; }' "$JEDIT/modes/catalog"
30e49efdd4e3 basic isabelle mode setup;
wenzelm
parents: 34414
diff changeset
    93
34646
9560a458efed updated to jedit 4.3pre17 -- no longer provide separate ml.xml;
wenzelm
parents: 34519
diff changeset
    94
34332
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    95
# build archive
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    96
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    97
echo "${JEDIT}.tar.gz"
37355
1255ba99ed1e no symlinks;
wenzelm
parents: 37218
diff changeset
    98
tar czf "${JEDIT}.tar.gz" "$JEDIT"