lib/Tools/usedir
author wenzelm
Tue, 18 Mar 1997 18:20:52 +0100
changeset 2812 dfcd1b00f294
parent 2808 e8a224e41b9f
child 2849 01a536a6e4fb
permissions -rwxr-xr-x
added quit();
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
     1
#!/bin/bash -norc
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
     2
#
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
     3
# $Id$
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
     4
#
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
     5
# DESCRIPTION: build object-logic or run examples
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
     6
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
     7
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
     8
## diagnostics
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
     9
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    10
PRG=$(basename $0)
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    11
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    12
function usage()
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    13
{
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    14
  echo
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    15
  echo "Usage: $PRG LOGIC NAME"
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    16
  echo
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    17
  echo "  Options are:"
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    18
  echo "    -b           build mode (output heap image, use dir \".\")"
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    19
  echo "    -c           force copying of heap file (for Poly/ML)"
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    20
  echo "    -s NAME      override session NAME"
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    21
  echo
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    22
  echo "  Build object-logic or run examples. Also creates browsing"
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    23
  echo "  information (HTML etc.) according to settings."
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    24
  echo
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    25
  exit 1
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    26
}
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    27
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    28
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    29
## process command line
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    30
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    31
# options
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    32
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    33
BUILD=""
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    34
COPYDB=""
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    35
SESSION=""
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    36
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    37
while getopts "bc" OPT
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    38
do
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    39
  case "$OPT" in
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    40
    b)
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    41
      BUILD=true
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    42
      ;;
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    43
    c)
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    44
      COPYDB="-c"
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    45
      ;;
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    46
    s)
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    47
      SESSION="$OPTARG"
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    48
      ;;
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    49
    \?)
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    50
      usage
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    51
      ;;
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    52
  esac
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    53
done
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    54
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    55
shift $(($OPTIND - 1))
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    56
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    57
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    58
# args
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    59
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    60
[ $# -ne 2 ] && usage
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    61
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    62
LOGIC="$1"; shift
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    63
NAME="$1"; shift
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    64
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    65
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    66
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    67
## main
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    68
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    69
[ -z "$SESSION" ] && SESSION=$(basename $NAME)
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    70
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    71
if [ -n "$BUILD" ]; then
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    72
  exec $ISABELLE \
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    73
    -e "make_html := $ISABELLE_HTML;" \
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    74
    -e "set_session\"$SESSION\";" \
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    75
    -e "exit_use_dir\".\";" \
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    76
    -q $COPYDB $LOGIC $NAME
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    77
else
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    78
  exec $ISABELLE \
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    79
    -e "make_html := $ISABELLE_HTML;" \
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    80
    -e "set_session\"$SESSION\";" \
2812
dfcd1b00f294 added quit();
wenzelm
parents: 2808
diff changeset
    81
    -e "exit_use_dir\"$NAME\"; quit();" \
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    82
    -r -q $LOGIC
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    83
fi