lib/Tools/usedir
author wenzelm
Tue Mar 18 17:03:05 1997 +0100 (1997-03-18)
changeset 2808 e8a224e41b9f
child 2812 dfcd1b00f294
permissions -rwxr-xr-x
usedir -- build object-logic or run examples;
wenzelm@2808
     1
#!/bin/bash -norc
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 \".\")"
wenzelm@2808
    19
  echo "    -c           force copying of heap file (for Poly/ML)"
wenzelm@2808
    20
  echo "    -s NAME      override session NAME"
wenzelm@2808
    21
  echo
wenzelm@2808
    22
  echo "  Build object-logic or run examples. Also creates browsing"
wenzelm@2808
    23
  echo "  information (HTML etc.) according to settings."
wenzelm@2808
    24
  echo
wenzelm@2808
    25
  exit 1
wenzelm@2808
    26
}
wenzelm@2808
    27
wenzelm@2808
    28
wenzelm@2808
    29
## process command line
wenzelm@2808
    30
wenzelm@2808
    31
# options
wenzelm@2808
    32
wenzelm@2808
    33
BUILD=""
wenzelm@2808
    34
COPYDB=""
wenzelm@2808
    35
SESSION=""
wenzelm@2808
    36
wenzelm@2808
    37
while getopts "bc" OPT
wenzelm@2808
    38
do
wenzelm@2808
    39
  case "$OPT" in
wenzelm@2808
    40
    b)
wenzelm@2808
    41
      BUILD=true
wenzelm@2808
    42
      ;;
wenzelm@2808
    43
    c)
wenzelm@2808
    44
      COPYDB="-c"
wenzelm@2808
    45
      ;;
wenzelm@2808
    46
    s)
wenzelm@2808
    47
      SESSION="$OPTARG"
wenzelm@2808
    48
      ;;
wenzelm@2808
    49
    \?)
wenzelm@2808
    50
      usage
wenzelm@2808
    51
      ;;
wenzelm@2808
    52
  esac
wenzelm@2808
    53
done
wenzelm@2808
    54
wenzelm@2808
    55
shift $(($OPTIND - 1))
wenzelm@2808
    56
wenzelm@2808
    57
wenzelm@2808
    58
# args
wenzelm@2808
    59
wenzelm@2808
    60
[ $# -ne 2 ] && usage
wenzelm@2808
    61
wenzelm@2808
    62
LOGIC="$1"; shift
wenzelm@2808
    63
NAME="$1"; shift
wenzelm@2808
    64
wenzelm@2808
    65
wenzelm@2808
    66
wenzelm@2808
    67
## main
wenzelm@2808
    68
wenzelm@2808
    69
[ -z "$SESSION" ] && SESSION=$(basename $NAME)
wenzelm@2808
    70
wenzelm@2808
    71
if [ -n "$BUILD" ]; then
wenzelm@2808
    72
  exec $ISABELLE \
wenzelm@2808
    73
    -e "make_html := $ISABELLE_HTML;" \
wenzelm@2808
    74
    -e "set_session\"$SESSION\";" \
wenzelm@2808
    75
    -e "exit_use_dir\".\";" \
wenzelm@2808
    76
    -q $COPYDB $LOGIC $NAME
wenzelm@2808
    77
else
wenzelm@2808
    78
  exec $ISABELLE \
wenzelm@2808
    79
    -e "make_html := $ISABELLE_HTML;" \
wenzelm@2808
    80
    -e "set_session\"$SESSION\";" \
wenzelm@2808
    81
    -e "exit_use_dir\"$NAME\";" \
wenzelm@2808
    82
    -r -q $LOGIC
wenzelm@2808
    83
fi