more robust "isabelle build_scala" as separate tool;
authorwenzelm
Sun, 18 Jul 2021 12:48:31 +0200
changeset 74038 b4f57bfe82e7
parent 74037 c13198575f75
child 74039 8c213672f6f3
more robust "isabelle build_scala" as separate tool;
Admin/build_history
Admin/build_release
Admin/cronjob/main
bin/isabelle
lib/Tools/components
lib/Tools/console
lib/Tools/java
lib/Tools/scala
lib/Tools/scala_build
lib/Tools/scalac
lib/scripts/getfunctions
src/Tools/GraphBrowser/lib/Tools/browser
src/Tools/jEdit/lib/Tools/jedit
--- a/Admin/build_history	Sat Jul 17 23:09:54 2021 +0200
+++ b/Admin/build_history	Sun Jul 18 12:48:31 2021 +0200
@@ -5,5 +5,5 @@
 unset CDPATH
 THIS="$(cd "$(dirname "$0")"; pwd)"
 
-env ISABELLE_SETUP_CLASSPATH_SKIP=true "$THIS/../bin/isabelle" java isabelle.setup.Setup build > /dev/null || exit $?
-exec "$THIS/../bin/isabelle_java" isabelle.Build_History "$@"
+"$THIS/../bin/isabelle" scala_build -q || exit $?
+"$THIS/../bin/isabelle_java" isabelle.Build_History "$@"
--- a/Admin/build_release	Sat Jul 17 23:09:54 2021 +0200
+++ b/Admin/build_release	Sun Jul 18 12:48:31 2021 +0200
@@ -5,5 +5,5 @@
 unset CDPATH
 THIS="$(cd "$(dirname "$0")"; pwd)"
 
-env ISABELLE_SETUP_CLASSPATH_SKIP=true "$THIS/../bin/isabelle" java isabelle.setup.Setup build > /dev/null || exit $?
-exec "$THIS/../bin/isabelle_java" isabelle.Build_Release "$@"
+"$THIS/../bin/isabelle" scala_build -q || exit $?
+"$THIS/../bin/isabelle_java" isabelle.Build_Release "$@"
--- a/Admin/cronjob/main	Sat Jul 17 23:09:54 2021 +0200
+++ b/Admin/cronjob/main	Sun Jul 18 12:48:31 2021 +0200
@@ -8,5 +8,5 @@
 source "$HOME/.bashrc"
 
 export ISABELLE_IDENTIFIER="cronjob"
-env ISABELLE_SETUP_CLASSPATH_SKIP=true "$THIS/../../bin/isabelle" java isabelle.setup.Setup build > /dev/null || exit $?
-exec "$THIS/../../bin/isabelle_java" isabelle.Isabelle_Cronjob "$@"
+"$THIS/../../bin/isabelle" scala_build -q || exit $?
+"$THIS/../../bin/isabelle_java" isabelle.Isabelle_Cronjob "$@"
--- a/bin/isabelle	Sat Jul 17 23:09:54 2021 +0200
+++ b/bin/isabelle	Sun Jul 18 12:48:31 2021 +0200
@@ -45,7 +45,7 @@
 
 ## internal tool or usage (Scala)
 
-isabelle_scala_build || exit $?
+"$ISABELLE_HOME/lib/Tools/scala_build" || exit $?
 
 eval "declare -a JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS)"
 exec isabelle java "${JAVA_ARGS[@]}" isabelle.Isabelle_Tool "$@"
--- a/lib/Tools/components	Sat Jul 17 23:09:54 2021 +0200
+++ b/lib/Tools/components	Sun Jul 18 12:48:31 2021 +0200
@@ -127,7 +127,7 @@
   echo "Missing components:"
   for NAME in "${MISSING_COMPONENTS[@]}"; do echo "  $NAME"; done
 elif [ "${#UPDATE_COMPONENTS[@]}" -ne 0 ]; then
-  isabelle_scala_build || exit $?
+  isabelle scala_build || exit $?
   exec isabelle java isabelle.Components "${UPDATE_COMPONENTS[@]}"
 else
   for NAME in "${SELECTED_COMPONENTS[@]}"
--- a/lib/Tools/console	Sat Jul 17 23:09:54 2021 +0200
+++ b/lib/Tools/console	Sun Jul 18 12:48:31 2021 +0200
@@ -4,7 +4,7 @@
 #
 # DESCRIPTION: raw ML process (interactive mode)
 
-isabelle_scala_build || exit $?
+isabelle scala_build || exit $?
 
 eval "declare -a JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS)"
 
--- a/lib/Tools/java	Sat Jul 17 23:09:54 2021 +0200
+++ b/lib/Tools/java	Sun Jul 18 12:48:31 2021 +0200
@@ -6,11 +6,7 @@
 
 eval "declare -a JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS)"
 
-if [ -z "$ISABELLE_SETUP_CLASSPATH_SKIP" -o "$ISABELLE_SETUP_CLASSPATH_SKIP" = "false" ]
-then
-  classpath "$ISABELLE_SETUP_CLASSPATH"; unset ISABELLE_SETUP_CLASSPATH
-fi
-
+classpath "$ISABELLE_SETUP_CLASSPATH"; unset ISABELLE_SETUP_CLASSPATH
 classpath "$CLASSPATH"; unset CLASSPATH
 
 isabelle_java java "${JAVA_ARGS[@]}" \
