# HG changeset patch
# User wenzelm
# Date 882271471 -3600
# Node ID 950001e4859ac53ad6b70c11e93ad8fd2a1ab5ed
# Parent  231730ecaa95f7751c6850b8733defdd55eb0fbf
tuned;

diff -r 231730ecaa95 -r 950001e4859a lib/Tools/usedir
--- a/lib/Tools/usedir	Tue Dec 16 12:19:26 1997 +0100
+++ b/lib/Tools/usedir	Tue Dec 16 12:24:31 1997 +0100
@@ -70,27 +70,32 @@
 LOGIC="$1"; shift
 NAME="$1"; shift
 
+[ -z "$SESSION" ] && SESSION=$(basename $NAME)
 
-# prepare directories for html and graph output
+
+
+## main
 
-if [ $INFO = "true" -a ! -d $ISABELLE_BROWSER_INFO ]; then
+# prepare browser info directories
+
+if [ "$INFO" = "true" -a ! -d $ISABELLE_BROWSER_INFO ]; then
+
   mkdir -p $ISABELLE_BROWSER_INFO/gif
-  cp $ISABELLE_HOME/lib/images/*arrow.gif $ISABELLE_BROWSER_INFO/gif
+  cp $ISABELLE_HOME/lib/images/blue_arrow.gif $ISABELLE_BROWSER_INFO/gif
+  cp $ISABELLE_HOME/lib/images/red_arrow.gif $ISABELLE_BROWSER_INFO/gif
   cp $ISABELLE_HOME/lib/logo/isabelle.gif $ISABELLE_BROWSER_INFO/gif/isabelle.gif
   cp $ISABELLE_HOME/lib/html/index1.html $ISABELLE_BROWSER_INFO/index.html
+
   mkdir -p $ISABELLE_BROWSER_INFO/graph
   cp $ISABELLE_HOME/lib/html/index2.html $ISABELLE_BROWSER_INFO/graph/index.html
   mkdir $ISABELLE_BROWSER_INFO/graph/GraphBrowser
   mkdir $ISABELLE_BROWSER_INFO/graph/awtUtilities
-  cp $ISABELLE_HOME/lib/browser/G*/*.class $ISABELLE_BROWSER_INFO/graph/G*
-  cp $ISABELLE_HOME/lib/browser/a*/*.class $ISABELLE_BROWSER_INFO/graph/a*
+  cp $ISABELLE_HOME/lib/browser/GraphBrowser/*.class $ISABELLE_BROWSER_INFO/graph/GraphBrowser
+  cp $ISABELLE_HOME/lib/browser/awtUtilities/*.class $ISABELLE_BROWSER_INFO/graph/awtUtilities
+
 fi
 
 
-## main
-
-[ -z "$SESSION" ] && SESSION=$(basename $NAME)
-
 if [ -n "$BUILD" ]; then
   exec $ISABELLE \
     -e "make_html := $INFO; make_graph := $INFO; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; add_session\"$SESSION\"; exit_use_dir\".\"; make_html := false; make_graph := false;" \