lib/Tools/jedit
author wenzelm
Sat Jul 25 10:31:27 2009 +0200 (2009-07-25)
changeset 32187 cca43ca13f4f
parent 29143 72c960b2b83e
permissions -rwxr-xr-x
renamed structure Display_Goal to Goal_Display;
wenzelm@28649
     1
#!/usr/bin/env bash
wenzelm@28649
     2
#
wenzelm@28649
     3
# Author: Makarius
wenzelm@28649
     4
#
wenzelm@28649
     5
# DESCRIPTION: Isabelle/jEdit interface wrapper
wenzelm@28649
     6
wenzelm@28649
     7
wenzelm@28649
     8
## diagnostics
wenzelm@28649
     9
wenzelm@28649
    10
function fail()
wenzelm@28649
    11
{
wenzelm@28649
    12
  echo "$1" >&2
wenzelm@28649
    13
  exit 2
wenzelm@28649
    14
}
wenzelm@28649
    15
wenzelm@28649
    16
wenzelm@28649
    17
## main
wenzelm@28649
    18
wenzelm@28649
    19
[ -z "$JEDIT_HOME" ] && fail "Missing Isabelle/jEdit installation (JEDIT_HOME)"
wenzelm@28649
    20
wenzelm@28649
    21
INTERFACE="$JEDIT_HOME/interface"
wenzelm@28649
    22
[ ! -x "$INTERFACE" ] && fail "Bad interface script: \"$INTERFACE\""
wenzelm@28649
    23
wenzelm@28649
    24
exec "$INTERFACE" "$@"