| author | blanchet | 
| Tue, 17 May 2011 15:11:36 +0200 | |
| changeset 42831 | c9b0968484fb | 
| parent 34283 | 7911e83d06c0 | 
| child 47113 | b5a5662528fb | 
| 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 "###"  | 
| 
 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 
wenzelm 
parents:  
diff
changeset
 | 
63  | 
echo "### Building graph browser ..."  | 
| 
 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 
wenzelm 
parents:  
diff
changeset
 | 
64  | 
echo "###"  | 
| 
 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 
wenzelm 
parents:  
diff
changeset
 | 
65  | 
|
| 
 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 
wenzelm 
parents:  
diff
changeset
 | 
66  | 
rm -rf classes && mkdir classes  | 
| 
 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 
wenzelm 
parents:  
diff
changeset
 | 
67  | 
|
| 
 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 
wenzelm 
parents:  
diff
changeset
 | 
68  | 
  javac -d classes -source 1.4 "${SOURCES[@]}" || \
 | 
| 
 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 
wenzelm 
parents:  
diff
changeset
 | 
69  | 
fail "Failed to compile sources"  | 
| 
 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 
wenzelm 
parents:  
diff
changeset
 | 
70  | 
jar cf "$(jvmpath "$TARGET")" -C classes . ||  | 
| 
 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 
wenzelm 
parents:  
diff
changeset
 | 
71  | 
fail "Failed to produce $TARGET"  | 
| 
 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 
wenzelm 
parents:  
diff
changeset
 | 
72  | 
|
| 
 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 
wenzelm 
parents:  
diff
changeset
 | 
73  | 
rm -rf classes  | 
| 
 
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
 
wenzelm 
parents:  
diff
changeset
 | 
74  | 
fi  |