lib/Tools/usedir
author wenzelm
Tue, 16 Dec 1997 12:24:31 +0100
changeset 4419 950001e4859a
parent 4075 8a467dc6e667
child 4451 f9e3e9f1af61
permissions -rwxr-xr-x
tuned;
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 \".\")"
3747
cd9b6c86926c There is now one single option -i for generating theory browsing
berghofe
parents: 3636
diff changeset
    19
  echo "    -i BOOL      generate theory browsing information,"
cd9b6c86926c There is now one single option -i for generating theory browsing
berghofe
parents: 3636
diff changeset
    20
  echo "                 i.e. HTML / graph 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=""
3747
cd9b6c86926c There is now one single option -i for generating theory browsing
berghofe
parents: 3636
diff changeset
    35
INFO=false
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    36
SESSION=""
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    37
2917
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    38
function getoptions()
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    39
{
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    40
  OPTIND=1
3747
cd9b6c86926c There is now one single option -i for generating theory browsing
berghofe
parents: 3636
diff changeset
    41
  while getopts "bi:s:" OPT
2917
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    42
  do
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    43
    case "$OPT" in
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    44
      b)
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    45
        BUILD=true
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    46
        ;;
3747
cd9b6c86926c There is now one single option -i for generating theory browsing
berghofe
parents: 3636
diff changeset
    47
      i)
cd9b6c86926c There is now one single option -i for generating theory browsing
berghofe
parents: 3636
diff changeset
    48
        INFO="$OPTARG"
2917
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    49
        ;;
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    50
      s)
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    51
        SESSION="$OPTARG"
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    52
        ;;
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    53
      \?)
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    54
        usage
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    55
        ;;
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    56
    esac
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    57
  done
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    58
}
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    59
2917
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    60
getoptions $ISABELLE_USEDIR_OPTIONS
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    61
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    62
getoptions "$@"
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    63
shift $(($OPTIND - 1))
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
# args
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    67
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    68
[ $# -ne 2 ] && usage
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
LOGIC="$1"; shift
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    71
NAME="$1"; shift
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    72
4419
wenzelm
parents: 4075
diff changeset
    73
[ -z "$SESSION" ] && SESSION=$(basename $NAME)
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    74
4419
wenzelm
parents: 4075
diff changeset
    75
wenzelm
parents: 4075
diff changeset
    76
wenzelm
parents: 4075
diff changeset
    77
## main
3636
3f2e55e5bacc Added some code for generating theory browsing data.
berghofe
parents: 3504
diff changeset
    78
4419
wenzelm
parents: 4075
diff changeset
    79
# prepare browser info directories
wenzelm
parents: 4075
diff changeset
    80
wenzelm
parents: 4075
diff changeset
    81
if [ "$INFO" = "true" -a ! -d $ISABELLE_BROWSER_INFO ]; then
wenzelm
parents: 4075
diff changeset
    82
3747
cd9b6c86926c There is now one single option -i for generating theory browsing
berghofe
parents: 3636
diff changeset
    83
  mkdir -p $ISABELLE_BROWSER_INFO/gif
4419
wenzelm
parents: 4075
diff changeset
    84
  cp $ISABELLE_HOME/lib/images/blue_arrow.gif $ISABELLE_BROWSER_INFO/gif
wenzelm
parents: 4075
diff changeset
    85
  cp $ISABELLE_HOME/lib/images/red_arrow.gif $ISABELLE_BROWSER_INFO/gif
3848
97bb3ff3c771 non-transparent logo;
wenzelm
parents: 3844
diff changeset
    86
  cp $ISABELLE_HOME/lib/logo/isabelle.gif $ISABELLE_BROWSER_INFO/gif/isabelle.gif
3747
cd9b6c86926c There is now one single option -i for generating theory browsing
berghofe
parents: 3636
diff changeset
    87
  cp $ISABELLE_HOME/lib/html/index1.html $ISABELLE_BROWSER_INFO/index.html
4419
wenzelm
parents: 4075
diff changeset
    88
3636
3f2e55e5bacc Added some code for generating theory browsing data.
berghofe
parents: 3504
diff changeset
    89
  mkdir -p $ISABELLE_BROWSER_INFO/graph
3f2e55e5bacc Added some code for generating theory browsing data.
berghofe
parents: 3504
diff changeset
    90
  cp $ISABELLE_HOME/lib/html/index2.html $ISABELLE_BROWSER_INFO/graph/index.html
3f2e55e5bacc Added some code for generating theory browsing data.
berghofe
parents: 3504
diff changeset
    91
  mkdir $ISABELLE_BROWSER_INFO/graph/GraphBrowser
3f2e55e5bacc Added some code for generating theory browsing data.
berghofe
parents: 3504
diff changeset
    92
  mkdir $ISABELLE_BROWSER_INFO/graph/awtUtilities
4419
wenzelm
parents: 4075
diff changeset
    93
  cp $ISABELLE_HOME/lib/browser/GraphBrowser/*.class $ISABELLE_BROWSER_INFO/graph/GraphBrowser
wenzelm
parents: 4075
diff changeset
    94
  cp $ISABELLE_HOME/lib/browser/awtUtilities/*.class $ISABELLE_BROWSER_INFO/graph/awtUtilities
wenzelm
parents: 4075
diff changeset
    95
3636
3f2e55e5bacc Added some code for generating theory browsing data.
berghofe
parents: 3504
diff changeset
    96
fi
3f2e55e5bacc Added some code for generating theory browsing data.
berghofe
parents: 3504
diff changeset
    97
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    98
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    99
if [ -n "$BUILD" ]; then
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   100
  exec $ISABELLE \
4075
8a467dc6e667 set_session renamed to add_session;
wenzelm
parents: 3848
diff changeset
   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;" \
3504
8493dbe2f009 -w option;
wenzelm
parents: 3264
diff changeset
   102
    -q -w $LOGIC $NAME
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   103
else
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   104
  exec $ISABELLE \
4075
8a467dc6e667 set_session renamed to add_session;
wenzelm
parents: 3848
diff changeset
   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();" \
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   106
    -r -q $LOGIC
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   107
fi