src/Tools/jEdit/lib/Tools/jedit
author wenzelm
Sun Nov 25 21:35:29 2012 +0100 (2012-11-25)
changeset 50208 1382ad6d4774
parent 50202 ec0f2f8dbeb9
child 50299 f70b3712040f
permissions -rwxr-xr-x
tuned signature;
wenzelm@34333
     1
#!/usr/bin/env bash
wenzelm@34333
     2
#
wenzelm@34664
     3
# Author: Makarius
wenzelm@34664
     4
#
wenzelm@34664
     5
# DESCRIPTION: Isabelle/jEdit interface wrapper
wenzelm@34664
     6
wenzelm@34333
     7
wenzelm@43285
     8
## sources
wenzelm@43285
     9
wenzelm@43320
    10
declare -a SOURCES=(
wenzelm@43285
    11
  "src/dockable.scala"
wenzelm@43285
    12
  "src/document_model.scala"
wenzelm@43285
    13
  "src/document_view.scala"
wenzelm@49570
    14
  "src/graphview_dockable.scala"
wenzelm@43285
    15
  "src/html_panel.scala"
wenzelm@48921
    16
  "src/hyperlink.scala"
wenzelm@49726
    17
  "src/info_dockable.scala"
wenzelm@50208
    18
  "src/isabelle.scala"
wenzelm@43285
    19
  "src/isabelle_encoding.scala"
wenzelm@49246
    20
  "src/isabelle_logic.scala"
wenzelm@43285
    21
  "src/isabelle_options.scala"
wenzelm@43285
    22
  "src/isabelle_sidekick.scala"
wenzelm@49406
    23
  "src/jedit_lib.scala"
wenzelm@49600
    24
  "src/jedit_main.scala"
wenzelm@50202
    25
  "src/jedit_options.scala"
wenzelm@44577
    26
  "src/jedit_thy_load.scala"
wenzelm@43285
    27
  "src/output_dockable.scala"
wenzelm@43285
    28
  "src/plugin.scala"
wenzelm@49398
    29
  "src/pretty_text_area.scala"
wenzelm@49702
    30
  "src/pretty_tooltip.scala"
wenzelm@43285
    31
  "src/protocol_dockable.scala"
wenzelm@43285
    32
  "src/raw_output_dockable.scala"
wenzelm@48014
    33
  "src/readme_dockable.scala"
wenzelm@50202
    34
  "src/rendering.scala"
wenzelm@49411
    35
  "src/rich_text_area.scala"
wenzelm@43285
    36
  "src/scala_console.scala"
wenzelm@49492
    37
  "src/sendback.scala"
wenzelm@43285
    38
  "src/session_dockable.scala"
immler@50143
    39
  "src/symbols_dockable.scala"
wenzelm@48021
    40
  "src/syslog_dockable.scala"
wenzelm@46572
    41
  "src/text_overview.scala"
wenzelm@43414
    42
  "src/token_markup.scala"
wenzelm@43285
    43
)
wenzelm@43285
    44
wenzelm@43320
    45
declare -a RESOURCES=(
wenzelm@43286
    46
  "src/actions.xml"
wenzelm@43286
    47
  "src/dockables.xml"
wenzelm@43286
    48
  "src/Isabelle.props"
wenzelm@43286
    49
  "src/services.xml"
wenzelm@43285
    50
)
wenzelm@43285
    51
wenzelm@43285
    52
wenzelm@34333
    53
## diagnostics
wenzelm@34333
    54
wenzelm@34664
    55
PRG="$(basename "$0")"
wenzelm@34664
    56
wenzelm@43284
    57
function usage()
wenzelm@34333
    58
{
wenzelm@34333
    59
  echo
wenzelm@34664
    60
  echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]"
wenzelm@34333
    61
  echo
wenzelm@34333
    62
  echo "  Options are:"
wenzelm@34333
    63
  echo "    -J OPTION    add JVM runtime option"
wenzelm@34409
    64
  echo "                 (default JEDIT_JAVA_OPTIONS=$JEDIT_JAVA_OPTIONS)"
