#!/bin/bash

 #

 # $Id$

 # Author: Markus Wenzel, TU Muenchen

 # License: GPL (GNU GENERAL PUBLIC LICENSE)

 #

 # DESCRIPTION: build object-logic or run examples

 ## diagnostics

 PRG=$(basename "$0")

 function usage()

 {

   echo

   echo "Usage: $PRG [OPTIONS] LOGIC NAME"

   echo

   echo "  Options are:"

   echo "    -D PATH      dump generated document sources into PATH"

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

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

   echo "    -c BOOL      tell ML system to compress output image (default true)"

   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

 DUMP=""

 RPATH=""

 BUILD=""

 COMPRESS=true

 DOCUMENT=false

 INFO=false

 RESET=false

 SESSION=""

 function getoptions()

 {

   OPTIND=1

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

   do

     case "$OPT" in

       D)

         DUMP="$OPTARG"

         ;;

       P)

         RPATH="$OPTARG"

         ;;

       b)

         BUILD=true

         ;;

       c)

         COMPRESS="$OPTARG"

         ;;

       d)

         DOCUMENT="$OPTARG"

         ;;

       i)

         INFO="$OPTARG"

         ;;

       r)

         RESET=true

         ;;

       s)

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

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

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

 fi

 # prepare log dir

 LOGDIR="$ISABELLE_OUTPUT/log"

 mkdir -p "$LOGDIR"

 # run isabelle

 PARENT=$(basename "$LOGIC")

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

 if [ "$DOCUMENT" != false -a -d document ]; then

   DOC="$DOCUMENT"

   [ -n "$DUMP" -a -d "$DUMP" ] && "$ISATOOL" latex -o sty "$DUMP/root.tex" >/dev/null

 else

   DOC=""

 fi

 SECONDS=0

 if [ -n "$BUILD" ]; then

   ITEM="$SESSION"

   echo "Building $ITEM ..."

   LOG="$LOGDIR/$ITEM"

   OPT_C=""

   [ "$COMPRESS" = true ] && OPT_C="-c"

   "$ISABELLE" \

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

     $OPT_C -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\" \"$DUMP\" \"$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"