# HG changeset patch
# User wenzelm
# Date 1197749868 -3600
# Node ID ce061f5083d7dd30b95091dc7a333ec7678104b1
# Parent  9fc75df32c81000855119a0a382879a9a6811232
added javapath (for cygwin);

diff -r 9fc75df32c81 -r ce061f5083d7 lib/Tools/browser
--- a/lib/Tools/browser	Sat Dec 15 20:10:26 2007 +0100
+++ b/lib/Tools/browser	Sat Dec 15 21:17:48 2007 +0100
@@ -61,7 +61,8 @@
 
 ## main
 
-export CLASSPATH="$ISABELLE_HOME/lib/browser/GraphBrowser.jar"
+export CLASSPATH="$(javapath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar")"
+
 if [ -z "$GRAPHFILE" ]; then
   cd "$ISABELLE_BROWSER_INFO"
   exec java GraphBrowser.GraphBrowser
@@ -82,9 +83,9 @@
   esac
 
   if [ -z "$OUTFILE" ]; then
-    java GraphBrowser.GraphBrowser "$PRIVATE_FILE"
+    java GraphBrowser.GraphBrowser "$(javapath "$PRIVATE_FILE")"
   else
-    java GraphBrowser.Console "$PRIVATE_FILE" "$OUTFILE"
+    java GraphBrowser.Console "$(javapath "$PRIVATE_FILE")" "$(javapath "$OUTFILE")"
   fi
   RC="$?"
 
diff -r 9fc75df32c81 -r ce061f5083d7 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Sat Dec 15 20:10:26 2007 +0100
+++ b/lib/scripts/getsettings	Sat Dec 15 21:17:48 2007 +0100
@@ -44,6 +44,13 @@
   echo "$RESULT"
 }
 
+#Java path wrapper
+if [ "$OSTYPE" = cygwin ]; then
+  function javapath() { cygpath -w "$@"; }
+else
+  function javapath() { echo "$@"; }
+fi
+
 #get actual settings
 source "$ISABELLE_HOME/etc/settings" || exit 2
 ISABELLE_SITE_SETTINGS_PRESENT=true