offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
authorwenzelm
Mon Nov 07 14:59:58 2011 +0100 (2011-11-07)
changeset 453857c1375ba1424
parent 45384 dffa657f0aa2
child 45388 121b2db078b1
offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
Admin/build
lib/Tools/java
lib/Tools/scala
lib/Tools/scalac
lib/scripts/java_ext_dirs
src/Pure/System/Java_Ext_Dirs.java
src/Tools/JVM/Java_Ext_Dirs.java
src/Tools/JVM/build
src/Tools/JVM/java_ext_dirs
src/Tools/JVM/java_ext_dirs.jar
     1.1 --- a/Admin/build	Mon Nov 07 14:23:50 2011 +0100
     1.2 +++ b/Admin/build	Mon Nov 07 14:59:58 2011 +0100
     1.3 @@ -84,7 +84,6 @@
     1.4  
     1.5  function build_jars ()
     1.6  {
     1.7 -  "$ISABELLE_TOOL" env "$ISABELLE_HOME/lib/scripts/java_ext_dirs" >/dev/null
     1.8    pushd "$ISABELLE_HOME/src/Pure" >/dev/null
     1.9    "$ISABELLE_TOOL" env ./build-jars "$@" || exit $?
    1.10    popd >/dev/null
     2.1 --- a/lib/Tools/java	Mon Nov 07 14:23:50 2011 +0100
     2.2 +++ b/lib/Tools/java	Mon Nov 07 14:59:58 2011 +0100
     2.3 @@ -22,5 +22,5 @@
     2.4  fi
     2.5  
     2.6  exec "$JAVA_EXE" -Dfile.encoding=UTF-8 $SERVER \
     2.7 -  "-Djava.ext.dirs=$("$ISABELLE_HOME/lib/scripts/java_ext_dirs")" "$@"
     2.8 +  "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@"
     2.9  
     3.1 --- a/lib/Tools/scala	Mon Nov 07 14:23:50 2011 +0100
     3.2 +++ b/lib/Tools/scala	Mon Nov 07 14:59:58 2011 +0100
     3.3 @@ -10,4 +10,4 @@
     3.4  
     3.5  CLASSPATH="$(jvmpath "$CLASSPATH")"
     3.6  exec "$SCALA_HOME/bin/scala" -Dfile.encoding=UTF-8 \
     3.7 -  "-Djava.ext.dirs=$("$ISABELLE_HOME/lib/scripts/java_ext_dirs")" "$@"
     3.8 +  "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@"
     4.1 --- a/lib/Tools/scalac	Mon Nov 07 14:23:50 2011 +0100
     4.2 +++ b/lib/Tools/scalac	Mon Nov 07 14:59:58 2011 +0100
     4.3 @@ -10,4 +10,4 @@
     4.4  
     4.5  CLASSPATH="$(jvmpath "$CLASSPATH")"
     4.6  exec "$SCALA_HOME/bin/scalac" -Dfile.encoding=UTF-8 \
     4.7 -  "-Djava.ext.dirs=$("$ISABELLE_HOME/lib/scripts/java_ext_dirs")" "$@"
     4.8 +  "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@"
     5.1 --- a/lib/scripts/java_ext_dirs	Mon Nov 07 14:23:50 2011 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,45 +0,0 @@
     5.4 -#!/usr/bin/env bash
     5.5 -#
     5.6 -# Author: Makarius
     5.7 -#
     5.8 -# Augment Java extension directories.
     5.9 -
    5.10 -## diagnostics
    5.11 -
    5.12 -function fail()
    5.13 -{
    5.14 -  echo "$1" >&2
    5.15 -  exit 2
    5.16 -}
    5.17 -
    5.18 -
    5.19 -## dependencies
    5.20 -
    5.21 -SOURCE="$ISABELLE_HOME/src/Pure/System/Java_Ext_Dirs.java"
    5.22 -
    5.23 -TARGET_DIR="$ISABELLE_HOME/lib/classes"
    5.24 -TARGET="$TARGET_DIR/java_ext_dirs.jar"
    5.25 -
    5.26 -if [ ! -e "$TARGET" -o "$SOURCE" -nt "$TARGET" ]; then
    5.27 -  mkdir -p "$TARGET_DIR" || fail "Bad directory: \"$TARGET_DIR\""
    5.28 -  pushd "$TARGET_DIR" >/dev/null
    5.29 -
    5.30 -  BUILD="build$$"
    5.31 -  TMP_JAR="java_ext_dirs$$.jar"
    5.32 -
    5.33 -  rm -rf "$BUILD" && mkdir "$BUILD"
    5.34 -  javac -d "$BUILD" -source 1.5 "$(jvmpath "$SOURCE")" || fail "Failed to compile sources"
    5.35 -  jar cf "$TMP_JAR" -C "$BUILD" . || fail "Failed to produce $TMP_JAR"
    5.36 -  mv "$TMP_JAR" "$TARGET"
    5.37 -  rm -rf "$BUILD"
    5.38 -
    5.39 -  popd >/dev/null
    5.40 -fi
    5.41 -
    5.42 -
    5.43 -## main
    5.44 -
    5.45 -JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
    5.46 -exec "$JAVA_EXE" -classpath "$(jvmpath "$TARGET")" isabelle.Java_Ext_Dirs \
    5.47 -  "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")"
    5.48 -
     6.1 --- a/src/Pure/System/Java_Ext_Dirs.java	Mon Nov 07 14:23:50 2011 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,22 +0,0 @@
     6.4 -/*  Title:      Pure/System/Java_Ext_Dirs.java
     6.5 -    Author:     Makarius
     6.6 -
     6.7 -Augment Java extension directories.
     6.8 -*/
     6.9 -
    6.10 -package isabelle;
    6.11 -
    6.12 -public class Java_Ext_Dirs
    6.13 -{
    6.14 -  public static void main(String [] args) {
    6.15 -    StringBuilder s = new StringBuilder();
    6.16 -    int i;
    6.17 -    for (i = 0; i < args.length; i++) {
    6.18 -      s.append(args[i]);
    6.19 -      s.append(System.getProperty("path.separator"));
    6.20 -    }
    6.21 -    s.append(System.getProperty("java.ext.dirs"));
    6.22 -    System.out.println(s.toString());
    6.23 -  }
    6.24 -}
    6.25 -
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Tools/JVM/Java_Ext_Dirs.java	Mon Nov 07 14:59:58 2011 +0100
     7.3 @@ -0,0 +1,22 @@
     7.4 +/*  Title:      Pure/System/Java_Ext_Dirs.java
     7.5 +    Author:     Makarius
     7.6 +
     7.7 +Augment Java extension directories.
     7.8 +*/
     7.9 +
    7.10 +package isabelle;
    7.11 +
    7.12 +public class Java_Ext_Dirs
    7.13 +{
    7.14 +  public static void main(String [] args) {
    7.15 +    StringBuilder s = new StringBuilder();
    7.16 +    int i;
    7.17 +    for (i = 0; i < args.length; i++) {
    7.18 +      s.append(args[i]);
    7.19 +      s.append(System.getProperty("path.separator"));
    7.20 +    }
    7.21 +    s.append(System.getProperty("java.ext.dirs"));
    7.22 +    System.out.println(s.toString());
    7.23 +  }
    7.24 +}
    7.25 +
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Tools/JVM/build	Mon Nov 07 14:59:58 2011 +0100
     8.3 @@ -0,0 +1,31 @@
     8.4 +#!/usr/bin/env bash
     8.5 +#
     8.6 +# Author: Makarius
     8.7 +#
     8.8 +# Offline build script for JVM tools.
     8.9 +
    8.10 +## diagnostics
    8.11 +
    8.12 +function fail()
    8.13 +{
    8.14 +  echo "$1" >&2
    8.15 +  exit 2
    8.16 +}
    8.17 +
    8.18 +
    8.19 +## build
    8.20 +
    8.21 +cd "$(dirname "$0")"
    8.22 +
    8.23 +SOURCE="Java_Ext_Dirs.java"
    8.24 +TARGET="java_ext_dirs.jar"
    8.25 +
    8.26 +BUILD="build_dir$$"
    8.27 +TMP_JAR="java_ext_dirs$$.jar"
    8.28 +
    8.29 +rm -rf "$BUILD" && mkdir "$BUILD"
    8.30 +javac -source 1.4 -target 1.4 -d "$BUILD" "$SOURCE" || fail "Failed to compile sources"
    8.31 +jar cf "$TMP_JAR" -C "$BUILD" . || fail "Failed to produce \"$TMP_JAR\""
    8.32 +mv "$TMP_JAR" "$TARGET"
    8.33 +rm -rf "$BUILD"
    8.34 +
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/Tools/JVM/java_ext_dirs	Mon Nov 07 14:59:58 2011 +0100
     9.3 @@ -0,0 +1,23 @@
     9.4 +#!/usr/bin/env bash
     9.5 +#
     9.6 +# Author: Makarius
     9.7 +#
     9.8 +# Augment Java extension directories.
     9.9 +
    9.10 +## diagnostics
    9.11 +
    9.12 +function fail()
    9.13 +{
    9.14 +  echo "$1" >&2
    9.15 +  exit 2
    9.16 +}
    9.17 +
    9.18 +[ -n "$ISABELLE_HOME" ] || fail "Missing Isabelle settings environment"
    9.19 +
    9.20 +
    9.21 +## main
    9.22 +
    9.23 +JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
    9.24 +exec "$JAVA_EXE" -classpath "$(jvmpath "$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs.jar")" \
    9.25 +  isabelle.Java_Ext_Dirs "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")"
    9.26 +
    10.1 Binary file src/Tools/JVM/java_ext_dirs.jar has changed