wenzelm@43285
    65
  echo "    -b           build only"
wenzelm@48791
    66
  echo "    -d DIR       include session directory"
wenzelm@43285
    67
  echo "    -f           fresh build"
wenzelm@34333
    68
  echo "    -j OPTION    add jEdit runtime option"
wenzelm@34333
    69
  echo "                 (default JEDIT_OPTIONS=$JEDIT_OPTIONS)"
wenzelm@34333
    70
  echo "    -l NAME      logic image name (default ISABELLE_LOGIC=$ISABELLE_LOGIC)"
wenzelm@34333
    71
  echo "    -m MODE      add print mode for output"
wenzelm@34333
    72
  echo
wenzelm@34664
    73
  echo "Start jEdit with Isabelle plugin setup and opens theory FILES"
wenzelm@50114
    74
  echo "(default \"$USER_HOME/Scratch.thy\")."
wenzelm@34333
    75
  echo
wenzelm@34333
    76
  exit 1
wenzelm@34333
    77
}
wenzelm@34333
    78
wenzelm@43284
    79
function fail()
wenzelm@34333
    80
{
wenzelm@34333
    81
  echo "$1" >&2
wenzelm@34333
    82
  exit 2
wenzelm@34333
    83
}
wenzelm@34333
    84
wenzelm@43284
    85
function failed()
wenzelm@43284
    86
{
wenzelm@43284
    87
  fail "Failed!"
wenzelm@43284
    88
}
wenzelm@43284
    89
wenzelm@34333
    90
wenzelm@34333
    91
## process command line
wenzelm@34333
    92
wenzelm@34333
    93
# options
wenzelm@34333
    94
wenzelm@43285
    95
BUILD_ONLY=false
wenzelm@43285
    96
BUILD_JARS="jars"
wenzelm@48791
    97
JEDIT_SESSION_DIRS=""
wenzelm@34333
    98
JEDIT_LOGIC="$ISABELLE_LOGIC"
wenzelm@34333
    99
JEDIT_PRINT_MODE=""
wenzelm@34333
   100
wenzelm@43284
   101
function getoptions()
wenzelm@34780
   102
{
wenzelm@34780
   103
  OPTIND=1
wenzelm@48791
   104
  while getopts "J:bd:fj:l:m:" OPT
wenzelm@34780
   105
  do
wenzelm@34780
   106
    case "$OPT" in
wenzelm@34780
   107
      J)
wenzelm@34780
   108
        JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
wenzelm@34780
   109
        ;;
wenzelm@43285
   110
      b)
wenzelm@43285
   111
        BUILD_ONLY=true
wenzelm@43285
   112
        ;;
wenzelm@48791
   113
      d)
wenzelm@48791
   114
        if [ -z "$JEDIT_SESSION_DIRS" ]; then
wenzelm@48791
   115
          JEDIT_SESSION_DIRS="$OPTARG"
wenzelm@48791
   116
        else
wenzelm@48791
   117
          JEDIT_SESSION_DIRS="$JEDIT_SESSION_DIRS:$OPTARG"
wenzelm@48791
   118
        fi
wenzelm@48791
   119
        ;;
wenzelm@43285
   120
      f)
wenzelm@43285
   121
        BUILD_JARS="jars_fresh"
wenzelm@43285
   122
        ;;
wenzelm@34780
   123
      j)
wenzelm@34780
   124
        ARGS["${#ARGS[@]}"]="$OPTARG"
wenzelm@34780
   125
        ;;
wenzelm@34780
   126
      l)
wenzelm@34780
   127
        JEDIT_LOGIC="$OPTARG"
wenzelm@34780
   128
        ;;
wenzelm@34780
   129
      m)
wenzelm@34780
   130
        if [ -z "$JEDIT_PRINT_MODE" ]; then
wenzelm@34780
   131
          JEDIT_PRINT_MODE="$OPTARG"
wenzelm@34780
   132
        else
wenzelm@34780
   133
          JEDIT_PRINT_MODE="$JEDIT_PRINT_MODE,$OPTARG"
