1#!/usr/bin/env bash
2#
3# Author: Makarius
4#
5# DESCRIPTION: Isabelle/jEdit interface wrapper
6
7
8## sources
9
10declare -a SOURCES_BASE=(
11  "src-base/dockable.scala"
12  "src-base/isabelle_encoding.scala"
13  "src-base/jedit_lib.scala"
14  "src-base/pide_docking_framework.scala"
15  "src-base/plugin.scala"
16  "src-base/syntax_style.scala"
17)
18
19declare -a RESOURCES_BASE=(
20  "src-base/Isabelle_Base.props"
21  "src-base/services.xml"
22)
23
24declare -a SOURCES=(
25  "src/active.scala"
26  "src/completion_popup.scala"
27  "src/context_menu.scala"
28  "src/debugger_dockable.scala"
29  "src/document_model.scala"
30  "src/document_view.scala"
31  "src/documentation_dockable.scala"
32  "src/fold_handling.scala"
33  "src/font_info.scala"
34  "src/graphview_dockable.scala"
35  "src/info_dockable.scala"
36  "src/isabelle.scala"
37  "src/isabelle_encoding.scala"
38  "src/isabelle_options.scala"
39  "src/isabelle_sidekick.scala"
40  "src/jedit_bibtex.scala"
41  "src/jedit_editor.scala"
42  "src/jedit_lib.scala"
43  "src/jedit_options.scala"
44  "src/jedit_rendering.scala"
45  "src/jedit_resources.scala"
46  "src/jedit_sessions.scala"
47  "src/jedit_spell_checker.scala"
48  "src/keymap_merge.scala"
49  "src/monitor_dockable.scala"
50  "src/output_dockable.scala"
51  "src/plugin.scala"
52  "src/pretty_text_area.scala"
53  "src/pretty_tooltip.scala"
54  "src/process_indicator.scala"
55  "src/protocol_dockable.scala"
56  "src/query_dockable.scala"
57  "src/raw_output_dockable.scala"
58  "src/rich_text_area.scala"
59  "src/scala_console.scala"
60  "src/session_build.scala"
61  "src/simplifier_trace_dockable.scala"
62  "src/simplifier_trace_window.scala"
63  "src/sledgehammer_dockable.scala"
64  "src/state_dockable.scala"
65  "src/symbols_dockable.scala"
66  "src/syntax_style.scala"
67  "src/syslog_dockable.scala"
68  "src/text_overview.scala"
69  "src/text_structure.scala"
70  "src/theories_dockable.scala"
71  "src/timing_dockable.scala"
72  "src/token_markup.scala"
73)
74
75declare -a RESOURCES=(
76  "src/actions.xml"
77  "src/dockables.xml"
78  "src/Isabelle.props"
79  "src/jEdit.props"
80  "src/services.xml"
81  "src/modes/isabelle-ml.xml"
82  "src/modes/isabelle-news.xml"
83  "src/modes/isabelle-options.xml"
84  "src/modes/isabelle-root.xml"
85  "src/modes/isabelle.xml"
86  "src/modes/sml.xml"
87)
88
89
90## diagnostics
91
92PRG="$(basename "$0")"
93
94function usage()
95{
96  echo
97  echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]"
98  echo
99  echo "  Options are:"
100  echo "    -A NAME      ancestor session for options -R and -S (default: parent)"
101  echo "    -D NAME=X    set JVM system property"
102  echo "    -J OPTION    add JVM runtime option"
103  echo "                 (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
104  echo "    -R NAME      build image with requirements from other sessions"
105  echo "    -S NAME      like option -R, with focus on selected session"
106  echo "    -b           build only"
107  echo "    -d DIR       include session directory"
108  echo "    -f           fresh build"
109  echo "    -i NAME      include session in name-space of theories"
110  echo "    -j OPTION    add jEdit runtime option"
111  echo "                 (default $JEDIT_OPTIONS)"
112  echo "    -l NAME      logic session name"
113  echo "    -m MODE      add print mode for output"
114  echo "    -n           no build of session image on startup"
115  echo "    -p CMD       ML process command prefix (process policy)"
116  echo "    -s           system build mode for session image"
117  echo
118  echo "  Start jEdit with Isabelle plugin setup and open FILES"
119  echo "  (default \"$USER_HOME/Scratch.thy\" or \":\" for empty buffer)."
120  echo
121  exit 1
122}
123
124function fail()
125{
126  echo "$1" >&2
127  exit 2
128}
129
130function failed()
131{
132  fail "Failed!"
133}
134
135
136## process command line
137
138# options
139
140BUILD_ONLY=false
141BUILD_JARS="jars"
142ML_PROCESS_POLICY=""
143JEDIT_LOGIC_ANCESTOR=""
144JEDIT_LOGIC_REQUIREMENTS=""
145JEDIT_LOGIC_FOCUS=""
146JEDIT_INCLUDE_SESSIONS=""
147JEDIT_SESSION_DIRS=""
148JEDIT_LOGIC=""
149JEDIT_PRINT_MODE=""
150JEDIT_BUILD_MODE="normal"
151
152function getoptions()
153{
154  OPTIND=1
155  while getopts "A:BFD:J:R:S:bd:fi:j:l:m:np:s" OPT
156  do
157    case "$OPT" in
158      A)
159        JEDIT_LOGIC_ANCESTOR="$OPTARG"
160        ;;
161      D)
162        JAVA_ARGS["${#JAVA_ARGS[@]}"]="-D$OPTARG"
163        ;;
164      J)
165        JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
166        ;;
167      R)
168        JEDIT_LOGIC="$OPTARG"
169        JEDIT_LOGIC_REQUIREMENTS="true"
170        ;;
171      S)
172        JEDIT_LOGIC="$OPTARG"
173        JEDIT_LOGIC_REQUIREMENTS="true"
174        JEDIT_LOGIC_FOCUS="true"
175        ;;
176      b)
177        BUILD_ONLY=true
178        ;;
179      d)
180        if [ -z "$JEDIT_SESSION_DIRS" ]; then
181          JEDIT_SESSION_DIRS="$OPTARG"
182        else
183          JEDIT_SESSION_DIRS="$JEDIT_SESSION_DIRS:$OPTARG"
184        fi
185        ;;
186      i)
187        if [ -z "$JEDIT_INCLUDE_SESSIONS" ]; then
188          JEDIT_INCLUDE_SESSIONS="$OPTARG"
189        else
190          JEDIT_INCLUDE_SESSIONS="$JEDIT_INCLUDE_SESSIONS:$OPTARG"
191        fi
192        ;;
193      f)
194        BUILD_JARS="jars_fresh"
195        ;;
196      j)
197        ARGS["${#ARGS[@]}"]="$OPTARG"
198        ;;
199      l)
200        JEDIT_LOGIC="$OPTARG"
201        ;;
202      m)
203        if [ -z "$JEDIT_PRINT_MODE" ]; then
204          JEDIT_PRINT_MODE="$OPTARG"
205        else
206          JEDIT_PRINT_MODE="$JEDIT_PRINT_MODE,$OPTARG"
207        fi
208        ;;
209      n)
210        JEDIT_BUILD_MODE="none"
211        ;;
212      p)
213        ML_PROCESS_POLICY="$OPTARG"
214        ;;
215      s)
216        JEDIT_BUILD_MODE="system"
217        ;;
218      \?)
219        usage
220        ;;
221    esac
222  done
223}
224
225eval "declare -a JAVA_ARGS=($JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
226
227declare -a ARGS=()
228
229declare -a OPTIONS; eval "OPTIONS=($ISABELLE_JEDIT_OPTIONS)"
230getoptions "${OPTIONS[@]}"
231
232getoptions "$@"
233shift $(($OPTIND - 1))
234
235
236# args
237
238while [ "$#" -gt 0 ]; do
239  ARGS["${#ARGS[@]}"]="$(platform_path "$1")"
240  shift
241done
242
243
244## dependencies
245
246if [ -e "$ISABELLE_HOME/Admin/build" ]; then
247  isabelle browser -b || exit $?
248  "$ISABELLE_HOME/Admin/build" "$BUILD_JARS" || exit $?
249fi
250
251PURE_JAR="$ISABELLE_HOME/lib/classes/Pure.jar"
252
253pushd "$JEDIT_HOME" >/dev/null || failed
254
255JEDIT_JAR="$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/jedit.jar"
256
257JEDIT_JARS=(
258  "$ISABELLE_JEDIT_BUILD_HOME/contrib/Code2HTML.jar"
259  "$ISABELLE_JEDIT_BUILD_HOME/contrib/CommonControls.jar"
260  "$ISABELLE_JEDIT_BUILD_HOME/contrib/Console.jar"
261  "$ISABELLE_JEDIT_BUILD_HOME/contrib/ErrorList.jar"
262  "$ISABELLE_JEDIT_BUILD_HOME/contrib/Highlight.jar"
263  "$ISABELLE_JEDIT_BUILD_HOME/contrib/kappalayout.jar"
264  "$ISABELLE_JEDIT_BUILD_HOME/contrib/MacOSX.jar"
265  "$ISABELLE_JEDIT_BUILD_HOME/contrib/Navigator.jar"
266  "$ISABELLE_JEDIT_BUILD_HOME/contrib/SideKick.jar"
267  "$ISABELLE_JEDIT_BUILD_HOME/contrib/idea-icons.jar"
268  "$ISABELLE_JEDIT_BUILD_HOME/contrib/jsr305-2.0.0.jar"
269)
270
271
272# target
273
274TARGET_BASE="dist/jars/Isabelle-jEdit-base.jar"
275TARGET="dist/jars/Isabelle-jEdit.jar"
276
277declare -a UPDATED=()
278
279if [ "$BUILD_JARS" = jars_fresh ]; then
280  OUTDATED=true
281else
282  OUTDATED=false
283  if [ ! -e "$TARGET_BASE" -a ! -e "$TARGET" ]; then
284    OUTDATED=true
285  else
286    if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
287      declare -a DEPS=(
288        "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR"
289        "${SOURCES_BASE[@]}" "${RESOURCES_BASE[@]}"
290        "${SOURCES[@]}" "${RESOURCES[@]}"
291      )
292    elif [ -e "$ISABELLE_HOME/Admin/build" ]; then
293      declare -a DEPS=(
294        "$PURE_JAR"
295        "${SOURCES_BASE[@]}" "${RESOURCES_BASE[@]}"
296        "${SOURCES[@]}" "${RESOURCES[@]}"
297      )
298    else
299      declare -a DEPS=()
300    fi
301    for DEP in "${DEPS[@]}"
302    do
303      [ ! -e "$DEP" ] && fail "Missing file: $DEP"
304      [ "$DEP" -nt "$TARGET_BASE" -o "$DEP" -nt "$TARGET" ] && {
305        OUTDATED=true
306        UPDATED["${#UPDATED[@]}"]="$DEP"
307      }
308    done
309  fi
310fi
311
312
313# build
314
315function init_resources ()
316{
317  mkdir -p dist/classes || failed
318  cp -p -R -f "$@" dist/classes/.
319}
320
321function compile_sources ()
322{
323  (
324    #FIXME workarounds for scalac 2.11.0
325    export CYGWIN="nodosfilewarning"
326    function stty() { :; }
327    export -f stty
328
329    for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR"
330    do
331      classpath "$JAR"
332    done
333    export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")"
334    isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS -d dist/classes "$@"
335  ) || fail "Failed to compile sources"
336}
337
338function make_jar ()
339{
340  cd dist/classes
341  isabelle_jdk jar cf "../../$1" * || failed
342  cd ../..
343  rm -rf dist/classes
344}
345
346if [ "$OUTDATED" = true ]
347then
348  echo "### Building Isabelle/jEdit ..."
349
350  [ "${#UPDATED[@]}" -gt 0 ] && {
351    echo "Changed files:"
352    for FILE in "${UPDATED[@]}"
353    do
354      echo "  $FILE"
355    done
356  }
357
358  [ -z "$ISABELLE_JEDIT_BUILD_HOME" ] && \
359    fail "Unknown ISABELLE_JEDIT_BUILD_HOME -- missing auxiliary component"
360
361  rm -rf dist || failed
362  mkdir -p dist || failed
363
364  cp -p -R -f "$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/." dist/.
365
366  init_resources "${RESOURCES_BASE[@]}"
367  compile_sources "${SOURCES_BASE[@]}"
368  make_jar "$TARGET_BASE"
369  classpath "$PWD/$TARGET_BASE"
370
371  init_resources "${RESOURCES[@]}"
372  cp src/jEdit.props dist/properties/.
373  cp -p -R -f src/modes/. dist/modes/.
374
375  perl -i -e 'while (<>) {
376    if (m/FILE="ml.xml"/ or m/FILE_NAME_GLOB="...sml,ml."/) { }
377    elsif (m/NAME="javacc"/) {
378      print qq!<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="{*.thy,ROOT0.ML,ROOT.ML}"/>\n\n!;
379      print qq!<MODE NAME="isabelle-ml" FILE="isabelle-ml.xml" FILE_NAME_GLOB="*.ML"/>\n\n!;
380      print qq!<MODE NAME="isabelle-news" FILE="isabelle-news.xml"/>\n\n!;
381      print qq!<MODE NAME="isabelle-options" FILE="isabelle-options.xml"/>\n\n!;
382      print qq!<MODE NAME="isabelle-root" FILE="isabelle-root.xml" FILE_NAME_GLOB="ROOT"/>\n\n!;
383      print;
384    }
385    elsif (m/NAME="sqr"/) {
386      print qq!<MODE NAME="sml" FILE="sml.xml" FILE_NAME_GLOB="*.{sml,sig}"/>\n\n!;
387      print;
388    }
389    else { print; }
390  }' dist/modes/catalog
391
392  cd dist
393  isabelle_jdk jar xf jedit.jar
394  cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" \
395    "org/gjt/sp/jedit/icons/themes/classic/32x32/apps/isabelle.gif" || failed
396  cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" \
397    "org/gjt/sp/jedit/icons/themes/tango/32x32/apps/isabelle.gif" || failed
398  isabelle_jdk jar cfe jedit.jar org.gjt.sp.jedit.jEdit org || failed
399  rm -rf META-INF org
400  cd ..
401
402  cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed
403  compile_sources "${SOURCES[@]}"
404  make_jar "$TARGET"
405
406  cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.5.0manual-a4.pdf" dist/doc/jedit-manual.pdf
407  cp dist/doc/CHANGES.txt dist/doc/jedit-changes
408  cat > dist/doc/Contents <<EOF
409Original jEdit Documentation
410  jedit-manual    jEdit 5.5 User's Guide
411  jedit-changes   jEdit 5.5 Version History
412
413EOF
414
415fi
416
417popd >/dev/null
418
419
420## main
421
422if [ "$BUILD_ONLY" = false ]
423then
424  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \
425    JEDIT_LOGIC_FOCUS JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_BUILD_MODE
426  export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
427  classpath "$JEDIT_HOME/dist/jedit.jar"
428  exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
429fi
430