author | wenzelm |
Sun, 18 Jul 2021 12:48:31 +0200 | |
changeset 74038 | b4f57bfe82e7 |
parent 74017 | b4e6b82fdb9e |
child 75291 | e4d6b9bd5071 |
permissions | -rwxr-xr-x |
34333 | 1 |
#!/usr/bin/env bash |
2 |
# |
|
34664 | 3 |
# Author: Makarius |
4 |
# |
|
5 |
# DESCRIPTION: Isabelle/jEdit interface wrapper |
|
6 |
||
34333 | 7 |
## diagnostics |
8 |
||
34664 | 9 |
PRG="$(basename "$0")" |
10 |
||
43284
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
11 |
function usage() |
34333 | 12 |
{ |
13 |
echo |
|
34664 | 14 |
echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]" |
34333 | 15 |
echo |
16 |
echo " Options are:" |
|
71548 | 17 |
echo " -A NAME ancestor session for option -R (default: parent)" |
62039 | 18 |
echo " -D NAME=X set JVM system property" |
66683 | 19 |
echo " -J OPTION add JVM runtime option" |
20 |
echo " (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)" |
|
68370 | 21 |
echo " -R NAME build image with requirements from other sessions" |
43285 | 22 |
echo " -b build only" |
48791 | 23 |
echo " -d DIR include session directory" |
43285 | 24 |
echo " -f fresh build" |
68541 | 25 |
echo " -i NAME include session in name-space of theories" |
34333 | 26 |
echo " -j OPTION add jEdit runtime option" |
66683 | 27 |
echo " (default $JEDIT_OPTIONS)" |
50403
87868964733c
more uniform default logic, using settings, options, args etc.;
wenzelm
parents:
50373
diff
changeset
|
28 |
echo " -l NAME logic session name" |
34333 | 29 |
echo " -m MODE add print mode for output" |
57086 | 30 |
echo " -n no build of session image on startup" |
63986
c7a4b03727ae
options for process policy, notably for multiprocessor machines;
wenzelm
parents:
63734
diff
changeset
|
31 |
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
|
32 |
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
|
33 |
echo " -u user build mode for session image (system_heaps=false)" |
34333 | 34 |
echo |
61171 | 35 |
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
|
36 |
echo " (default \"$USER_HOME/Scratch.thy\" or \":\" for empty buffer)." |
34333 | 37 |
echo |
38 |
exit 1 |
|
39 |
} |
|
40 |
||
43284
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
41 |
function fail() |
34333 | 42 |
{ |
43 |
echo "$1" >&2 |
|
44 |
exit 2 |
|
45 |
} |
|
46 |
||
43284
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
47 |
function failed() |
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
48 |
{ |
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
49 |
fail "Failed!" |
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
50 |
} |
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
51 |
|
34333 | 52 |
|
53 |
## process command line |
|
54 |
||
55 |
# options |
|
56 |
||
43285 | 57 |
BUILD_ONLY=false |
74038
b4f57bfe82e7
more robust "isabelle build_scala" as separate tool;
wenzelm
parents:
74017
diff
changeset
|
58 |
BUILD_OPTIONS="" |
63986
c7a4b03727ae
options for process policy, notably for multiprocessor machines;
wenzelm
parents:
63734
diff
changeset
|
59 |
ML_PROCESS_POLICY="" |
66988 | 60 |
JEDIT_LOGIC_ANCESTOR="" |
68370 | 61 |
JEDIT_LOGIC_REQUIREMENTS="" |
68541 | 62 |
JEDIT_INCLUDE_SESSIONS="" |
70382
23ba5a638e6d
more robust: avoid folding of jEdit file-names wrt. JEDIT_SESSION_DIRS;
wenzelm
parents:
70220
diff
changeset
|
63 |
JEDIT_SESSION_DIRS="-" |
50403
87868964733c
more uniform default logic, using settings, options, args etc.;
wenzelm
parents:
50373
diff
changeset
|
64 |
JEDIT_LOGIC="" |
34333 | 65 |
JEDIT_PRINT_MODE="" |
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69762
diff
changeset
|
66 |
JEDIT_NO_BUILD="" |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69762
diff
changeset
|
67 |
JEDIT_BUILD_MODE="default" |
34333 | 68 |
|
43284
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
69 |
function getoptions() |
34780 | 70 |
{ |
71 |
OPTIND=1 |
|
70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70382
diff
changeset
|
72 |
while getopts "A:BFD:J:R:bd:fi:j:l:m:np:su" OPT |
34780 | 73 |
do |
74 |
case "$OPT" in |
|
66988 | 75 |
A) |
76 |
JEDIT_LOGIC_ANCESTOR="$OPTARG" |
|
77 |
;; |
|
62039 | 78 |
D) |
79 |
JAVA_ARGS["${#JAVA_ARGS[@]}"]="-D$OPTARG" |
|
80 |
;; |
|
34780 | 81 |
J) |
82 |
JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG" |
|
83 |
;; |
|
64602 | 84 |
R) |
68370 | 85 |
JEDIT_LOGIC="$OPTARG" |
86 |
JEDIT_LOGIC_REQUIREMENTS="true" |
|
64602 | 87 |
;; |
43285 | 88 |
b) |
89 |
BUILD_ONLY=true |
|
90 |
;; |
|
48791 | 91 |
d) |
70382
23ba5a638e6d
more robust: avoid folding of jEdit file-names wrt. JEDIT_SESSION_DIRS;
wenzelm
parents:
70220
diff
changeset
|
92 |
JEDIT_SESSION_DIRS="$JEDIT_SESSION_DIRS:$OPTARG" |
48791 | 93 |
;; |
68541 | 94 |
i) |
95 |
if [ -z "$JEDIT_INCLUDE_SESSIONS" ]; then |
|
96 |
JEDIT_INCLUDE_SESSIONS="$OPTARG" |
|
97 |
else |
|
98 |
JEDIT_INCLUDE_SESSIONS="$JEDIT_INCLUDE_SESSIONS:$OPTARG" |
|
99 |
fi |
|
100 |
;; |
|
43285 | 101 |
f) |
74038
b4f57bfe82e7
more robust "isabelle build_scala" as separate tool;
wenzelm
parents:
74017
diff
changeset
|
102 |
BUILD_OPTIONS="-f" |
43285 | 103 |
;; |
34780 | 104 |
j) |
105 |
ARGS["${#ARGS[@]}"]="$OPTARG" |
|
106 |
;; |
|
107 |
l) |
|
108 |
JEDIT_LOGIC="$OPTARG" |
|
109 |
;; |
|
110 |
m) |
|
111 |
if [ -z "$JEDIT_PRINT_MODE" ]; then |
|
112 |
JEDIT_PRINT_MODE="$OPTARG" |
|
113 |
else |
|
114 |
JEDIT_PRINT_MODE="$JEDIT_PRINT_MODE,$OPTARG" |
|
115 |
fi |
|
116 |
;; |
|
50405
366c4a602500
clarified build_dialog: regular up-to-date check (extra cost of approx. 5s startup for HOL);
wenzelm
parents:
50403
diff
changeset
|
117 |
n) |
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69762
diff
changeset
|
118 |
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
|
119 |
;; |
63986
c7a4b03727ae
options for process policy, notably for multiprocessor machines;
wenzelm
parents:
63734
diff
changeset
|
120 |
p) |
c7a4b03727ae
options for process policy, notably for multiprocessor machines;
wenzelm
parents:
63734
diff
changeset
|
121 |
ML_PROCESS_POLICY="$OPTARG" |
c7a4b03727ae
options for process policy, notably for multiprocessor machines;
wenzelm
parents:
63734
diff
changeset
|
122 |
;; |
50373 | 123 |
s) |
53449 | 124 |
JEDIT_BUILD_MODE="system" |
50373 | 125 |
;; |
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69762
diff
changeset
|
126 |
u) |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69762
diff
changeset
|
127 |
JEDIT_BUILD_MODE="user" |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69762
diff
changeset
|
128 |
;; |
34780 | 129 |
\?) |
130 |
usage |
|
131 |
;; |
|
132 |
esac |
|
133 |
done |
|
134 |
} |
|
34581
abab3a577e10
slightly more robust treatment of options via arrays;
wenzelm
parents:
34412
diff
changeset
|
135 |
|
66906 | 136 |
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
|
137 |
|
53446
4adb2cce5fc6
use JEDIT_OPTIONS only once (in isabelle.Main.start_jedit);
wenzelm
parents:
53445
diff
changeset
|
138 |
declare -a ARGS=() |
34333 | 139 |
|
34780 | 140 |
declare -a OPTIONS; eval "OPTIONS=($ISABELLE_JEDIT_OPTIONS)" |
141 |
getoptions "${OPTIONS[@]}" |
|
142 |
||
143 |
getoptions "$@" |
|
34333 | 144 |
shift $(($OPTIND - 1)) |
145 |
||
146 |
||
147 |
# args |
|
148 |
||
61512
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61511
diff
changeset
|
149 |
while [ "$#" -gt 0 ]; do |
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61511
diff
changeset
|
150 |
ARGS["${#ARGS[@]}"]="$(platform_path "$1")" |
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61511
diff
changeset
|
151 |
shift |
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61511
diff
changeset
|
152 |
done |
34333 | 153 |
|
154 |
||
43284
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
155 |
## main |
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents:
41380
diff
changeset
|
156 |
|
74038
b4f57bfe82e7
more robust "isabelle build_scala" as separate tool;
wenzelm
parents:
74017
diff
changeset
|
157 |
isabelle scala_build $BUILD_OPTIONS || exit $? |
71368 | 158 |
|
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
|
159 |
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
|
160 |
then |
73161
31fbde3baa97
more systematic java-gui-setup, also for "isabelle jedit" command-line tool;
wenzelm
parents:
72248
diff
changeset
|
161 |
"$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
|
162 |
|
68370 | 163 |
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
|
164 |
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
|
165 |
export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY" |
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
|
166 |
exec isabelle java -splash:"$(platform_path "$ISABELLE_HOME/lib/logo/isabelle.gif")" \ |
73987
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73947
diff
changeset
|
167 |
"${JAVA_ARGS[@]}" isabelle.jedit.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
|
168 |
fi |