lib/Tools/scalac
author wenzelm
Fri, 16 Jul 2021 13:18:54 +0200
changeset 74017 b4e6b82fdb9e
parent 73989 842fc354c031
child 74038 b4f57bfe82e7
permissions -rwxr-xr-x
more direct isabelle_scala_build: always enabled, no "Admin" requirement;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
44950
f60405791a1d added "isabelle scalac" convenience;
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
f60405791a1d added "isabelle scalac" convenience;
wenzelm
parents:
diff changeset
     2
#
f60405791a1d added "isabelle scalac" convenience;
wenzelm
parents:
diff changeset
     3
# Author: Makarius
f60405791a1d added "isabelle scalac" convenience;
wenzelm
parents:
diff changeset
     4
#
f60405791a1d added "isabelle scalac" convenience;
wenzelm
parents:
diff changeset
     5
# DESCRIPTION: invoke Scala compiler within the Isabelle environment
f60405791a1d added "isabelle scalac" convenience;
wenzelm
parents:
diff changeset
     6
74017
b4e6b82fdb9e more direct isabelle_scala_build: always enabled, no "Admin" requirement;
wenzelm
parents: 73989
diff changeset
     7
isabelle_scala_build || exit $?
44950
f60405791a1d added "isabelle scalac" convenience;
wenzelm
parents:
diff changeset
     8
73989
842fc354c031 more robust classpath: skip empty entries;
wenzelm
parents: 73988
diff changeset
     9
classpath "$ISABELLE_SETUP_CLASSPATH"; unset ISABELLE_SETUP_CLASSPATH
842fc354c031 more robust classpath: skip empty entries;
wenzelm
parents: 73988
diff changeset
    10
classpath "$CLASSPATH"; unset CLASSPATH
73988
678e1c9eb009 more robust: avoid duplicate classpath entries;
wenzelm
parents: 69126
diff changeset
    11
47115
1a05adae1cc9 more robust command invocation via ISABELLE_JDK_HOME or SCALA_HOME (NB: bash exec requires genuine executable, not function);
wenzelm
parents: 45385
diff changeset
    12
isabelle_scala scalac -Dfile.encoding=UTF-8 \
61294
2d3d26e9b191 renamed jvmpath to platform_path;
wenzelm
parents: 53576
diff changeset
    13
  -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@"