lib/Tools/usedir
author berghofe
Tue Sep 30 12:52:15 1997 +0200 (1997-09-30)
changeset 3747 cd9b6c86926c
parent 3636 3f2e55e5bacc
child 3844 7704dc8997ed
permissions -rwxr-xr-x
There is now one single option -i for generating theory browsing
information instead of the two options -h and -g .
wenzelm@3007
     1
#!/bin/bash
wenzelm@2808
     2
#
wenzelm@2808
     3
# $Id$
wenzelm@2808
     4
#
wenzelm@2808
     5
# DESCRIPTION: build object-logic or run examples
wenzelm@2808
     6
wenzelm@2808
     7
wenzelm@2808
     8
## diagnostics
wenzelm@2808
     9
wenzelm@2808
    10
PRG=$(basename $0)
wenzelm@2808
    11
wenzelm@2808
    12
function usage()
wenzelm@2808
    13
{
wenzelm@2808
    14
  echo
wenzelm@2808
    15
  echo "Usage: $PRG LOGIC NAME"
wenzelm@2808
    16
  echo
wenzelm@2808
    17
  echo "  Options are:"
wenzelm@2808
    18
  echo "    -b           build mode (output heap image, use dir \".\")"
berghofe@3747
    19
  echo "    -i BOOL      generate theory browsing information,"
berghofe@3747
    20
  echo "                 i.e. HTML / graph data (default false)"
wenzelm@2808
    21
  echo "    -s NAME      override session NAME"
wenzelm@2808
    22
  echo
wenzelm@2808
    23
  echo "  Build object-logic or run examples. Also creates browsing"
wenzelm@2808
    24
  echo "  information (HTML etc.) according to settings."
wenzelm@2808
    25
  echo
wenzelm@2808
    26
  exit 1
wenzelm@2808
    27
}
wenzelm@2808
    28
wenzelm@2808
    29
wenzelm@2808
    30
## process command line
wenzelm@2808
    31
wenzelm@2808
    32
# options
wenzelm@2808
    33
wenzelm@2808
    34
BUILD=""
berghofe@3747
    35
INFO=false
wenzelm@2808
    36
SESSION=""
wenzelm@2808
    37
wenzelm@2917
    38
function getoptions()
wenzelm@2917
    39
{
wenzelm@2917
    40
  OPTIND=1
berghofe@3747
    41
  while getopts "bi:s:" OPT
wenzelm@2917
    42
  do
wenzelm@2917
    43
    case "$OPT" in
wenzelm@2917
    44
      b)
wenzelm@2917
    45
        BUILD=true
wenzelm@2917
    46
        ;;
berghofe@3747
    47
      i)
berghofe@3747
    48
        INFO="$OPTARG"
wenzelm@2917
    49
        ;;
wenzelm@2917
    50
      s)
wenzelm@2917
    51
        SESSION="$OPTARG"
wenzelm@2917
    52
        ;;
wenzelm@2917
    53
      \?)
wenzelm@2917
    54
        usage
wenzelm@2917
    55
        ;;
wenzelm@2917
    56
    esac
wenzelm@2917
    57
  done
wenzelm@2917
    58
}
wenzelm@2808
    59
wenzelm@2917
    60
getoptions $ISABELLE_USEDIR_OPTIONS
wenzelm@2917
    61
wenzelm@2917
    62
getoptions "$@"
wenzelm@2808
    63
shift $(($OPTIND - 1))
wenzelm@2808
    64
wenzelm@2808
    65
wenzelm@2808
    66
# args
wenzelm@2808
    67
wenzelm@2808
    68
[ $# -ne 2 ] && usage
wenzelm@2808
    69
wenzelm@2808
    70
LOGIC="$1"; shift
wenzelm@2808
    71
NAME="$1"; shift
wenzelm@2808
    72
wenzelm@2808
    73
berghofe@3636
    74
# prepare directories for html and graph output
berghofe@3636
    75
berghofe@3747
    76
if [ $INFO = "true" -a ! -d $ISABELLE_BROWSER_INFO ]; then
berghofe@3747
    77
  mkdir -p $ISABELLE_BROWSER_INFO/gif
berghofe@3747
    78
  cp $ISABELLE_HOME/lib/images/*.gif $ISABELLE_BROWSER_INFO/gif
berghofe@3747
    79
  cp $ISABELLE_HOME/lib/html/index1.html $ISABELLE_BROWSER_INFO/index.html
berghofe@3636
    80
  mkdir -p $ISABELLE_BROWSER_INFO/graph
berghofe@3636
    81
  cp $ISABELLE_HOME/lib/html/index2.html $ISABELLE_BROWSER_INFO/graph/index.html
berghofe@3636
    82
  mkdir $ISABELLE_BROWSER_INFO/graph/GraphBrowser
berghofe@3636
    83
  mkdir $ISABELLE_BROWSER_INFO/graph/awtUtilities
berghofe@3636
    84
  cp $ISABELLE_HOME/lib/browser/G*/*.class $ISABELLE_BROWSER_INFO/graph/G*
berghofe@3636
    85
  cp $ISABELLE_HOME/lib/browser/a*/*.class $ISABELLE_BROWSER_INFO/graph/a*
berghofe@3636
    86
fi
berghofe@3636
    87
wenzelm@2808
    88
wenzelm@2808
    89
## main
wenzelm@2808
    90
wenzelm@2808
    91
[ -z "$SESSION" ] && SESSION=$(basename $NAME)
wenzelm@2808
    92
wenzelm@2808
    93
if [ -n "$BUILD" ]; then
wenzelm@2808
    94
  exec $ISABELLE \
berghofe@3747
    95
    -e "make_html := $INFO; make_graph := $INFO; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; set_session\"$SESSION\"; exit_use_dir\".\"; make_html := false; make_graph := false;" \
wenzelm@3504
    96
    -q -w $LOGIC $NAME
wenzelm@2808
    97
else
wenzelm@2808
    98
  exec $ISABELLE \
berghofe@3747
    99
    -e "make_html := $INFO; make_graph := $INFO; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; set_session\"$SESSION\"; exit_use_dir\"$NAME\"; make_html := false; make_graph := false; quit();" \
wenzelm@2808
   100
    -r -q $LOGIC
wenzelm@2808
   101
fi