wenzelm@34780
   134
        fi
wenzelm@34780
   135
        ;;
wenzelm@34780
   136
      \?)
wenzelm@34780
   137
        usage
wenzelm@34780
   138
        ;;
wenzelm@34780
   139
    esac
wenzelm@34780
   140
  done
wenzelm@34780
   141
}
wenzelm@34581
   142
wenzelm@38257
   143
declare -a JAVA_ARGS; eval "JAVA_ARGS=($JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS)"
wenzelm@34843
   144
[ -n "$SCALA_HOME" ] && JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Dscala.home=$SCALA_HOME"
wenzelm@34843
   145
wenzelm@34780
   146
declare -a ARGS; eval "ARGS=($JEDIT_OPTIONS)"
wenzelm@34333
   147
wenzelm@34780
   148
declare -a OPTIONS; eval "OPTIONS=($ISABELLE_JEDIT_OPTIONS)"
wenzelm@34780
   149
getoptions "${OPTIONS[@]}"
wenzelm@34780
   150
wenzelm@34780
   151
getoptions "$@"
wenzelm@34333
   152
shift $(($OPTIND - 1))
wenzelm@34333
   153
wenzelm@34333
   154
wenzelm@34333
   155
# args
wenzelm@34333
   156
wenzelm@44485
   157
if [ "$#" -eq 0 ]; then
wenzelm@50120
   158
  ARGS["${#ARGS[@]}"]="$(jvmpath "$USER_HOME/Scratch.thy")"
wenzelm@44485
   159
else
wenzelm@44485
   160
  while [ "$#" -gt 0 ]; do
wenzelm@44485
   161
    ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
wenzelm@44485
   162
    shift
wenzelm@44485
   163
  done
wenzelm@44485
   164
fi
wenzelm@34333
   165
wenzelm@34333
   166
wenzelm@43284
   167
## dependencies
wenzelm@43284
   168
wenzelm@49953
   169
if [ -e "$ISABELLE_HOME/Admin/build" ]; then
wenzelm@49953
   170
  if [ "$BUILD_JARS" = jars_fresh ]; then
wenzelm@49953
   171
    "$ISABELLE_TOOL" graphview -b -f || exit $?
wenzelm@49953
   172
  else
wenzelm@49566
   173
    "$ISABELLE_HOME/Admin/build" "$BUILD_JARS" || exit $?
wenzelm@49953
   174
    "$ISABELLE_TOOL" graphview -b || exit $?
wenzelm@49953
   175
  fi
wenzelm@49953
   176
fi
wenzelm@43413
   177
wenzelm@43523
   178
PURE_JAR="$ISABELLE_HOME/lib/classes/ext/Pure.jar"
wenzelm@49566
   179
GRAPHVIEW_JAR="$ISABELLE_HOME/lib/classes/ext/Graphview.jar"
wenzelm@43413
   180
wenzelm@43285
   181
pushd "$JEDIT_HOME" >/dev/null || failed
wenzelm@43284
   182
wenzelm@43284
   183
JEDIT_JAR="$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/jedit.jar"
wenzelm@43284
   184
wenzelm@43284
   185
JEDIT_JARS=(
wenzelm@43284
   186
  "$ISABELLE_JEDIT_BUILD_HOME/contrib/Console.jar"
wenzelm@43284
   187
  "$ISABELLE_JEDIT_BUILD_HOME/contrib/ErrorList.jar"
wenzelm@43284
   188
  "$ISABELLE_JEDIT_BUILD_HOME/contrib/SideKick.jar"
wenzelm@43284
   189
  "$ISABELLE_JEDIT_BUILD_HOME/contrib/cobra.jar"
wenzelm@43284
   190
  "$ISABELLE_JEDIT_BUILD_HOME/contrib/js.jar"
wenzelm@43284
   191
)
wenzelm@43284
   192
wenzelm@43284
   193
wenzelm@43284
   194
# target
wenzelm@43284
   195
wenzelm@43284
   196
