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