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;
     1 #!/usr/bin/env bash
     2 #
     3 # makedist -- make Isabelle/jEdit distribution
     4 
     5 ## self references
     6 
     7 PRG=$(basename "$0")
     8 THIS=$(cd "$(dirname "$0")"; pwd)
     9 SUPER=$(cd "$THIS/.."; pwd)
    10 
    11 
    12 ## diagnostics
    13 
    14 JEDIT_HOME=""
    15 
    16 function usage()
    17 {
    18   echo
    19   echo "Usage: $PRG [OPTIONS]"
    20   echo
    21   echo "  Options are:"
    22   echo "    -j DIR       specify original jEdit distribution"
    23   echo
    24   echo "  Produce Isabelle/jEdit distribution from Netbeans build"
    25   echo "  in $THIS/dist"
    26   echo
    27   exit 1
    28 }
    29 
    30 fail()
    31 {
    32   echo "$1" >&2
    33   exit 2
    34 }
    35 
    36 
    37 ## process command line
    38 
    39 # options
    40 
    41 while getopts "j:s:" OPT
    42 do
    43   case "$OPT" in
    44     j)
    45       JEDIT_HOME="$OPTARG"
    46       ;;
    47     \?)
    48       usage
    49       ;;
    50   esac
    51 done
    52 
    53 shift $(($OPTIND - 1))
    54 
    55 
    56 # args
    57 
    58 [ "$#" -ne 0 ] && usage
    59 
    60 
    61 ## main
    62 
    63 cd "$THIS/dist" || fail "Bad directory: $THIS/dist"
    64 
    65 
    66 # target name
    67 
    68 [ -z "$JEDIT_HOME" ] && fail "Unknown JEDIT_HOME"
    69 
    70 VERSION=$(basename "$JEDIT_HOME")
    71 JEDIT="jedit-${VERSION}"
    72 
    73 rm -rf "$JEDIT" jedit
    74 mkdir "$JEDIT"
    75 
    76 
    77 # copy stuff
    78 
    79 [ "$JEDIT_HOME/jedit.jar" ] || fail "Bad original jEdit directory: $JEDIT_HOME"
    80 cp -R "$JEDIT_HOME/." "$JEDIT/."
    81 rm -rf "$JEDIT/jEdit" "$JEDIT/build-support"
    82 
    83 mkdir -p "$JEDIT/jars"
    84 cp -R jars/. "$JEDIT/jars/."
    85 
    86 cp -R "$THIS/dist-template/." "$JEDIT/."
    87 cp "$THIS/README" "$JEDIT/."
    88 
    89 perl -i -e 'while (<>) { if (m/NAME="javacc"/) {
    90   print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,;
    91   print qq,<MODE NAME="isabelle-session" FILE="isabelle-session.xml" FILE_NAME_GLOB="session.root"/>\n\n,; }
    92   print; }' "$JEDIT/modes/catalog"
    93 
    94 
    95 # build archive
    96 
    97 echo "${JEDIT}.tar.gz"
    98 tar czf "${JEDIT}.tar.gz" "$JEDIT"