lib/Tools/usedir
author wenzelm
Tue Apr 22 11:37:12 1997 +0200 (1997-04-22)
changeset 3007 e5efa177ee0c
parent 2917 c7411fce37e4
child 3054 c16029f41ad9
permissions -rwxr-xr-x
removed -norc;
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 \".\")"
wenzelm@2808
    19
  echo "    -c           force copying of heap file (for Poly/ML)"
wenzelm@2917
    20
  echo "    -g BOOL      generate theory graph data (default false)"
wenzelm@2917
    21
  echo "    -h BOOL      generate theory HTML data (default false)"
wenzelm@2808
    22
  echo "    -s NAME      override session NAME"
wenzelm@2808
    23
  echo
wenzelm@2808
    24
  echo "  Build object-logic or run examples. Also creates browsing"
wenzelm@2808
    25
  echo "  information (HTML etc.) according to settings."
wenzelm@2808
    26
  echo
wenzelm@2808
    27
  exit 1
wenzelm@2808
    28
}
wenzelm@2808
    29
wenzelm@2808
    30
wenzelm@2808
    31
## process command line
wenzelm@2808
    32
wenzelm@2808
    33
# options
wenzelm@2808
    34
wenzelm@2808
    35
BUILD=""
wenzelm@2808
    36
COPYDB=""
wenzelm@2917
    37
GRAPH=false
wenzelm@2917
    38
HTML=false
wenzelm@2808
    39
SESSION=""
wenzelm@2808
    40
wenzelm@2917
    41
function getoptions()
wenzelm@2917
    42
{
wenzelm@2917
    43
  OPTIND=1
wenzelm@2917
    44
  while getopts "bcg:h:s:" OPT
wenzelm@2917
    45
  do
wenzelm@2917
    46
    case "$OPT" in
wenzelm@2917
    47
      b)
wenzelm@2917
    48
        BUILD=true
wenzelm@2917
    49
        ;;
wenzelm@2917
    50
      c)
wenzelm@2917
    51
        COPYDB="-c"
wenzelm@2917
    52
        ;;
wenzelm@2917
    53
      g)
wenzelm@2917
    54
        GRAPH="$OPTARG"
wenzelm@2917
    55
        ;;
wenzelm@2917
    56
      h)
wenzelm@2917
    57
        HTML="$OPTARG"
wenzelm@2917
    58
        ;;
wenzelm@2917
    59
      s)
wenzelm@2917
    60
        SESSION="$OPTARG"
wenzelm@2917
    61
        ;;
wenzelm@2917
    62
      \?)
wenzelm@2917
    63
        usage
wenzelm@2917
    64
        ;;
wenzelm@2917
    65
    esac
wenzelm@2917
    66
  done
wenzelm@2917
    67
}
wenzelm@2808
    68
wenzelm@2917
    69
getoptions $ISABELLE_USEDIR_OPTIONS
wenzelm@2917
    70
wenzelm@2917
    71
getoptions "$@"
wenzelm@2808
    72
shift $(($OPTIND - 1))
wenzelm@2808
    73
wenzelm@2808
    74
wenzelm@2808
    75
# args
wenzelm@2808
    76
wenzelm@2808
    77
[ $# -ne 2 ] && usage
wenzelm@2808
    78
wenzelm@2808
    79
LOGIC="$1"; shift
wenzelm@2808
    80
NAME="$1"; shift
wenzelm@2808
    81
wenzelm@2808
    82
wenzelm@2808
    83
wenzelm@2808
    84
## main
wenzelm@2808
    85
wenzelm@2808
    86
[ -z "$SESSION" ] && SESSION=$(basename $NAME)
wenzelm@2808
    87
wenzelm@2808
    88
if [ -n "$BUILD" ]; then
wenzelm@2808
    89
  exec $ISABELLE \
wenzelm@2917
    90
    -e "make_html := $HTML;" \
wenzelm@2808
    91
    -e "set_session\"$SESSION\";" \
wenzelm@2808
    92
    -e "exit_use_dir\".\";" \
wenzelm@2808
    93
    -q $COPYDB $LOGIC $NAME
wenzelm@2808
    94
else
wenzelm@2808
    95
  exec $ISABELLE \
wenzelm@2917
    96
    -e "make_html := $HTML;" \
wenzelm@2808
    97
    -e "set_session\"$SESSION\";" \
wenzelm@2812
    98
    -e "exit_use_dir\"$NAME\"; quit();" \
wenzelm@2808
    99
    -r -q $LOGIC
wenzelm@2808
   100
fi