author | wenzelm |
Mon, 10 May 2021 22:18:12 +0200 | |
changeset 73660 | ff716ecb0805 |
parent 73653 | d9823224fcfe |
child 73661 | 8b3e672df28c |
permissions | -rwxr-xr-x |
34333 | 1 |
#!/usr/bin/env bash |
2 |
# |
|
34664 | 3 |
# Author: Makarius |
4 |
# |
|
5 |
# DESCRIPTION: Isabelle/jEdit interface wrapper |
|
6 |
||
43285 | 7 |
## sources |
8 |
||
71368 | 9 |
declare -a SOURCES0=( |
10 |
"src/Tools/jEdit/src-base/dockable.scala" |
|
11 |
"src/Tools/jEdit/src-base/isabelle_encoding.scala" |
|
12 |
"src/Tools/jEdit/src-base/jedit_lib.scala" |
|
13 |
"src/Tools/jEdit/src-base/pide_docking_framework.scala" |
|
14 |
"src/Tools/jEdit/src-base/plugin.scala" |
|
15 |
"src/Tools/jEdit/src-base/syntax_style.scala" |
|
66457
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents:
66120
diff
changeset
|
16 |
) |
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents:
66120
diff
changeset
|
17 |
|
71368 | 18 |
declare -a RESOURCES0=( |
19 |
"src/Tools/jEdit/src-base/Isabelle_Base.props" |
|
20 |
"src/Tools/jEdit/src-base/services.xml" |
|
66457
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents:
66120
diff
changeset
|
21 |
) |
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents:
66120
diff
changeset
|
22 |
|
43320 | 23 |
declare -a SOURCES=( |
71368 | 24 |
"src/Tools/jEdit/src/active.scala" |
25 |
"src/Tools/jEdit/src/completion_popup.scala" |
|
26 |
"src/Tools/jEdit/src/context_menu.scala" |
|
27 |
"src/Tools/jEdit/src/debugger_dockable.scala" |
|
28 |
"src/Tools/jEdit/src/document_model.scala" |
|
29 |
"src/Tools/jEdit/src/document_view.scala" |
|
30 |
"src/Tools/jEdit/src/documentation_dockable.scala" |
|
31 |
"src/Tools/jEdit/src/fold_handling.scala" |
|
32 |
"src/Tools/jEdit/src/font_info.scala" |
|
33 |
"src/Tools/jEdit/src/graphview_dockable.scala" |
|
34 |
"src/Tools/jEdit/src/info_dockable.scala" |
|
35 |
"src/Tools/jEdit/src/isabelle.scala" |
|
36 |
"src/Tools/jEdit/src/isabelle_encoding.scala" |
|
37 |
"src/Tools/jEdit/src/isabelle_export.scala" |
|
38 |
"src/Tools/jEdit/src/isabelle_options.scala" |
|
39 |
"src/Tools/jEdit/src/isabelle_session.scala" |
|
40 |
"src/Tools/jEdit/src/isabelle_sidekick.scala" |
|
41 |
"src/Tools/jEdit/src/isabelle_vfs.scala" |
|
42 |
"src/Tools/jEdit/src/jedit_bibtex.scala" |
|
43 |
"src/Tools/jEdit/src/jedit_editor.scala" |
|
44 |
"src/Tools/jEdit/src/jedit_lib.scala" |
|
45 |
"src/Tools/jEdit/src/jedit_options.scala" |
|
46 |
"src/Tools/jEdit/src/jedit_rendering.scala" |
|
47 |
"src/Tools/jEdit/src/jedit_resources.scala" |
|
48 |
"src/Tools/jEdit/src/jedit_sessions.scala" |
|
49 |
"src/Tools/jEdit/src/jedit_spell_checker.scala" |
|
50 |
"src/Tools/jEdit/src/keymap_merge.scala" |
|
51 |
"src/Tools/jEdit/src/monitor_dockable.scala" |
|
52 |
"src/Tools/jEdit/src/output_dockable.scala" |
|
53 |
"src/Tools/jEdit/src/plugin.scala" |
|
54 |
"src/Tools/jEdit/src/pretty_text_area.scala" |
|
55 |
"src/Tools/jEdit/src/pretty_tooltip.scala" |
|
56 |
"src/Tools/jEdit/src/process_indicator.scala" |
|
57 |
"src/Tools/jEdit/src/protocol_dockable.scala" |
|
58 |
"src/Tools/jEdit/src/query_dockable.scala" |
|
59 |
"src/Tools/jEdit/src/raw_output_dockable.scala" |
|
60 |
"src/Tools/jEdit/src/rich_text_area.scala" |
|
61 |
"src/Tools/jEdit/src/scala_console.scala" |
|
62 |
"src/Tools/jEdit/src/session_build.scala" |
|
63 |
"src/Tools/jEdit/src/simplifier_trace_dockable.scala" |
|
64 |
"src/Tools/jEdit/src/simplifier_trace_window.scala" |
|
65 |
"src/Tools/jEdit/src/sledgehammer_dockable.scala" |
|
66 |
"src/Tools/jEdit/src/state_dockable.scala" |
|
72248 | 67 |
"src/Tools/jEdit/src/status_widget.scala" |
71368 | 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" |
|
43285 | 76 |
) |
77 |
||
43320 | 78 |
declare -a RESOURCES=( |
71368 | 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/services.xml" |
|
43285 | 83 |
) |
84 |
||
85 |
||
34333 | 86 |
## diagnostics |
87 |
||
34664 | 88 |
PRG="$(basename "$0")" |
89 |
||
43284
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
90 |
function usage() |
34333 | 91 |
{ |
92 |
echo |
|
34664 | 93 |
echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]" |
34333 | 94 |
echo |
95 |
echo " Options are:" |
|
71548 | 96 |
echo " -A NAME ancestor session for option -R (default: parent)" |
62039 | 97 |
echo " -D NAME=X set JVM system property" |
66683 | 98 |
echo " -J OPTION add JVM runtime option" |
99 |
echo " (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)" |
|
68370 | 100 |
echo " -R NAME build image with requirements from other sessions" |
43285 | 101 |
echo " -b build only" |
48791 | 102 |
echo " -d DIR include session directory" |
43285 | 103 |
echo " -f fresh build" |
68541 | 104 |
echo " -i NAME include session in name-space of theories" |
34333 | 105 |
echo " -j OPTION add jEdit runtime option" |
66683 | 106 |
echo " (default $JEDIT_OPTIONS)" |
50403
87868964733c
more uniform default logic, using settings, options, args etc.;
wenzelm
parents:
50373
diff
changeset
|
107 |
echo " -l NAME logic session name" |
34333 | 108 |
echo " -m MODE add print mode for output" |
57086 | 109 |
echo " -n no build of session image on startup" |
63986
c7a4b03727ae
options for process policy, notably for multiprocessor machines;
wenzelm
parents:
63734
diff
changeset
|
110 |
echo " -p CMD ML process command prefix (process policy)" |
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69762
diff
changeset
|
111 |
echo " -s system build mode for session image (system_heaps=true)" |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69762
diff
changeset
|
112 |
echo " -u user build mode for session image (system_heaps=false)" |
34333 | 113 |
echo |
61171 | 114 |
echo " Start jEdit with Isabelle plugin setup and open FILES" |
61512
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61511
diff
changeset
|
115 |
echo " (default \"$USER_HOME/Scratch.thy\" or \":\" for empty buffer)." |
34333 | 116 |
echo |
117 |
exit 1 |
|
118 |
} |
|
119 |
||
43284
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
120 |
function fail() |
34333 | 121 |
{ |
122 |
echo "$1" >&2 |
|
123 |
exit 2 |
|
124 |
} |
|
125 |
||
43284
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
126 |
function failed() |
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
127 |
{ |
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
128 |
fail "Failed!" |
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
129 |
} |
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
130 |
|
34333 | 131 |
|
132 |
## process command line |
|
133 |
||
134 |
# options |
|
135 |
||
43285 | 136 |
BUILD_ONLY=false |
71372
85274743f789
clarified option -f: avoid accidental target_clean for proper release snapshot;
wenzelm
parents:
71371
diff
changeset
|
137 |
FRESH_BUILD="" |
63986
c7a4b03727ae
options for process policy, notably for multiprocessor machines;
wenzelm
parents:
63734
diff
changeset
|
138 |
ML_PROCESS_POLICY="" |
66988 | 139 |
JEDIT_LOGIC_ANCESTOR="" |
68370 | 140 |
JEDIT_LOGIC_REQUIREMENTS="" |
68541 | 141 |
JEDIT_INCLUDE_SESSIONS="" |
70382
23ba5a638e6d
more robust: avoid folding of jEdit file-names wrt. JEDIT_SESSION_DIRS;
wenzelm
parents:
70220
diff
changeset
|
142 |
JEDIT_SESSION_DIRS="-" |
50403
87868964733c
more uniform default logic, using settings, options, args etc.;
wenzelm
parents:
50373
diff
changeset
|
143 |
JEDIT_LOGIC="" |
34333 | 144 |
JEDIT_PRINT_MODE="" |
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69762
diff
changeset
|
145 |
JEDIT_NO_BUILD="" |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69762
diff
changeset
|
146 |
JEDIT_BUILD_MODE="default" |
34333 | 147 |
|
43284
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
148 |
function getoptions() |
34780 | 149 |
{ |
150 |
OPTIND=1 |
|
70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70382
diff
changeset
|
151 |
while getopts "A:BFD:J:R:bd:fi:j:l:m:np:su" OPT |
34780 | 152 |
do |
153 |
case "$OPT" in |
|
66988 | 154 |
A) |
155 |
JEDIT_LOGIC_ANCESTOR="$OPTARG" |
|
156 |
;; |
|
62039 | 157 |
D) |
158 |
JAVA_ARGS["${#JAVA_ARGS[@]}"]="-D$OPTARG" |
|
159 |
;; |
|
34780 | 160 |
J) |
161 |
JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG" |
|
162 |
;; |
|
64602 | 163 |
R) |
68370 | 164 |
JEDIT_LOGIC="$OPTARG" |
165 |
JEDIT_LOGIC_REQUIREMENTS="true" |
|
64602 | 166 |
;; |
43285 | 167 |
b) |
168 |
BUILD_ONLY=true |
|
169 |
;; |
|
48791 | 170 |
d) |
70382
23ba5a638e6d
more robust: avoid folding of jEdit file-names wrt. JEDIT_SESSION_DIRS;
wenzelm
parents:
70220
diff
changeset
|
171 |
JEDIT_SESSION_DIRS="$JEDIT_SESSION_DIRS:$OPTARG" |
48791 | 172 |
;; |
68541 | 173 |
i) |
174 |
if [ -z "$JEDIT_INCLUDE_SESSIONS" ]; then |
|
175 |
JEDIT_INCLUDE_SESSIONS="$OPTARG" |
|
176 |
else |
|
177 |
JEDIT_INCLUDE_SESSIONS="$JEDIT_INCLUDE_SESSIONS:$OPTARG" |
|
178 |
fi |
|
179 |
;; |
|
43285 | 180 |
f) |
71372
85274743f789
clarified option -f: avoid accidental target_clean for proper release snapshot;
wenzelm
parents:
71371
diff
changeset
|
181 |
FRESH_BUILD="true" |
43285 | 182 |
;; |
34780 | 183 |
j) |
184 |
ARGS["${#ARGS[@]}"]="$OPTARG" |
|
185 |
;; |
|
186 |
l) |
|
187 |
JEDIT_LOGIC="$OPTARG" |
|
188 |
;; |
|
189 |
m) |
|
190 |
if [ -z "$JEDIT_PRINT_MODE" ]; then |
|
191 |
JEDIT_PRINT_MODE="$OPTARG" |
|
192 |
else |
|
193 |
JEDIT_PRINT_MODE="$JEDIT_PRINT_MODE,$OPTARG" |
|
194 |
fi |
|
195 |
;; |
|
50405
366c4a602500
clarified build_dialog: regular up-to-date check (extra cost of approx. 5s startup for HOL);
wenzelm
parents:
50403
diff
changeset
|
196 |
n) |
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69762
diff
changeset
|
197 |
JEDIT_NO_BUILD="true" |
50405
366c4a602500
clarified build_dialog: regular up-to-date check (extra cost of approx. 5s startup for HOL);
wenzelm
parents:
50403
diff
changeset
|
198 |
;; |
63986
c7a4b03727ae
options for process policy, notably for multiprocessor machines;
wenzelm
parents:
63734
diff
changeset
|
199 |
p) |
c7a4b03727ae
options for process policy, notably for multiprocessor machines;
wenzelm
parents:
63734
diff
changeset
|
200 |
ML_PROCESS_POLICY="$OPTARG" |
c7a4b03727ae
options for process policy, notably for multiprocessor machines;
wenzelm
parents:
63734
diff
changeset
|
201 |
;; |
50373 | 202 |
s) |
53449 | 203 |
JEDIT_BUILD_MODE="system" |
50373 | 204 |
;; |
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69762
diff
changeset
|
205 |
u) |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69762
diff
changeset
|
206 |
JEDIT_BUILD_MODE="user" |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69762
diff
changeset
|
207 |
;; |
34780 | 208 |
\?) |
209 |
usage |
|
210 |
;; |
|
211 |
esac |
|
212 |
done |
|
213 |
} |
|
34581
abab3a577e10
slightly more robust treatment of options via arrays;
wenzelm
parents:
34412
diff
changeset
|
214 |
|
66906 | 215 |
eval "declare -a JAVA_ARGS=($JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)" |
34843
eb8806a2e348
define scala.home, for more robust startup of Scala tools, notably the compiler;
wenzelm
parents:
34790
diff
changeset
|
216 |
|
53446
4adb2cce5fc6
use JEDIT_OPTIONS only once (in isabelle.Main.start_jedit);
wenzelm
parents:
53445
diff
changeset
|
217 |
declare -a ARGS=() |
34333 | 218 |
|
34780 | 219 |
declare -a OPTIONS; eval "OPTIONS=($ISABELLE_JEDIT_OPTIONS)" |
220 |
getoptions "${OPTIONS[@]}" |
|
221 |
||
222 |
getoptions "$@" |
|
34333 | 223 |
shift $(($OPTIND - 1)) |
224 |
||
225 |
||
226 |
# args |
|
227 |
||
61512
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61511
diff
changeset
|
228 |
while [ "$#" -gt 0 ]; do |
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61511
diff
changeset
|
229 |
ARGS["${#ARGS[@]}"]="$(platform_path "$1")" |
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61511
diff
changeset
|
230 |
shift |
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61511
diff
changeset
|
231 |
done |
34333 | 232 |
|
233 |
||
43284
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
234 |
## dependencies |
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
235 |
|
49953 | 236 |
if [ -e "$ISABELLE_HOME/Admin/build" ]; then |
62589
b5783412bfed
prefer plain "isabelle" from PATH within Isabelle settings environment;
wenzelm
parents:
62039
diff
changeset
|
237 |
isabelle browser -b || exit $? |
71372
85274743f789
clarified option -f: avoid accidental target_clean for proper release snapshot;
wenzelm
parents:
71371
diff
changeset
|
238 |
if [ -n "$FRESH_BUILD" ]; then |
85274743f789
clarified option -f: avoid accidental target_clean for proper release snapshot;
wenzelm
parents:
71371
diff
changeset
|
239 |
"$ISABELLE_HOME/Admin/build" jars_fresh || exit $? |
85274743f789
clarified option -f: avoid accidental target_clean for proper release snapshot;
wenzelm
parents:
71371
diff
changeset
|
240 |
else |
85274743f789
clarified option -f: avoid accidental target_clean for proper release snapshot;
wenzelm
parents:
71371
diff
changeset
|
241 |
"$ISABELLE_HOME/Admin/build" jars || exit $? |
85274743f789
clarified option -f: avoid accidental target_clean for proper release snapshot;
wenzelm
parents:
71371
diff
changeset
|
242 |
fi |
85274743f789
clarified option -f: avoid accidental target_clean for proper release snapshot;
wenzelm
parents:
71371
diff
changeset
|
243 |
elif [ -n "$FRESH_BUILD" ]; then |
85274743f789
clarified option -f: avoid accidental target_clean for proper release snapshot;
wenzelm
parents:
71371
diff
changeset
|
244 |
echo >&2 "### Ignoring fresh build option: not a repository clone" |
85274743f789
clarified option -f: avoid accidental target_clean for proper release snapshot;
wenzelm
parents:
71371
diff
changeset
|
245 |
FRESH_BUILD="" |
49953 | 246 |
fi |
43413 | 247 |
|
43284
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
248 |
|
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
249 |
# target |
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
250 |
|
71368 | 251 |
pushd "$ISABELLE_HOME" >/dev/null || failed |
43284
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
252 |
|
71368 | 253 |
TARGET_DIR="src/Tools/jEdit/dist" |
254 |
TARGET_JAR0="$TARGET_DIR/jars/Isabelle-jEdit-base.jar" |
|
255 |
TARGET_JAR="$TARGET_DIR/jars/Isabelle-jEdit.jar" |
|
256 |
TARGET_SHASUM="$TARGET_DIR/Isabelle-jEdit.shasum" |
|
257 |
||
258 |
declare -a TARGET_DEPS=("lib/classes/Pure.jar" "$TARGET_DIR/jedit.jar") |
|
73653
d9823224fcfe
build auxiliary jEdit component in Isabelle/Scala;
wenzelm
parents:
73652
diff
changeset
|
259 |
for DEP in "$TARGET_DIR"/jars/*.jar |
71368 | 260 |
do |
73653
d9823224fcfe
build auxiliary jEdit component in Isabelle/Scala;
wenzelm
parents:
73652
diff
changeset
|
261 |
TARGET_DEPS["${#TARGET_DEPS[@]}"]="$DEP" |
71368 | 262 |
done |
43384 | 263 |
|
71368 | 264 |
function target_shasum() |
265 |
( |
|
266 |
shasum -a1 -b "$TARGET_JAR0" "$TARGET_JAR" "${TARGET_DEPS[@]}" \ |
|
267 |
"${SOURCES0[@]}" "${RESOURCES0[@]}" "${SOURCES[@]}" "${RESOURCES[@]}" 2>/dev/null |
|
268 |
) |
|
269 |
||
270 |
function target_clean() |
|
271 |
{ |
|
272 |
rm -rf "$ISABELLE_HOME/$TARGET_DIR" |
|
273 |
} |
|
274 |
||
71372
85274743f789
clarified option -f: avoid accidental target_clean for proper release snapshot;
wenzelm
parents:
71371
diff
changeset
|
275 |
[ -n "$FRESH_BUILD" ] && target_clean |
43284
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
276 |
|
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
277 |
|
71368 | 278 |
## build |
279 |
||
280 |
BUILD_DIR="$TARGET_DIR/build" |
|
43284
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
281 |
|
66457
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents:
66120
diff
changeset
|
282 |
function init_resources () |
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents:
66120
diff
changeset
|
283 |
{ |
71368 | 284 |
mkdir -p "$BUILD_DIR" || failed |
285 |
cp -p -R "$@" "$BUILD_DIR/." |
|
66457
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents:
66120
diff
changeset
|
286 |
} |
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents:
66120
diff
changeset
|
287 |
|
71368 | 288 |
function compile_sources() |
66457
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents:
66120
diff
changeset
|
289 |
{ |
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents:
66120
diff
changeset
|
290 |
( |
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents:
66120
diff
changeset
|
291 |
#FIXME workarounds for scalac 2.11.0 |
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents:
66120
diff
changeset
|
292 |
export CYGWIN="nodosfilewarning" |
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents:
66120
diff
changeset
|
293 |
function stty() { :; } |
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents:
66120
diff
changeset
|
294 |
export -f stty |
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents:
66120
diff
changeset
|
295 |
|
71368 | 296 |
for DEP in "${TARGET_DEPS[@]}" |
66457
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents:
66120
diff
changeset
|
297 |
do |
71368 | 298 |
classpath "$DEP" |
66457
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents:
66120
diff
changeset
|
299 |
done |
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents:
66120
diff
changeset
|
300 |
export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")" |
71368 | 301 |
isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS -d "$BUILD_DIR" "$@" |
66457
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents:
66120
diff
changeset
|
302 |
) || fail "Failed to compile sources" |
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents:
66120
diff
changeset
|
303 |
} |
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents:
66120
diff
changeset
|
304 |
|
71368 | 305 |
function make_jar() |
66457
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents:
66120
diff
changeset
|
306 |
{ |
71368 | 307 |
isabelle_jdk jar -c -f "$1" -C "$BUILD_DIR" . || failed |
308 |
rm -rf "$ISABELLE_HOME/$BUILD_DIR" |
|
66457
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents:
66120
diff
changeset
|
309 |
} |
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents:
66120
diff
changeset
|
310 |
|
71375 | 311 |
target_shasum | cmp "$TARGET_SHASUM" >/dev/null 2>/dev/null |
71371 | 312 |
if [ -e "$ISABELLE_HOME/Admin/build" -a "$?" -ne 0 ]; then |
43405 | 313 |
echo "### Building Isabelle/jEdit ..." |
314 |
||
43284
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
315 |
[ -z "$ISABELLE_JEDIT_BUILD_HOME" ] && \ |
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
316 |
fail "Unknown ISABELLE_JEDIT_BUILD_HOME -- missing auxiliary component" |
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
317 |
|
71368 | 318 |
target_clean || failed |
319 |
mkdir -p "$TARGET_DIR" || failed |
|
43287 | 320 |
|
73653
d9823224fcfe
build auxiliary jEdit component in Isabelle/Scala;
wenzelm
parents:
73652
diff
changeset
|
321 |
cp -p -R "$ISABELLE_JEDIT_BUILD_HOME/$ISABELLE_JEDIT_BUILD_VERSION/." "$TARGET_DIR/." |
71368 | 322 |
|
323 |
init_resources "${RESOURCES0[@]}" |
|
324 |
compile_sources "${SOURCES0[@]}" |
|
325 |
make_jar "$TARGET_JAR0" |
|
326 |
classpath "$TARGET_JAR0" |
|
66457
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents:
66120
diff
changeset
|
327 |
|
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents:
66120
diff
changeset
|
328 |
init_resources "${RESOURCES[@]}" |
9098c36abd1a
separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents:
66120
diff
changeset
|
329 |
compile_sources "${SOURCES[@]}" |
71368 | 330 |
make_jar "$TARGET_JAR" |
56422 | 331 |
|
71368 | 332 |
target_shasum > "$TARGET_SHASUM" |
43284
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
333 |
fi |
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
334 |
|
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
335 |
|
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
336 |
## main |
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
337 |
|
71368 | 338 |
popd >/dev/null |
339 |
||
53576
793a429c63e7
maintain classpath in more elementary manner: turn ISABELLE_CLASSPATH into -classpath option, so that all jars are covered by sun.misc.Launcher.AppClassLoader (e.g. relevant for loading add-on resources);
wenzelm
parents:
53451
diff
changeset
|
340 |
if [ "$BUILD_ONLY" = false ] |
793a429c63e7
maintain classpath in more elementary manner: turn ISABELLE_CLASSPATH into -classpath option, so that all jars are covered by sun.misc.Launcher.AppClassLoader (e.g. relevant for loading add-on resources);
wenzelm
parents:
53451
diff
changeset
|
341 |
then |
73161
31fbde3baa97
more systematic java-gui-setup, also for "isabelle jedit" command-line tool;
wenzelm
parents:
72248
diff
changeset
|
342 |
"$ISABELLE_HOME/lib/scripts/java-gui-setup" |
31fbde3baa97
more systematic java-gui-setup, also for "isabelle jedit" command-line tool;
wenzelm
parents:
72248
diff
changeset
|
343 |
|
68370 | 344 |
export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \ |
70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70382
diff
changeset
|
345 |
JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_NO_BUILD JEDIT_BUILD_MODE |
63986
c7a4b03727ae
options for process policy, notably for multiprocessor machines;
wenzelm
parents:
63734
diff
changeset
|
346 |
export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY" |
53576
793a429c63e7
maintain classpath in more elementary manner: turn ISABELLE_CLASSPATH into -classpath option, so that all jars are covered by sun.misc.Launcher.AppClassLoader (e.g. relevant for loading add-on resources);
wenzelm
parents:
53451
diff
changeset
|
347 |
classpath "$JEDIT_HOME/dist/jedit.jar" |
70220
089753519be0
more uniform Isabelle splash screen -- avoid problems with jEdit splash and Java 11 on some Linux window managers;
wenzelm
parents:
69854
diff
changeset
|
348 |
exec isabelle java -splash:"$(platform_path "$ISABELLE_HOME/lib/logo/isabelle.gif")" \ |
089753519be0
more uniform Isabelle splash screen -- avoid problems with jEdit splash and Java 11 on some Linux window managers;
wenzelm
parents:
69854
diff
changeset
|
349 |
"${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}" |
50416
2e1b47e22fc6
more rigorous "build only" mode: avoid build dialog of logic image and its potential need for GUI display;
wenzelm
parents:
50405
diff
changeset
|
350 |
fi |