Admin/ProofGeneral/3.7.1.1/interface
author blanchet
Mon, 19 May 2014 23:43:53 +0200
changeset 57005 33f3d2ea803d
parent 41639 d1cac8c778ed
permissions -rwxr-xr-x
store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33901
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
     2
#
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
     3
# interface,v 9.1 2008/02/06 15:40:45 makarius Exp
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
     4
#
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
     5
# Proof General interface wrapper for Isabelle.
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
     6
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
     7
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
     8
## self references
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
     9
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    10
THIS="$(cd "$(dirname "$0")"; pwd)"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    11
SUPER="$(cd "$THIS/.."; pwd)"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    12
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    13
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    14
## diagnostics
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    15
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    16
usage()
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    17
{
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    18
  echo
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    19
  echo "Usage: Isabelle [OPTIONS] [FILES ...]"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    20
  echo
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    21
  echo "  Options are:"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    22
  echo "    -I BOOL      use Isabelle/Isar (default: true, implied by -P true)"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    23
  echo "    -L NAME      abbreviates -l NAME -k NAME"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    24
  echo "    -P BOOL      actually start Proof General (default true), otherwise"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    25
  echo "                 run plain tty session"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    26
  echo "    -U BOOL      enable Unicode (UTF-8) communication (default true)"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    27
  echo "    -X BOOL      configure the X-Symbol package on startup (default true)"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    28
  echo "    -f SIZE      set X-Symbol font size (default 12)"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    29
  echo "    -g GEOMETRY  specify Emacs geometry"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    30
  echo "    -k NAME      use specific isar-keywords for named logic"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    31
  echo "    -l NAME      logic image name (default \$ISABELLE_LOGIC=$ISABELLE_LOGIC)"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    32
  echo "    -m MODE      add print mode for output"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    33
  echo "    -p NAME      Emacs program name (default emacs)"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    34
  echo "    -u BOOL      use personal .emacs file (default true)"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    35
  echo "    -w BOOL      use window system (default true)"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    36
  echo "    -x BOOL      enable the X-Symbol package on startup (default false)"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    37
  echo
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    38
  echo "Starts Proof General for Isabelle with theory and proof FILES"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    39
  echo "(default Scratch.thy)."
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    40
  echo
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    41
  echo "  PROOFGENERAL_OPTIONS=$PROOFGENERAL_OPTIONS"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    42
  echo
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    43
  exit 1
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    44
}
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    45
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    46
fail()
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    47
{
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    48
  echo "$1" >&2
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    49
  exit 2
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    50
}
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    51
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    52
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    53
## process command line
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    54
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    55
# options
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    56
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    57
ISABELLE_OPTIONS=""
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    58
ISAR="true"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    59
START_PG="true"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    60
GEOMETRY=""
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    61
KEYWORDS=""
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    62
LOGIC="$ISABELLE_LOGIC"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    63
PROGNAME="emacs"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    64
INITFILE="true"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    65
WINDOWSYSTEM="true"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    66
XSYMBOL=""
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    67
XSYMBOL_SETUP=true
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    68
XSYMBOL_FONTSIZE="12"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    69
UNICODE=""
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    70
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    71
getoptions()
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    72
{
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    73
  OPTIND=1
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    74
  while getopts "I:L:P:U:X:f:g:k:l:m:p:u:w:x:" OPT
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    75
  do
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    76
    case "$OPT" in
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    77
      I)
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    78
        ISAR="$OPTARG"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    79
        ;;
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    80
      L)
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    81
        KEYWORDS="$OPTARG"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    82
        LOGIC="$OPTARG"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    83
        ;;
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    84
      P)
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    85
        START_PG="$OPTARG"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    86
        ;;
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    87
      U)
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    88
        UNICODE="$OPTARG"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    89
        ;;
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    90
      X)
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    91
        XSYMBOL_SETUP="$OPTARG"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    92
        ;;
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    93
      f)
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    94
        XSYMBOL_FONTSIZE="$OPTARG"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    95
        ;;
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    96
      g)
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    97
        GEOMETRY="$OPTARG"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    98
        ;;
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
    99
      k)
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   100
        KEYWORDS="$OPTARG"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   101
        ;;
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   102
      l)
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   103
        LOGIC="$OPTARG"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   104
        ;;
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   105
      m)
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   106
        if [ -z "$ISABELLE_OPTIONS" ]; then
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   107
          ISABELLE_OPTIONS="-m $OPTARG"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   108
        else
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   109
          ISABELLE_OPTIONS="$ISABELLE_OPTIONS -m $OPTARG"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   110
        fi
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   111
        ;;
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   112
      p)
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   113
        PROGNAME="$OPTARG"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   114
        ;;
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   115
      u)
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   116
        INITFILE="$OPTARG"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   117
        ;;
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   118
      w)
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   119
        WINDOWSYSTEM="$OPTARG"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   120
        ;;
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   121
      x)
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   122
        XSYMBOL="$OPTARG"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   123
        ;;
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   124
      \?)
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   125
        usage
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   126
        ;;
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   127
    esac
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   128
  done
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   129
}
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   130
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   131
eval "OPTIONS=($PROOFGENERAL_OPTIONS)"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   132
getoptions "${OPTIONS[@]}"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   133
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   134
getoptions "$@"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   135
shift $(($OPTIND - 1))
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   136
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   137
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   138
# args
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   139
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   140
declare -a FILES=()
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   141
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   142
if [ "$#" -eq 0 ]; then
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   143
  FILES["${#FILES[@]}"]="Scratch.thy"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   144
