author | wenzelm |
Thu, 22 Sep 2016 11:25:27 +0200 | |
changeset 63936 | b87784e19a77 |
parent 61294 | 2d3d26e9b191 |
child 68014 | 9096895dc2a6 |
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:
47113
diff
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" |
61294 | 68 |
isabelle_jdk jar cf "$(platform_path "$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 |