#!/bin/bash

 #

 # $Id$

 #

 # DESCRIPTION: build object-logic or run examples

 ## diagnostics

 PRG=$(basename $0)

 function usage()

 {

   echo

   echo "Usage: $PRG LOGIC NAME"

   echo

   echo "  Options are:"

   echo "    -P PATH      set path for remote theory browsing information"

   echo "    -b           build mode (output heap image, using current dir)"

   echo "    -d FORMAT    build document as FORMAT (default false)"

   echo "    -i BOOL      generate theory browsing information,"

   echo "                 i.e. HTML / graph data (default false)"

   echo "    -r           reset session path"

   echo "    -s NAME      override session NAME"

   echo

   echo "  Build object-logic or run examples. Also creates browsing"

   echo "  information (HTML etc.) according to settings."

   echo

   echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"

   echo

   exit 1

 }

 ## process command line

 # options

 BUILD=""

 DOCUMENT=false

 INFO=false

 RESET=false

 SESSION=""

 RPATH=""

 function getoptions()

 {

   OPTIND=1

   while getopts "P:bc:d:i:rs:" OPT

   do

     case "$OPT" in

       b)

         BUILD=true

         ;;

       d)

         DOCUMENT="$OPTARG"

         ;;

       i)

         INFO="$OPTARG"

         ;;

       r)

         RESET=true

         ;;

       s)

         SESSION="$OPTARG"

         ;;

       P)

         RPATH="$OPTARG"

         ;;

       \?)

         usage

         ;;

     esac

   done

 }

 getoptions $ISABELLE_USEDIR_OPTIONS

 getoptions "$@"

 shift $(($OPTIND - 1))

 # args

 [ $# -ne 2 ] && usage

 LOGIC="$1"; shift

 NAME="$1"; shift

 [ -z "$SESSION" ] && SESSION=$(basename $NAME)

 ## main

 # prepare browser info dir

 if [ "$INFO" = "true" -a ! -f $ISABELLE_BROWSER_INFO/index.html ]; then

   mkdir -p $ISABELLE_BROWSER_INFO/gif

   cp $ISABELLE_HOME/lib/logo/isabelle.gif $ISABELLE_BROWSER_INFO/gif/isabelle.gif

   cp $ISABELLE_HOME/lib/html/index1.html $ISABELLE_BROWSER_INFO/index.html

   mkdir -p $ISABELLE_BROWSER_INFO/graph

   cp $ISABELLE_HOME/lib/html/index2.html $ISABELLE_BROWSER_INFO/graph/index.html

   mkdir $ISABELLE_BROWSER_INFO/graph/GraphBrowser

   mkdir $ISABELLE_BROWSER_INFO/graph/awtUtilities

   cp $ISABELLE_HOME/lib/browser/GraphBrowser/*.class $ISABELLE_BROWSER_INFO/graph/GraphBrowser

   cp $ISABELLE_HOME/lib/browser/awtUtilities/*.class $ISABELLE_BROWSER_INFO/graph/awtUtilities

 fi

 # prepare log dir

 LOGDIR="$ISABELLE_OUTPUT/log"

 mkdir -p "$LOGDIR"

 # run isabelle

 PARENT=$(basename "$LOGIC")

 [ -z "$BUILD" ] && cd "$NAME"

 DOC=""

 [ "$DOCUMENT" != false -a -d document ] && DOC="$DOCUMENT"

 SECONDS=0

 if [ -n "$BUILD" ]; then

   ITEM="$SESSION"

   echo "Building $ITEM ..."

   LOG="$LOGDIR/$ITEM"

   $ISABELLE \

     -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$RPATH\";" \

     -q -w $LOGIC $NAME > $LOG 2>&1

   RC=$?

 else

   ITEM=$(basename $LOGIC)-"$SESSION"

   echo "Running $ITEM ..."

   LOG="$LOGDIR/$ITEM"

   $ISABELLE \

     -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$RPATH\"; quit();" \

     -r -q $LOGIC > $LOG 2>&1

   RC=$?

   cd ..

 fi

 ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)

 # exit status

 if [ $RC -eq 0 ]; then

   echo "Finished $ITEM ($ELAPSED elapsed time)"

   gzip --force "$LOG"

 else

   echo "$ITEM FAILED"

   echo "(see also $LOG)"

   echo; tail $LOG; echo

 fi

 exit $RC