TARGET="dist/jars/Isabelle-jEdit.jar"
wenzelm@43284
   197
wenzelm@43384
   198
declare -a UPDATED=()
wenzelm@43384
   199
wenzelm@43285
   200
if [ "$BUILD_JARS" = jars_fresh ]; then
wenzelm@43285
   201
  OUTDATED=true
wenzelm@43285
   202
else
wenzelm@43285
   203
  OUTDATED=false
wenzelm@43368
   204
  if [ ! -e "$TARGET" ]; then
wenzelm@43368
   205
    OUTDATED=true
wenzelm@43384
   206
  else
wenzelm@43384
   207
    if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
wenzelm@49566
   208
      declare -a DEPS=(
wenzelm@49566
   209
        "$JEDIT_JAR" "${JEDIT_JARS[@]}"
wenzelm@49566
   210
        "$PURE_JAR" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}"
wenzelm@49566
   211
      )
wenzelm@47666
   212
    elif [ -e "$ISABELLE_HOME/Admin/build" ]; then
wenzelm@49566
   213
      declare -a DEPS=("$PURE_JAR" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
wenzelm@43384
   214
    else
wenzelm@47666
   215
      declare -a DEPS=()
wenzelm@43384
   216
    fi
wenzelm@43384
   217
    for DEP in "${DEPS[@]}"
wenzelm@43368
   218
    do
wenzelm@43384
   219
      [ ! -e "$DEP" ] && fail "Missing file: $DEP"
wenzelm@43384
   220
      [ "$DEP" -nt "$TARGET" ] && {
wenzelm@43384
   221
        OUTDATED=true
wenzelm@43384
   222
        UPDATED["${#UPDATED[@]}"]="$DEP"
wenzelm@43384
   223
      }
wenzelm@43368
   224
    done
wenzelm@43368
   225
  fi
wenzelm@43285
   226
fi
wenzelm@43284
   227
wenzelm@43284
   228
wenzelm@43284
   229
# build
wenzelm@43284
   230
wenzelm@43284
   231
if [ "$OUTDATED" = true ]
wenzelm@43284
   232
then
wenzelm@43405
   233
  echo "### Building Isabelle/jEdit ..."
wenzelm@43405
   234
wenzelm@43384
   235
  [ "${#UPDATED[@]}" -gt 0 ] && {
wenzelm@43405
   236
    echo "Changed files:"
wenzelm@43384
   237
    for FILE in "${UPDATED[@]}"
wenzelm@43384
   238
    do
wenzelm@43384
   239
      echo "  $FILE"
wenzelm@43384
   240
    done
wenzelm@43384
   241
  }
wenzelm@43384
   242
wenzelm@43284
   243
  [ -z "$ISABELLE_JEDIT_BUILD_HOME" ] && \
wenzelm@43284
   244
    fail "Unknown ISABELLE_JEDIT_BUILD_HOME -- missing auxiliary component"
wenzelm@43284
   245
wenzelm@43284
   246
  rm -rf dist || failed
wenzelm@43284
   247
  mkdir -p dist dist/classes || failed
wenzelm@43287
   248
wenzelm@46502
   249
  cp -p -R -f "$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/." dist/.
wenzelm@46502
   250
  cp -p -R -f "${RESOURCES[@]}" dist/classes/.
wenzelm@43287
   251
  cp src/jEdit.props dist/properties/.
wenzelm@46502
   252
  cp -p -R -f src/modes/. dist/modes/.
wenzelm@43284
   253
wenzelm@43391
   254
  perl -i -e 'while (<>) {
wenzelm@43391
   255
    if (m/NAME="javacc"/) {
wenzelm@43391
   256
      print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,;
wenzelm@48366
   257
      print qq,<MODE NAME="isabelle-options" FILE="isabelle-options.xml"/>\n\n,;
wenzelm@48575
   258
      print qq,<MODE NAME="isabelle-root" FILE="isabelle-root.xml" FILE_NAME_GLOB="ROOT"/>\n\n,; }
wenzelm@43391
   259
    elsif (m/NAME="scheme"/) {
wenzelm@43391
   260
      print qq,<MODE NAME="scala" FILE="scala.xml" FILE_NAME_GLOB="*.scala" />\n\n,; }
wenzelm@43284
   261
    print; }' dist/modes/catalog
