| author | blanchet | 
| Thu, 18 Sep 2014 16:47:40 +0200 | |
| changeset 58374 | 1b4d31b7bd10 | 
| parent 49004 | 3a324a3f4aea | 
| child 61294 | 2d3d26e9b191 | 
| permissions | -rwxr-xr-x | 
| 34283 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 1 | #!/usr/bin/env bash | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 2 | # | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 3 | # Author: Makarius | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 4 | # | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 5 | # mk - build graph browser | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 6 | # | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 7 | # Requires proper Isabelle settings environment. | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 8 | |
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 9 | |
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 10 | ## diagnostics | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 11 | |
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 12 | function fail() | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 13 | {
 | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 14 | echo "$1" >&2 | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 15 | exit 2 | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 16 | } | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 17 | |
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 18 | [ -n "$ISABELLE_HOME" ] || fail "Missing Isabelle settings environment" | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 19 | |
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 20 | |
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 21 | ## dependencies | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 22 | |
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 23 | declare -a SOURCES=( | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 24 | GraphBrowser/AWTFontMetrics.java | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 25 | GraphBrowser/AbstractFontMetrics.java | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 26 | GraphBrowser/Box.java | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 27 | GraphBrowser/Console.java | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 28 | GraphBrowser/DefaultFontMetrics.java | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 29 | GraphBrowser/Directory.java | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 30 | GraphBrowser/DummyVertex.java | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 31 | GraphBrowser/Graph.java | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 32 | GraphBrowser/GraphBrowser.java | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 33 | GraphBrowser/GraphBrowserFrame.java | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 34 | GraphBrowser/GraphView.java | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 35 | GraphBrowser/NormalVertex.java | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 36 | GraphBrowser/ParseError.java | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 37 | GraphBrowser/Region.java | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 38 | GraphBrowser/Spline.java | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 39 | GraphBrowser/TreeBrowser.java | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 40 | GraphBrowser/TreeNode.java | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 41 | GraphBrowser/Vertex.java | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 42 | awtUtilities/Border.java | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 43 | awtUtilities/MessageDialog.java | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 44 | awtUtilities/TextFrame.java | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 45 | ) | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 46 | |
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 47 | TARGET="$ISABELLE_HOME/lib/browser/GraphBrowser.jar" | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 48 | |
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 49 | |
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 50 | ## main | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 51 | |
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 52 | OUTDATED=false | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 53 | |
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 54 | for SOURCE in "${SOURCES[@]}"
 | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 55 | do | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 56 | [ ! -e "$SOURCE" ] && fail "Missing source file: $SOURCE" | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 57 | [ ! -e "$TARGET" -o "$SOURCE" -nt "$TARGET" ] && OUTDATED=true | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 58 | done | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 59 | |
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 60 | if [ "$OUTDATED" = true ] | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 61 | then | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 62 | echo "### Building graph browser ..." | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 63 | |
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 64 | rm -rf classes && mkdir classes | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 65 | |
| 47115 
1a05adae1cc9
more robust command invocation via ISABELLE_JDK_HOME or SCALA_HOME (NB: bash exec requires genuine executable, not function);
 wenzelm parents: 
47113diff
changeset | 66 |   isabelle_jdk javac -d classes -source 1.4 "${SOURCES[@]}" || \
 | 
| 34283 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 67 | fail "Failed to compile sources" | 
| 47115 
1a05adae1cc9
more robust command invocation via ISABELLE_JDK_HOME or SCALA_HOME (NB: bash exec requires genuine executable, not function);
 wenzelm parents: 
47113diff
changeset | 68 | isabelle_jdk jar cf "$(jvmpath "$TARGET")" -C classes . || | 
| 34283 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 69 | fail "Failed to produce $TARGET" | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 70 | |
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 71 | rm -rf classes | 
| 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 wenzelm parents: diff
changeset | 72 | fi |