# HG changeset patch
# User wenzelm
# Date 1457870690 -3600
# Node ID 0a01bc7f09464d8956e28921a3002e4d2ef36967
# Parent  7c723aa878714487515aa9c9e300b942ec896ee8
prefer Scala over bash function;

diff -r 7c723aa87871 -r 0a01bc7f0946 lib/scripts/getfunctions
--- a/lib/scripts/getfunctions	Sun Mar 13 12:50:46 2016 +0100
+++ b/lib/scripts/getfunctions	Sun Mar 13 13:04:50 2016 +0100
@@ -24,33 +24,6 @@
   export -f tar
 fi
 
-#shared library convenience
-function librarypath ()
-{
-  for X in "$@"
-  do
-    case "$ISABELLE_PLATFORM" in
-      *-darwin)
-        if [ -z "$DYLD_LIBRARY_PATH" ]; then
-          DYLD_LIBRARY_PATH="$X"
-        else
-          DYLD_LIBRARY_PATH="$X:$DYLD_LIBRARY_PATH"
-        fi
-        export DYLD_LIBRARY_PATH
-        ;;
-      *)
-        if [ -z "$LD_LIBRARY_PATH" ]; then
-          LD_LIBRARY_PATH="$X"
-        else
-          LD_LIBRARY_PATH="$X:$LD_LIBRARY_PATH"
-        fi
-        export LD_LIBRARY_PATH
-        ;;
-    esac
-  done
-}
-export -f librarypath
-
 #robust invocation via ISABELLE_JDK_HOME
 function isabelle_jdk ()
 {
diff -r 7c723aa87871 -r 0a01bc7f0946 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sun Mar 13 12:50:46 2016 +0100
+++ b/src/Pure/System/isabelle_system.scala	Sun Mar 13 13:04:50 2016 +0100
@@ -144,6 +144,16 @@
 
   def cygwin_root(): String = getenv_strict("CYGWIN_ROOT")
 
+  def library_path(env: Map[String, String], elem: String): Map[String, String] =
+    if (Platform.is_windows) env
+    else {
+      val x = if (Platform.is_macos) "DYLD_LIBRARY_PATH" else "LD_LIBRARY_PATH"
+      env.getOrElse(x, "") match {
+        case "" => env + (x -> elem)
+        case y => env + (x -> (y + ":" + elem))
+      }
+    }
+
 
 
   /** file-system operations **/
diff -r 7c723aa87871 -r 0a01bc7f0946 src/Pure/Tools/ml_process.scala
--- a/src/Pure/Tools/ml_process.scala	Sun Mar 13 12:50:46 2016 +0100
+++ b/src/Pure/Tools/ml_process.scala	Sun Mar 13 13:04:50 2016 +0100
@@ -98,9 +98,12 @@
       (eval_heaps ::: eval_initial ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process).
         map(eval => List("--eval", eval)).flatten ::: args
 
-    Bash.process(
-      """librarypath "$ML_HOME"; exec "$ML_HOME/poly" -q """ + File.bash_args(bash_args),
-      cwd = cwd, env = env ++ env_options ++ env_tmp, redirect = redirect,
+    Bash.process("""exec "$ML_HOME/poly" -q """ + File.bash_args(bash_args),
+      cwd = cwd,
+      env =
+        Isabelle_System.library_path(env ++ env_options ++ env_tmp,
+          Isabelle_System.getenv_strict("ML_HOME")),
+      redirect = redirect,
       cleanup = () =>
         {
           isabelle_process_options.delete