# HG changeset patch
# User wenzelm
# Date 1262812732 -3600
# Node ID 7911e83d06c0e3e9da524de63e25806ace5de3eb
# Parent  549969a7f5826e0d5d7540ecde51c31de6f70fb0
simplified build/bootstrap of graph browser -- avoid make;

diff -r 549969a7f582 -r 7911e83d06c0 Admin/build
--- a/Admin/build	Wed Jan 06 20:00:22 2010 +0100
+++ b/Admin/build	Wed Jan 06 22:18:52 2010 +0100
@@ -58,12 +58,9 @@
 
 function build_browser ()
 {
-  echo "###"
-  echo "### Building graph browser ..."
-  echo "###"
-
-  cd "$ISABELLE_HOME/lib/browser"
-  make clean all || fail "Failed to build graph browser!"
+  pushd "$ISABELLE_HOME/lib/browser" >/dev/null
+  "$ISABELLE_TOOL" env ./build || fail "Failed!"
+  popd >/dev/null
 }
 
 
diff -r 549969a7f582 -r 7911e83d06c0 lib/Tools/browser
--- a/lib/Tools/browser	Wed Jan 06 20:00:22 2010 +0100
+++ b/lib/Tools/browser	Wed Jan 06 22:18:52 2010 +0100
@@ -60,6 +60,8 @@
 
 ## main
 
+[ -e "$ISABELLE_HOME/Admin/build" ] && "$ISABELLE_HOME/Admin/build" browser
+
 classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar"
 
 if [ -z "$GRAPHFILE" ]; then
diff -r 549969a7f582 -r 7911e83d06c0 lib/browser/Makefile
--- a/lib/browser/Makefile	Wed Jan 06 20:00:22 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-
-DST=classes
-
-all: GraphBrowser.jar
-
-GraphBrowser.jar: GraphBrowser/*.java awtUtilities/*.java
-	mkdir -p $(DST)
-	javac -source 1.4 -d $(DST) GraphBrowser/GraphBrowser.java GraphBrowser/Console.java
-	jar cf GraphBrowser.jar -C $(DST) . 
-	rm -rf $(DST)
-
-clean:
-	rm -f GraphBrowser/*.class
-	rm -f awtUtilities/*.class
-	rm -rf $(DST)
-	rm -f GraphBrowser.jar
diff -r 549969a7f582 -r 7911e83d06c0 lib/browser/build
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/browser/build	Wed Jan 06 22:18:52 2010 +0100
@@ -0,0 +1,74 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# mk - build graph browser
+#
+# Requires proper Isabelle settings environment.
+
+
+## diagnostics
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+[ -n "$ISABELLE_HOME" ] || fail "Missing Isabelle settings environment"
+
+
+## dependencies
+
+declare -a SOURCES=(
+  GraphBrowser/AWTFontMetrics.java
+  GraphBrowser/AbstractFontMetrics.java
+  GraphBrowser/Box.java
+  GraphBrowser/Console.java
+  GraphBrowser/DefaultFontMetrics.java
+  GraphBrowser/Directory.java
+  GraphBrowser/DummyVertex.java
+  GraphBrowser/Graph.java
+  GraphBrowser/GraphBrowser.java
+  GraphBrowser/GraphBrowserFrame.java
+  GraphBrowser/GraphView.java
+  GraphBrowser/NormalVertex.java
+  GraphBrowser/ParseError.java
+  GraphBrowser/Region.java
+  GraphBrowser/Spline.java
+  GraphBrowser/TreeBrowser.java
+  GraphBrowser/TreeNode.java
+  GraphBrowser/Vertex.java
+  awtUtilities/Border.java
+  awtUtilities/MessageDialog.java
+  awtUtilities/TextFrame.java
+)
+
+TARGET="$ISABELLE_HOME/lib/browser/GraphBrowser.jar"
+
+
+## main
+
+OUTDATED=false
+
+for SOURCE in "${SOURCES[@]}"
+do
+  [ ! -e "$SOURCE" ] && fail "Missing source file: $SOURCE"
+  [ ! -e "$TARGET" -o "$SOURCE" -nt "$TARGET" ] && OUTDATED=true
+done
+
+if [ "$OUTDATED" = true ]
+then
+  echo "###"
+  echo "### Building graph browser ..."
+  echo "###"
+
+  rm -rf classes && mkdir classes
+
+  javac -d classes -source 1.4 "${SOURCES[@]}" || \
+    fail "Failed to compile sources"
+  jar cf "$(jvmpath "$TARGET")" -C classes . ||
+    fail "Failed to produce $TARGET"
+
+  rm -rf classes
+fi