lib/Tools/usedir
author wenzelm
Tue Dec 16 12:24:31 1997 +0100 (1997-12-16)
changeset 4419 950001e4859a
parent 4075 8a467dc6e667
child 4451 f9e3e9f1af61
permissions -rwxr-xr-x
tuned;
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 \".\")"
berghofe@3747
    19
  echo "    -i BOOL      generate theory browsing information,"
berghofe@3747
    20
  echo "                 i.e. HTML / graph data (default false)"
wenzelm@2808
    21
  echo "    -s NAME      override session NAME"
wenzelm@2808
    22
  echo
wenzelm@2808
    23
  echo "  Build object-logic or run examples. Also creates browsing"
wenzelm@2808
    24
  echo "  information (HTML etc.) according to settings."
wenzelm@2808
    25
  echo
wenzelm@2808
    26
  exit 1
wenzelm@2808
    27
}
wenzelm@2808
    28
wenzelm@2808
    29
wenzelm@2808
    30
## process command line
wenzelm@2808
    31
wenzelm@2808
    32
# options
wenzelm@2808
    33
wenzelm@2808
    34
BUILD=""
berghofe@3747
    35
INFO=false
wenzelm@2808
    36
SESSION=""
wenzelm@2808
    37
wenzelm@2917
    38
function getoptions()
wenzelm@2917
    39
{
wenzelm@2917
    40
  OPTIND=1
berghofe@3747
    41
  while getopts "bi:s:" OPT
wenzelm@2917
    42
  do
wenzelm@2917
    43
    case "$OPT" in
wenzelm@2917
    44
      b)
wenzelm@2917
    45
        BUILD=true
wenzelm@2917
    46
        ;;
berghofe@3747
    47
      i)
berghofe@3747
    48
        INFO="$OPTARG"
wenzelm@2917
    49
        ;;
wenzelm@2917
    50
      s)
wenzelm@2917
    51
        SESSION="$OPTARG"
wenzelm@2917
    52
        ;;
wenzelm@2917
    53
      \?)
wenzelm@2917
    54
        usage
wenzelm@2917
    55
        ;;
wenzelm@2917
    56
    esac
wenzelm@2917
    57
  done
wenzelm@2917
    58
}
wenzelm@2808
    59
wenzelm@2917
    60
getoptions $ISABELLE_USEDIR_OPTIONS
wenzelm@2917
    61
wenzelm@2917
    62
getoptions "$@"
wenzelm@2808
    63
shift $(($OPTIND - 1))
wenzelm@2808
    64
wenzelm@2808
    65
wenzelm@2808
    66
# args
wenzelm@2808
    67
wenzelm@2808
    68
[ $# -ne 2 ] && usage
wenzelm@2808
    69
wenzelm@2808
    70
LOGIC="$1"; shift
wenzelm@2808
    71
NAME="$1"; shift
wenzelm@2808
    72
wenzelm@4419
    73
[ -z "$SESSION" ] && SESSION=$(basename $NAME)
wenzelm@2808
    74
wenzelm@4419
    75
wenzelm@4419
    76
wenzelm@4419
    77
## main
berghofe@3636
    78
wenzelm@4419
    79
# prepare browser info directories
wenzelm@4419
    80
wenzelm@4419
    81
if [ "$INFO" = "true" -a ! -d $ISABELLE_BROWSER_INFO ]; then
wenzelm@4419
    82
berghofe@3747
    83
  mkdir -p $ISABELLE_BROWSER_INFO/gif
wenzelm@4419
    84
  cp $ISABELLE_HOME/lib/images/blue_arrow.gif $ISABELLE_BROWSER_INFO/gif
wenzelm@4419
    85
  cp $ISABELLE_HOME/lib/images/red_arrow.gif $ISABELLE_BROWSER_INFO/gif
wenzelm@3848
    86
  cp $ISABELLE_HOME/lib/logo/isabelle.gif $ISABELLE_BROWSER_INFO/gif/isabelle.gif
berghofe@3747
    87
  cp $ISABELLE_HOME/lib/html/index1.html $ISABELLE_BROWSER_INFO/index.html
wenzelm@4419
    88
berghofe@3636
    89
  mkdir -p $ISABELLE_BROWSER_INFO/graph
berghofe@3636
    90
  cp $ISABELLE_HOME/lib/html/index2.html $ISABELLE_BROWSER_INFO/graph/index.html
berghofe@3636
    91
  mkdir $ISABELLE_BROWSER_INFO/graph/GraphBrowser
berghofe@3636
    92
  mkdir $ISABELLE_BROWSER_INFO/graph/awtUtilities
wenzelm@4419
    93
  cp $ISABELLE_HOME/lib/browser/GraphBrowser/*.class $ISABELLE_BROWSER_INFO/graph/GraphBrowser
wenzelm@4419
    94
  cp $ISABELLE_HOME/lib/browser/awtUtilities/*.class $ISABELLE_BROWSER_INFO/graph/awtUtilities
wenzelm@4419
    95
berghofe@3636
    96
fi
berghofe@3636
    97
wenzelm@2808
    98
wenzelm@2808
    99
if [ -n "$BUILD" ]; then
wenzelm@2808
   100
  exec $ISABELLE \
wenzelm@4075
   101
    -e "make_html := $INFO; make_graph := $INFO; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; add_session\"$SESSION\"; exit_use_dir\".\"; make_html := false; make_graph := false;" \
wenzelm@3504
   102
    -q -w $LOGIC $NAME
wenzelm@2808
   103
else
wenzelm@2808
   104
  exec $ISABELLE \
wenzelm@4075
   105
    -e "make_html := $INFO; make_graph := $INFO; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; add_session\"$SESSION\"; exit_use_dir\"$NAME\"; make_html := false; make_graph := false; quit();" \
wenzelm@2808
   106
    -r -q $LOGIC
wenzelm@2808
   107
fi