wenzelm@43284
   262
wenzelm@47995
   263
  cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed
wenzelm@43284
   264
  (
wenzelm@49566
   265
    for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$GRAPHVIEW_JAR" \
wenzelm@49566
   266
      "$SCALA_HOME/lib/scala-compiler.jar"
wenzelm@43284
   267
    do
wenzelm@43284
   268
      CLASSPATH="$CLASSPATH:$JAR"
wenzelm@43284
   269
    done
wenzelm@43284
   270
    CLASSPATH="$(jvmpath "$CLASSPATH")"
wenzelm@47009
   271
    exec "$SCALA_HOME/bin/scalac" $ISABELLE_SCALA_BUILD_OPTIONS -d dist/classes "${SOURCES[@]}"
wenzelm@43284
   272
  ) || fail "Failed to compile sources"
wenzelm@43284
   273
wenzelm@43284
   274
  cd dist/classes
wenzelm@47115
   275
  isabelle_jdk jar cf "../jars/Isabelle-jEdit.jar" * || failed
wenzelm@43284
   276
  cd ../..
wenzelm@43284
   277
  rm -rf dist/classes
wenzelm@43284
   278
fi
wenzelm@43284
   279
wenzelm@43284
   280
popd >/dev/null
wenzelm@43284
   281
wenzelm@43284
   282
wenzelm@43284
   283
## main
wenzelm@43284
   284
wenzelm@43284
   285
# perspective
wenzelm@34880
   286
wenzelm@34880
   287
mkdir -p "$JEDIT_SETTINGS/DockableWindowManager"
wenzelm@34880
   288
wenzelm@34880
   289
if [ ! -e "$JEDIT_SETTINGS/perspective.xml" ]; then
wenzelm@34880
   290
  cat > "$JEDIT_SETTINGS/DockableWindowManager/perspective-view0.xml" <<EOF
wenzelm@48014
   291
<DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="isabelle-readme" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />
wenzelm@34880
   292
EOF
wenzelm@34880
   293
  cat > "$JEDIT_SETTINGS/perspective.xml" <<EOF
wenzelm@34880
   294
<?xml version="1.0" encoding="UTF-8" ?>
wenzelm@34880
   295
<!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd">
wenzelm@34880
   296
<PERSPECTIVE>
wenzelm@34880
   297
<VIEW PLAIN="FALSE">
wenzelm@34880
   298
<GEOMETRY X="0" Y="35" WIDTH="1072" HEIGHT="787" EXT_STATE="0" />
wenzelm@34880
   299
</VIEW>
wenzelm@34880
   300
</PERSPECTIVE>
wenzelm@34880
   301
EOF
wenzelm@34880
   302
fi
wenzelm@34880
   303
wenzelm@34880
   304
wenzelm@43284
   305
# run
wenzelm@34333
   306
wenzelm@43285
   307
[ "$BUILD_ONLY" = true ] || {
wenzelm@43285
   308
  case "$JEDIT_LOGIC" in
wenzelm@43285
   309
    /*)
wenzelm@43285
   310
      ;;
wenzelm@43285
   311
    */*)
wenzelm@43285
   312
      JEDIT_LOGIC="$(pwd -P)/$JEDIT_LOGIC"
wenzelm@43285
   313
      ;;
wenzelm@43285
   314
  esac
wenzelm@34333
   315
wenzelm@48791
   316
  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE
wenzelm@34333
   317
wenzelm@43285
   318
  exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \
wenzelm@43285
   319
    -jar "$(jvmpath "$JEDIT_HOME/dist/jedit.jar")" \
wenzelm@43285
   320
    "-settings=$(jvmpath "$JEDIT_SETTINGS")" "${ARGS[@]}"
wenzelm@43285
   321
}