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;
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 #
     5 # DESCRIPTION: build object-logic or run examples
     6 
     7 
     8 ## diagnostics
     9 
    10 PRG=$(basename $0)
    11 
    12 function usage()
    13 {
    14   echo
    15   echo "Usage: $PRG LOGIC NAME"
    16   echo
    17   echo "  Options are:"
    18   echo "    -b           build mode (output heap image, use dir \".\")"
    19   echo "    -c           force copying of heap file (for Poly/ML)"
    20   echo "    -g BOOL      generate theory graph data (default false)"
    21   echo "    -h BOOL      generate theory HTML data (default false)"
    22   echo "    -s NAME      override session NAME"
    23   echo
    24   echo "  Build object-logic or run examples. Also creates browsing"
    25   echo "  information (HTML etc.) according to settings."
    26   echo
    27   exit 1
    28 }
    29 
    30 
    31 ## process command line
    32 
    33 # options
    34 
    35 BUILD=""
    36 COPYDB=""
    37 GRAPH=false
    38 HTML=false
    39 SESSION=""
    40 
    41 function getoptions()
    42 {
    43   OPTIND=1
    44   while getopts "bcg:h:s:" OPT
    45   do
    46     case "$OPT" in
    47       b)
    48         BUILD=true
    49         ;;
    50       c)
    51         COPYDB="-c"
    52         ;;
    53       g)
    54         GRAPH="$OPTARG"
    55         ;;
    56       h)
    57         HTML="$OPTARG"
    58         ;;
    59       s)
    60         SESSION="$OPTARG"
    61         ;;
    62       \?)
    63         usage
    64         ;;
    65     esac
    66   done
    67 }
    68 
    69 getoptions $ISABELLE_USEDIR_OPTIONS
    70 
    71 getoptions "$@"
    72 shift $(($OPTIND - 1))
    73 
    74 
    75 # args
    76 
    77 [ $# -ne 2 ] && usage
    78 
    79 LOGIC="$1"; shift
    80 NAME="$1"; shift
    81 
    82 
    83 
    84 ## main
    85 
    86 [ -z "$SESSION" ] && SESSION=$(basename $NAME)
    87 
    88 if [ -n "$BUILD" ]; then
    89   exec $ISABELLE \
    90     -e "make_html := $HTML;" \
    91     -e "set_session\"$SESSION\";" \
    92     -e "exit_use_dir\".\";" \
    93     -q $COPYDB $LOGIC $NAME
    94 else
    95   exec $ISABELLE \
    96     -e "make_html := $HTML;" \
    97     -e "set_session\"$SESSION\";" \
    98     -e "exit_use_dir\"$NAME\"; quit();" \
    99     -r -q $LOGIC
   100 fi