| author | nipkow | 
| Mon, 26 Aug 2024 18:26:06 +0200 | |
| changeset 80775 | de95c82eb31a | 
| parent 77483 | 291f5848bf55 | 
| child 82321 | 0811cfce1f5b | 
| 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"  | 
| 77483 | 31  | 
echo " -p CMD command prefix for ML process (e.g. NUMA 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=""  | 
| 77483 | 59  | 
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"  | 
|
| 75296 | 109  | 
JEDIT_LOGIC_REQUIREMENTS="false"  | 
| 34780 | 110  | 
;;  | 
111  | 
m)  | 
|
112  | 
if [ -z "$JEDIT_PRINT_MODE" ]; then  | 
|
113  | 
JEDIT_PRINT_MODE="$OPTARG"  | 
|
114  | 
else  | 
|
115  | 
JEDIT_PRINT_MODE="$JEDIT_PRINT_MODE,$OPTARG"  | 
|
116  | 
fi  | 
|
117  | 
;;  | 
|
| 
50405
 
366c4a602500
clarified build_dialog: regular up-to-date check (extra cost of approx. 5s startup for HOL);
 
wenzelm 
parents: 
50403 
diff
changeset
 | 
118  | 
n)  | 
| 
69854
 
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
 
wenzelm 
parents: 
69762 
diff
changeset
 | 
119  | 
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
 | 
120  | 
;;  | 
| 
63986
 
c7a4b03727ae
options for process policy, notably for multiprocessor machines;
 
wenzelm 
parents: 
63734 
diff
changeset
 | 
121  | 
p)  | 
| 77483 | 122  | 
PROCESS_POLICY="$OPTARG"  | 
| 
63986
 
c7a4b03727ae
options for process policy, notably for multiprocessor machines;
 
wenzelm 
parents: 
63734 
diff
changeset
 | 
123  | 
;;  | 
| 50373 | 124  | 
s)  | 
| 53449 | 125  | 
JEDIT_BUILD_MODE="system"  | 
| 50373 | 126  | 
;;  | 
| 
69854
 
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
 
wenzelm 
parents: 
69762 
diff
changeset
 | 
127  | 
u)  | 
| 
 
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
 
wenzelm 
parents: 
69762 
diff
changeset
 | 
128  | 
JEDIT_BUILD_MODE="user"  | 
| 
 
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
 
wenzelm 
parents: 
69762 
diff
changeset
 | 
129  | 
;;  | 
| 34780 | 130  | 
\?)  | 
131  | 
usage  | 
|
132  | 
;;  | 
|
133  | 
esac  | 
|
134  | 
done  | 
|
135  | 
}  | 
|
| 
34581
 
abab3a577e10
slightly more robust treatment of options via arrays;
 
wenzelm 
parents: 
34412 
diff
changeset
 | 
136  | 
|
| 66906 | 137  | 
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
 | 
138  | 
|
| 
53446
 
4adb2cce5fc6
use JEDIT_OPTIONS only once (in isabelle.Main.start_jedit);
 
wenzelm 
parents: 
53445 
diff
changeset
 | 
139  | 
declare -a ARGS=()  | 
| 34333 | 140  | 
|
| 34780 | 141  | 
declare -a OPTIONS; eval "OPTIONS=($ISABELLE_JEDIT_OPTIONS)"  | 
142  | 
getoptions "${OPTIONS[@]}"
 | 
|
143  | 
||
144  | 
getoptions "$@"  | 
|
| 34333 | 145  | 
shift $(($OPTIND - 1))  | 
146  | 
||
147  | 
||
148  | 
# args  | 
|
149  | 
||
| 
61512
 
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
 
wenzelm 
parents: 
61511 
diff
changeset
 | 
150  | 
while [ "$#" -gt 0 ]; do  | 
| 
 
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
 
wenzelm 
parents: 
61511 
diff
changeset
 | 
151  | 
  ARGS["${#ARGS[@]}"]="$(platform_path "$1")"
 | 
| 
 
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
 
wenzelm 
parents: 
61511 
diff
changeset
 | 
152  | 
shift  | 
| 
 
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
 
wenzelm 
parents: 
61511 
diff
changeset
 | 
153  | 
done  | 
| 34333 | 154  | 
|
155  | 
||
| 
43284
 
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
 
wenzelm 
parents: 
41380 
diff
changeset
 | 
156  | 
## main  | 
| 
 
04d473e883df
build jedit as part of regular startup script (in that case depending on jedit_build component);
 
wenzelm 
parents: 
41380 
diff
changeset
 | 
157  | 
|
| 
74038
 
b4f57bfe82e7
more robust "isabelle build_scala" as separate tool;
 
wenzelm 
parents: 
74017 
diff
changeset
 | 
158  | 
isabelle scala_build $BUILD_OPTIONS || exit $?  | 
| 71368 | 159  | 
|
| 
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
 | 
160  | 
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
 | 
161  | 
then  | 
| 
73161
 
31fbde3baa97
more systematic java-gui-setup, also for "isabelle jedit" command-line tool;
 
wenzelm 
parents: 
72248 
diff
changeset
 | 
162  | 
"$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
 | 
163  | 
|
| 68370 | 164  | 
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
 | 
165  | 
JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_NO_BUILD JEDIT_BUILD_MODE  | 
| 77483 | 166  | 
export JEDIT_PROCESS_POLICY="$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
 | 
167  | 
exec isabelle java -splash:"$(platform_path "$ISABELLE_HOME/lib/logo/isabelle.gif")" \  | 
| 75291 | 168  | 
    "${JAVA_ARGS[@]}" isabelle.jedit.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
 | 
169  | 
fi  |