src/Tools/jEdit/makedist
author immler@in.tum.de
Sun, 01 Feb 2009 13:38:51 +0100
changeset 34515 3be515f1379d
parent 34512 14d70378f1c7
child 34519 92f50a3b4a6a
permissions -rwxr-xr-x
use FontMetrics.getMaxAdvance if available; 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
34414
de921b3cb263 updated to 4.3pre16;
wenzelm
parents: 34413
diff changeset
    14
JEDIT_HOME="/home/isajedit/jedit-orig/4.3pre16"
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 "                 (default: $JEDIT_HOME)"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    24
  echo
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    25
  echo "  Produce Isabelle/jEdit distribution from Netbeans build"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    26
  echo "  in $THIS/dist"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    27
  echo
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    28
  exit 1
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    29
}
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    30
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    31
fail()
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    32
{
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    33
  echo "$1" >&2
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    34
  exit 2
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
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    38
## process command line
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    39
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    40
# options
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    41
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    42
while getopts "j:s:" OPT
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    43
do
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    44
  case "$OPT" in
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    45
    j)
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    46
      JEDIT_HOME="$OPTARG"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    47
      ;;
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    48
    \?)
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    49
      usage
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    50
      ;;
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    51
  esac
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    52
done
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    53
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    54
shift $(($OPTIND - 1))
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    55
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    56
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    57
# args
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    58
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    59
[ "$#" -ne 0 ] && usage
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    60
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    61
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    62
## main
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    63
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    64
cd "$THIS/dist" || fail "Bad directory: $THIS/dist"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    65
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    66
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    67
# target name
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    68
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    69
VERSION=$(basename "$JEDIT_HOME")
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    70
JEDIT="jedit-${VERSION}"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    71
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    72
rm -rf "$JEDIT" jedit
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    73
mkdir "$JEDIT"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    74
ln -s "$JEDIT" 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
34512
14d70378f1c7 modified netbeans build such that dist can be used as settings-directory for jedit;
immler@in.tum.de
parents: 34478
diff changeset
    83
cp -R jars "$JEDIT/jars"
34332
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    84
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    85
cp -R "$THIS/dist-template/." "$JEDIT/."
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    86
34419
30e49efdd4e3 basic isabelle mode setup;
wenzelm
parents: 34414
diff changeset
    87
perl -i -e 'while (<>) { if (m/NAME="javacc"/) {
30e49efdd4e3 basic isabelle mode setup;
wenzelm
parents: 34414
diff changeset
    88
  print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,; }
30e49efdd4e3 basic isabelle mode setup;
wenzelm
parents: 34414
diff changeset
    89
  print; }' "$JEDIT/modes/catalog"
30e49efdd4e3 basic isabelle mode setup;
wenzelm
parents: 34414
diff changeset
    90
34332
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    91
# build archive
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    92
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    93
echo "${JEDIT}.tar.gz"
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    94
tar czf "${JEDIT}.tar.gz" "$JEDIT" jedit
545a73fee0e3 make Isabelle/jEdit distribution;
wenzelm
parents:
diff changeset
    95
ln -sf "${JEDIT}.tar.gz" jedit.tar.gz