#!/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 "    -B           build mode with THIS_IS_ISABELLE_BUILD indication"

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

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

   echo "    -i BOOL      generate theory browsing information,"

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

   echo "    -m BOOL      multi line output (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

   exit 1

 }

 ## process command line

 # options

 BUILD=""

 INFO=false

 MULTI=false

 RESET=false

 SESSION=""

 RPATH=""

 function getoptions()

 {

   OPTIND=1

   while getopts "BP:bi:m:rs:" OPT

   do

     case "$OPT" in

       B)

         BUILD=true

         export THIS_IS_ISABELLE_BUILD=true

         ;;

       b)

         BUILD=true

         ;;

       i)

         INFO="$OPTARG"

         ;;

       m)

         MULTI="$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

 SECONDS=0

 PARENT=$(basename "$LOGIC")

 ECHO_LINE="echo -n"

 [ "$MULTI" = "true" ] && ECHO_LINE="echo"

 if [ -n "$BUILD" ]; then

   ITEM="$SESSION"

   $ECHO_LINE "Building $ITEM ..."

   LOG="$LOGDIR/$ITEM"

   $ISABELLE \

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

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

   RC=$?

 else

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

   $ECHO_LINE "Running $ITEM ..."

   LOG="$LOGDIR/$ITEM"

   cd "$NAME"

   $ISABELLE \

     -e "Session.use_dir $RESET $INFO \"$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

   if [ "$MULTI" = "true" ]; then

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

   else

     echo " OK  ($ELAPSED elapsed time)"

   fi

   gzip --force "$LOG"

 else

   [ "$MULTI" = "true" ] || echo

   echo "$ITEM FAILED"

   echo "(see also $LOG)"

   echo; tail $LOG; echo

 fi

 exit $RC