lib/browser/build
author traytel
Mon, 24 Oct 2016 16:53:32 +0200
changeset 64379 71f42dcaa1df
parent 61294 2d3d26e9b191
child 68014 9096895dc2a6
permissions -rwxr-xr-x
additional user-specified simp (naturality) rules used in friend_of_corec
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 "### 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
2d3d26e9b191 renamed jvmpath to platform_path;
wenzelm
parents: 49004
diff changeset
    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