lib/browser/build
author wenzelm
Tue, 21 Dec 2010 21:21:21 +0100
changeset 41377 390c53904220
parent 34283 7911e83d06c0
child 47113 b5a5662528fb
permissions -rwxr-xr-x
configuration option "syntax_ast_trace" and "syntax_ast_stat";
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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