lib/Tools/usedir

Added some code for generating theory browsing data.

#!/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 (output heap image, use dir \".\")"
  echo "    -g BOOL      generate theory graph data (default false)"
  echo "    -h BOOL      generate theory HTML data (default false)"
  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=""
GRAPH=false
HTML=false
SESSION=""

function getoptions()
{
  OPTIND=1
  while getopts "bcg:h:s:" OPT
  do
    case "$OPT" in
      b)
        BUILD=true
        ;;
      g)
        GRAPH="$OPTARG"
        ;;
      h)
        HTML="$OPTARG"
        ;;
      s)
        SESSION="$OPTARG"
        ;;
      \?)
        usage
        ;;
    esac
  done
}

getoptions $ISABELLE_USEDIR_OPTIONS

getoptions "$@"
shift $(($OPTIND - 1))


# args

[ $# -ne 2 ] && usage

LOGIC="$1"; shift
NAME="$1"; shift


# prepare directories for html and graph output

if [ $HTML = "true" -o $GRAPH = "true" ]; then
  if [ ! -d $ISABELLE_BROWSER_INFO/gif ]; then
    mkdir -p $ISABELLE_BROWSER_INFO/gif
    cp $ISABELLE_HOME/lib/images/*.gif $ISABELLE_BROWSER_INFO/gif
  fi
fi

if [ $HTML = "true" -a ! -d $ISABELLE_BROWSER_INFO/html ]; then
  mkdir -p $ISABELLE_BROWSER_INFO/html
  cp $ISABELLE_HOME/lib/html/index1.html $ISABELLE_BROWSER_INFO/html/index.html
fi

if [ $GRAPH = "true" -a ! -d $ISABELLE_BROWSER_INFO/graph ]; then
  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/G*/*.class $ISABELLE_BROWSER_INFO/graph/G*
  cp $ISABELLE_HOME/lib/browser/a*/*.class $ISABELLE_BROWSER_INFO/graph/a*
fi


## main

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

if [ -n "$BUILD" ]; then
  exec $ISABELLE \
    -e "make_html := $HTML; make_graph := $GRAPH; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; set_session\"$SESSION\"; exit_use_dir\".\"; make_html := false; make_graph := false;" \
    -q -w $LOGIC $NAME
else
  exec $ISABELLE \
    -e "make_html := $HTML; make_graph := $GRAPH; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; set_session\"$SESSION\"; exit_use_dir\"$NAME\"; make_html := false; make_graph := false; quit();" \
    -r -q $LOGIC
fi