else
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   145
  while [ "$#" -gt 0 ]; do
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   146
    FILES["${#FILES[@]}"]="$1"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   147
    shift
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   148
  done
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   149
fi
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   150
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   151
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   152
## smart X11 font installation
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   153
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   154
function checkfonts ()
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   155
{
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   156
  XLSFONTS=$(xlsfonts -fn "-xsymb-xsymb0-*" 2>&1) || return 1
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   157
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   158
  case "$XLSFONTS" in
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   159
    xlsfonts:*)
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   160
      return 1
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   161
      ;;
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   162
  esac
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   163
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   164
  return 0
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   165
}
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   166
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   167
function installfonts ()
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   168
{
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   169
  checkfonts "$XSYMBOL_PATTERN" || eval $XSYMBOL_INSTALLFONTS
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   170
}
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   171
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   172
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   173
## main
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   174
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   175
# Isabelle2008 compatibility
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   176
[ -z "$ISABELLE_PROCESS" ] && export ISABELLE_PROCESS="$ISABELLE"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   177
[ -z "$ISABELLE_TOOL" ] && export ISABELLE_TOOL="$ISATOOL"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   178
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   179
if [ "$START_PG" = false ]; then
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   180
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   181
  [ "$ISAR" = true ] && ISABELLE_OPTIONS="$ISABELLE_OPTIONS -I"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   182
  exec "$ISABELLE_PROCESS" $ISABELLE_OPTIONS "$LOGIC"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   183
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   184
else
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   185
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   186
  declare -a ARGS=()
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   187
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   188
  if [ -n "$GEOMETRY" ]; then
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   189
    ARGS["${#ARGS[@]}"]="-geometry"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   190
    ARGS["${#ARGS[@]}"]="$GEOMETRY"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   191
  fi
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   192
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   193
  [ "$INITFILE" = false ] && ARGS["${#ARGS[@]}"]="-q"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   194
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   195
  if [ "$WINDOWSYSTEM" = false ]; then
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   196
    ARGS["${#ARGS[@]}"]="-nw"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   197
    XSYMBOL=false
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   198
  elif [ -z "$DISPLAY" ]; then
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   199
    XSYMBOL=false
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   200
  else
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   201
    [ -n "$XSYMBOL_INSTALLFONTS" -a "$XSYMBOL_SETUP" = true ] && installfonts
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   202
  fi
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   203
33902
ea0e7ac4aaad implicit font installation for Mac OS;
wenzelm
parents: 33901
diff changeset
   204
  if [ $(uname -s) = Darwin -a -d "$HOME/Library/Fonts" ]