--- a/lib/Tools/scala	Sat Jul 17 23:09:54 2021 +0200
+++ b/lib/Tools/scala	Sun Jul 18 12:48:31 2021 +0200
@@ -4,7 +4,7 @@
 #
 # DESCRIPTION: invoke Scala within the Isabelle environment
 
-isabelle_scala_build || exit $?
+isabelle scala_build || exit $?
 
 eval "declare -a JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS)"
 declare -a SCALA_ARGS=()
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/scala_build	Sun Jul 18 12:48:31 2021 +0200
@@ -0,0 +1,70 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: build Isabelle/Scala/Java components
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+  echo
+  echo "Usage: isabelle $PRG [OPTIONS]"
+  echo
+  echo "  Options are:"
+  echo "    -f           force fresh build"
+  echo "    -q           quiet mode: suppress stdout/stderr"
+  echo
+  exit 1
+}
+
+
+## process command line
+
+COMMAND="build"
+QUIET=""
+
+while getopts "fq" OPT
+do
+  case "$OPT" in
+    f)
+      COMMAND="build_fresh"
+      ;;
+    q)
+      QUIET="true"
+      ;;
+    \?)
+      usage
+      ;;
+  esac
+done
+
+shift $(($OPTIND - 1))
+
+[ "$#" -ne 0 ] && usage
+
+
+## main
+
+#remove historic material
+rm -rf \
+  "$ISABELLE_HOME/lib/classes/Pure.jar" \
+  "$ISABELLE_HOME/lib/classes/Pure.shasum" \
+  "$ISABELLE_HOME/src/Tools/jEdit/dist"
+
+classpath "$CLASSPATH"; unset CLASSPATH
+
+eval "declare -a JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS)"
+
+JAVA_ARGS["${#JAVA_ARGS[@]}"]="-classpath"
+JAVA_ARGS["${#JAVA_ARGS[@]}"]="$(platform_path "$ISABELLE_CLASSPATH")"
+JAVA_ARGS["${#JAVA_ARGS[@]}"]="isabelle.setup.Setup"
+JAVA_ARGS["${#JAVA_ARGS[@]}"]="$COMMAND"
+
+if [ -z "$QUIET" ]; then
+  isabelle_java java "${JAVA_ARGS[@]}"
+else
+  isabelle_java java "${JAVA_ARGS[@]}" > /dev/null 2> /dev/null
+fi
--- a/lib/Tools/scalac	Sat Jul 17 23:09:54 2021 +0200
+++ b/lib/Tools/scalac	Sun Jul 18 12:48:31 2021 +0200
@@ -4,7 +4,7 @@
 #
 # DESCRIPTION: invoke Scala compiler within the Isabelle environment
 
-isabelle_scala_build || exit $?
+isabelle scala_build || exit $?
 
 classpath "$ISABELLE_SETUP_CLASSPATH"; unset ISABELLE_SETUP_CLASSPATH
 classpath "$CLASSPATH"; unset CLASSPATH
--- a/lib/scripts/getfunctions	Sat Jul 17 23:09:54 2021 +0200
+++ b/lib/scripts/getfunctions	Sun Jul 18 12:48:31 2021 +0200
@@ -211,22 +211,6 @@
 }
 export -f isabelle_directory
 
-#Isabelle/Scala/Java build
-function isabelle_scala_build ()
-{
-  rm -rf \
-    "$ISABELLE_HOME/lib/classes/Pure.jar" \
-    "$ISABELLE_HOME/lib/classes/Pure.shasum" \
-    "$ISABELLE_HOME/src/Tools/jEdit/dist"
-  if [ "$1" = "fresh" ]; then
-    CMD="build_fresh"
-  else
-    CMD="build"
-  fi
-  env ISABELLE_SETUP_CLASSPATH_SKIP=true isabelle java isabelle.setup.Setup "$CMD"
-}
-export -f isabelle_scala_build
-
 #arrays
 function splitarray ()
 {
--- a/src/Tools/GraphBrowser/lib/Tools/browser	Sat Jul 17 23:09:54 2021 +0200
+++ b/src/Tools/GraphBrowser/lib/Tools/browser	Sun Jul 18 12:48:31 2021 +0200
@@ -65,7 +65,7 @@
 
 ## main
 
-isabelle_scala_build || exit $?
+isabelle scala_build || exit $?
 
 if [ -n "$GRAPHFILE" ]; then
   PRIVATE_FILE="${ISABELLE_TMP:-${TMPDIR:-/tmp}}/$$"$(basename "$GRAPHFILE")
--- a/src/Tools/jEdit/lib/Tools/jedit	Sat Jul 17 23:09:54 2021 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Sun Jul 18 12:48:31 2021 +0200
@@ -55,7 +55,7 @@
 # options
 
 BUILD_ONLY=false
-FRESH_BUILD=""
+BUILD_OPTIONS=""
 ML_PROCESS_POLICY=""
 JEDIT_LOGIC_ANCESTOR=""
 JEDIT_LOGIC_REQUIREMENTS=""
@@ -99,7 +99,7 @@
         fi
         ;;
       f)
-        FRESH_BUILD="true"
+        BUILD_OPTIONS="-f"
         ;;
       j)
         ARGS["${#ARGS[@]}"]="$OPTARG"
@@ -154,11 +154,7 @@
 
 ## main
 
-if [ -n "$FRESH_BUILD" ]; then
-  isabelle_scala_build fresh || exit "$?"
-else
-  isabelle_scala_build || exit "$?"
-fi
+isabelle scala_build $BUILD_OPTIONS || exit $?
 
 if [ "$BUILD_ONLY" = false ]
 then