lib/Tools/build_dialog
author traytel
Thu, 13 Dec 2012 15:39:07 +0100
changeset 50518 d4fdda801e19
parent 50405 366c4a602500
child 50546 1b01a57d2749
permissions -rwxr-xr-x
short library for streams
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50365
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
     2
#
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
     3
# Author: Makarius
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
     4
#
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
     5
# DESCRIPTION: build Isabelle session images via GUI dialog
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
     6
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
     7
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
     8
## diagnostics
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
     9
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    10
PRG="$(basename "$0")"
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    11
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    12
function usage()
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    13
{
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    14
  echo
50404
898cac1dad5e avoid startup within GUI thread -- it is only required later for dialog;
wenzelm
parents: 50403
diff changeset
    15
  echo "Usage: isabelle $PRG [OPTIONS] LOGIC"
50365
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    16
  echo
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    17
  echo "  Options are:"
50403
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50370
diff changeset
    18
  echo "    -L OPTION    default logic via system option"
50365
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    19
  echo "    -d DIR       include session directory"
50369
622002c702ad more elementary dialog, with less interaction;
wenzelm
parents: 50365
diff changeset
    20
  echo "    -s           system build mode: produce output in ISABELLE_HOME"
50365
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    21
  echo
50404
898cac1dad5e avoid startup within GUI thread -- it is only required later for dialog;
wenzelm
parents: 50403
diff changeset
    22
  echo "  Build Isabelle session image LOGIC via GUI dialog."
50365
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    23
  echo
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    24
  exit 1
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    25
}
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    26
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    27
function fail()
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    28
{
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    29
  echo "$1" >&2
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    30
  exit 2
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    31
}
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    32
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    33
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    34
## process command line
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    35
50403
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50370
diff changeset
    36
LOGIC_OPTION=""
50365
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    37
declare -a INCLUDE_DIRS=()
50369
622002c702ad more elementary dialog, with less interaction;
wenzelm
parents: 50365
diff changeset
    38
SYSTEM_MODE=false
50365
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    39
50405
366c4a602500 clarified build_dialog: regular up-to-date check (extra cost of approx. 5s startup for HOL);
wenzelm
parents: 50404
diff changeset
    40
while getopts "L:d:s" OPT
50365
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    41
do
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    42
  case "$OPT" in
50403
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50370
diff changeset
    43
    L)
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50370
diff changeset
    44
      LOGIC_OPTION="$OPTARG"
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50370
diff changeset
    45
      ;;
50365
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    46
    d)
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    47
      INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG"
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    48
      ;;
50369
622002c702ad more elementary dialog, with less interaction;
wenzelm
parents: 50365
diff changeset
    49
    s)
622002c702ad more elementary dialog, with less interaction;
wenzelm
parents: 50365
diff changeset
    50
      SYSTEM_MODE="true"
622002c702ad more elementary dialog, with less interaction;
wenzelm
parents: 50365
diff changeset
    51
      ;;
50365
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    52
    \?)
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    53
      usage
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    54
      ;;
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    55
  esac
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    56
done
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    57
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    58
shift $(($OPTIND - 1))
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    59
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    60
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    61
# args
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    62
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    63
[ "$#" -ne 1 ] && usage
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    64
50404
898cac1dad5e avoid startup within GUI thread -- it is only required later for dialog;
wenzelm
parents: 50403
diff changeset
    65
LOGIC="$1"; shift
50365
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    66
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    67
50403
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50370
diff changeset
    68
## main
50365
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    69
50403
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50370
diff changeset
    70
[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
50365
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    71
50403
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50370
diff changeset
    72
"$ISABELLE_TOOL" java isabelle.Build_Dialog \
50405
366c4a602500 clarified build_dialog: regular up-to-date check (extra cost of approx. 5s startup for HOL);
wenzelm
parents: 50404
diff changeset
    73
  "$LOGIC_OPTION" "$SYSTEM_MODE" "$LOGIC" "${INCLUDE_DIRS[@]}"
50365
82f5aea343e7 basic wrapper for session build dialog;
wenzelm
parents:
diff changeset
    74