ea0e7ac4aaad implicit font installation for Mac OS;
wenzelm
parents: 33901
diff changeset
   205
  then
ea0e7ac4aaad implicit font installation for Mac OS;
wenzelm
parents: 33901
diff changeset
   206
    if [ ! -f "$HOME/Library/Fonts/XSymb0Medium.ttf" -o ! -f "$HOME/Library/Fonts/XSymb1Medium.ttf" ]
ea0e7ac4aaad implicit font installation for Mac OS;
wenzelm
parents: 33901
diff changeset
   207
    then
ea0e7ac4aaad implicit font installation for Mac OS;
wenzelm
parents: 33901
diff changeset
   208
      cp -f "$SUPER/x-symbol/etc/fonts-ttf/XSymb0Medium.ttf" "$HOME/Library/Fonts/"
ea0e7ac4aaad implicit font installation for Mac OS;
wenzelm
parents: 33901
diff changeset
   209
      cp -f "$SUPER/x-symbol/etc/fonts-ttf/XSymb1Medium.ttf" "$HOME/Library/Fonts/"
33903
14ff44e21bec adhoc delay after font installation -- increases chance that Emacs will actually see them;
wenzelm
parents: 33902
diff changeset
   210
      sleep 3
33902
ea0e7ac4aaad implicit font installation for Mac OS;
wenzelm
parents: 33901
diff changeset
   211
    fi
ea0e7ac4aaad implicit font installation for Mac OS;
wenzelm
parents: 33901
diff changeset
   212
  fi
ea0e7ac4aaad implicit font installation for Mac OS;
wenzelm
parents: 33901
diff changeset
   213
33901
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   214
  ARGS["${#ARGS[@]}"]="-l"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   215
  ARGS["${#ARGS[@]}"]="$SUPER/isar/interface-setup.el"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   216
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   217
  if [ -n "$KEYWORDS" ]; then
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   218
    if [ -f "$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" ]; then
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   219
      ARGS["${#ARGS[@]}"]="-l"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   220
      ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   221
    elif [ -f "$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el" ]; then
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   222
      ARGS["${#ARGS[@]}"]="-l"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   223
      ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   224
    else
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   225
      fail "No isar-keywords file for '$KEYWORDS'"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   226
    fi
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   227
  elif [ -f "$ISABELLE_HOME_USER/etc/isar-keywords.el" ]; then
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   228
    ARGS["${#ARGS[@]}"]="-l"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   229
    ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords.el"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   230
  elif [ -f "$ISABELLE_HOME/etc/isar-keywords.el" ]; then
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   231
    ARGS["${#ARGS[@]}"]="-l"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   232
    ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords.el"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   233
  fi
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   234
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   235
  for FILE in "$ISABELLE_HOME/etc/proofgeneral-settings.el" \
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   236
      "$ISABELLE_HOME_USER/etc/proofgeneral-settings.el"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   237
  do
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   238
    if [ -f "$FILE" ]; then
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   239
      ARGS["${#ARGS[@]}"]="-l"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   240
      ARGS["${#ARGS[@]}"]="$FILE"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   241
    fi
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   242
  done
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   243
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   244
  case "$LOGIC" in
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   245
    /*)
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   246
      ;;
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   247
    */*)
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   248
      LOGIC="$(pwd -P)/$LOGIC"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   249
      ;;
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   250
  esac
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   251
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   252
  export PROOFGENERAL_HOME="$SUPER"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   253
  export PROOFGENERAL_ASSISTANTS="isar"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   254
  export PROOFGENERAL_LOGIC="$LOGIC"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   255
  export PROOFGENERAL_XSYMBOL="$XSYMBOL"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   256
  export PROOFGENERAL_UNICODE="$UNICODE"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   257
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   258
  export ISABELLE_OPTIONS XSYMBOL_FONTSIZE
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   259
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   260
  exec "$PROGNAME" "${ARGS[@]}" "${FILES[@]}"
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   261
2202882e5ec7 modernized interface script for PG 3.7.1 -- backport from PG 4.0 branch;
wenzelm
parents:
diff changeset
   262
fi