lib/browser/build
changeset 34283 7911e83d06c0
child 47113 b5a5662528fb
equal deleted inserted replaced
34282:549969a7f582 34283:7911e83d06c0
       
     1 #!/usr/bin/env bash
       
     2 #
       
     3 # Author: Makarius
       
     4 #
       
     5 # mk - build graph browser
       
     6 #
       
     7 # Requires proper Isabelle settings environment.
       
     8 
       
     9 
       
    10 ## diagnostics
       
    11 
       
    12 function fail()
       
    13 {
       
    14   echo "$1" >&2
       
    15   exit 2
       
    16 }
       
    17 
       
    18 [ -n "$ISABELLE_HOME" ] || fail "Missing Isabelle settings environment"
       
    19 
       
    20 
       
    21 ## dependencies
       
    22 
       
    23 declare -a SOURCES=(
       
    24   GraphBrowser/AWTFontMetrics.java
       
    25   GraphBrowser/AbstractFontMetrics.java
       
    26   GraphBrowser/Box.java
       
    27   GraphBrowser/Console.java
       
    28   GraphBrowser/DefaultFontMetrics.java
       
    29   GraphBrowser/Directory.java
       
    30   GraphBrowser/DummyVertex.java
       
    31   GraphBrowser/Graph.java
       
    32   GraphBrowser/GraphBrowser.java
       
    33   GraphBrowser/GraphBrowserFrame.java
       
    34   GraphBrowser/GraphView.java
       
    35   GraphBrowser/NormalVertex.java
       
    36   GraphBrowser/ParseError.java
       
    37   GraphBrowser/Region.java
       
    38   GraphBrowser/Spline.java
       
    39   GraphBrowser/TreeBrowser.java
       
    40   GraphBrowser/TreeNode.java
       
    41   GraphBrowser/Vertex.java
       
    42   awtUtilities/Border.java
       
    43   awtUtilities/MessageDialog.java
       
    44   awtUtilities/TextFrame.java
       
    45 )
       
    46 
       
    47 TARGET="$ISABELLE_HOME/lib/browser/GraphBrowser.jar"
       
    48 
       
    49 
       
    50 ## main
       
    51 
       
    52 OUTDATED=false
       
    53 
       
    54 for SOURCE in "${SOURCES[@]}"
       
    55 do
       
    56   [ ! -e "$SOURCE" ] && fail "Missing source file: $SOURCE"
       
    57   [ ! -e "$TARGET" -o "$SOURCE" -nt "$TARGET" ] && OUTDATED=true
       
    58 done
       
    59 
       
    60 if [ "$OUTDATED" = true ]
       
    61 then
       
    62   echo "###"
       
    63   echo "### Building graph browser ..."
       
    64   echo "###"
       
    65 
       
    66   rm -rf classes && mkdir classes
       
    67 
       
    68   javac -d classes -source 1.4 "${SOURCES[@]}" || \
       
    69     fail "Failed to compile sources"
       
    70   jar cf "$(jvmpath "$TARGET")" -C classes . ||
       
    71     fail "Failed to produce $TARGET"
       
    72 
       
    73   rm -rf classes
       
    74 fi