lib/Tools/usedir
author paulson
Thu, 05 Jun 1997 13:22:25 +0200
changeset 3403 6cc663f6d62e
parent 3264 4ca0b6507ed5
child 3504 8493dbe2f009
permissions -rwxr-xr-x
A slight simplification of optstring The new "simpset" keyword in the "recdef" declaration
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3007
e5efa177ee0c removed -norc;
wenzelm
parents: 2917
diff changeset
     1
#!/bin/bash
2808
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 \".\")"
2917
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    19
  echo "    -g BOOL      generate theory graph data (default false)"
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    20
  echo "    -h BOOL      generate theory HTML data (default false)"
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    21
  echo "    -s NAME      override session NAME"
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    22
  echo
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    23
  echo "  Build object-logic or run examples. Also creates browsing"
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    24
  echo "  information (HTML etc.) according to settings."
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    25
  echo
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    26
  exit 1
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
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    30
## process command line
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    31
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    32
# options
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    33
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    34
BUILD=""
2917
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    35
GRAPH=false
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    36
HTML=false
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    37
SESSION=""
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    38
2917
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    39
function getoptions()
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    40
{
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    41
  OPTIND=1
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    42
  while getopts "bcg:h:s:" OPT
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    43
  do
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    44
    case "$OPT" in
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    45
      b)
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    46
        BUILD=true
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    47
        ;;
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    48
      g)
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    49
        GRAPH="$OPTARG"
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    50
        ;;
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    51
      h)
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    52
        HTML="$OPTARG"
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    53
        ;;
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    54
      s)
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    55
        SESSION="$OPTARG"
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    56
        ;;
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    57
      \?)
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    58
        usage
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    59
        ;;
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    60
    esac
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    61
  done
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    62
}
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    63
2917
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    64
getoptions $ISABELLE_USEDIR_OPTIONS
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    65
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    66
getoptions "$@"
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    67
shift $(($OPTIND - 1))
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
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    70
# args
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    71
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    72
[ $# -ne 2 ] && usage
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    73
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    74
LOGIC="$1"; shift
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    75
NAME="$1"; shift
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    76
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    77
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    78
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    79
## main
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    80
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    81
[ -z "$SESSION" ] && SESSION=$(basename $NAME)
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    82
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    83
if [ -n "$BUILD" ]; then
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    84
  exec $ISABELLE \
3264
4ca0b6507ed5 tuned command line;
wenzelm
parents: 3254
diff changeset
    85
    -e "make_html := $HTML; set_session\"$SESSION\"; exit_use_dir\".\"; make_html := false;" \
3054
c16029f41ad9 removed -c option;
wenzelm
parents: 3007
diff changeset
    86
    -q $LOGIC $NAME
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    87
else
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    88
  exec $ISABELLE \
3264
4ca0b6507ed5 tuned command line;
wenzelm
parents: 3254
diff changeset
    89
    -e "make_html := $HTML; set_session\"$SESSION\"; exit_use_dir\"$NAME\"; make_html := false; quit();" \
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    90
    -r -q $LOGIC
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    91
fi