2 # |
2 # |
3 # Author: Makarius |
3 # Author: Makarius |
4 # |
4 # |
5 # DESCRIPTION: run Isabelle process with raw ML console and line editor |
5 # DESCRIPTION: run Isabelle process with raw ML console and line editor |
6 |
6 |
7 ## settings |
7 isabelle_admin_build jars || exit $? |
8 |
8 |
9 case "$ISABELLE_JAVA_PLATFORM" in |
9 case "$ISABELLE_JAVA_PLATFORM" in |
10 x86-*) |
10 x86-*) |
11 ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS32" |
11 ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS32" |
12 ;; |
12 ;; |
13 x86_64-*) |
13 x86_64-*) |
14 ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS64" |
14 ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS64" |
15 ;; |
15 ;; |
16 esac |
16 esac |
17 |
17 |
18 |
|
19 ## diagnostics |
|
20 |
|
21 PRG="$(basename "$0")" |
|
22 |
|
23 function usage() |
|
24 { |
|
25 echo |
|
26 echo "Usage: isabelle $PRG [OPTIONS]" |
|
27 echo |
|
28 echo " Options are:" |
|
29 echo " -d DIR include session directory" |
|
30 echo " -l NAME logic session name (default ISABELLE_LOGIC=\"$ISABELLE_LOGIC\")" |
|
31 echo " -m MODE add print mode for output" |
|
32 echo " -n no build of session image on startup" |
|
33 echo " -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)" |
|
34 echo " -r logic session is RAW_ML_SYSTEM" |
|
35 echo " -s system build mode for session image" |
|
36 echo |
|
37 echo " Run Isabelle process with raw ML console and line editor" |
|
38 echo " (ISABELLE_LINE_EDITOR=\"$ISABELLE_LINE_EDITOR\")." |
|
39 echo |
|
40 exit 1 |
|
41 } |
|
42 |
|
43 |
|
44 ## process command line |
|
45 |
|
46 # options |
|
47 |
|
48 declare -a ISABELLE_OPTIONS=() |
|
49 |
|
50 declare -a INCLUDE_DIRS=() |
|
51 LOGIC="$ISABELLE_LOGIC" |
|
52 NO_BUILD="false" |
|
53 declare -a SYSTEM_OPTIONS=() |
|
54 SYSTEM_MODE="false" |
|
55 |
|
56 while getopts "d:l:m:no:rs" OPT |
|
57 do |
|
58 case "$OPT" in |
|
59 d) |
|
60 INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG" |
|
61 ;; |
|
62 l) |
|
63 LOGIC="$OPTARG" |
|
64 ;; |
|
65 m) |
|
66 ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-m" |
|
67 ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTARG" |
|
68 ;; |
|
69 n) |
|
70 NO_BUILD="true" |
|
71 ;; |
|
72 o) |
|
73 SYSTEM_OPTIONS["${#SYSTEM_OPTIONS[@]}"]="$OPTARG" |
|
74 ;; |
|
75 r) |
|
76 LOGIC="RAW_ML_SYSTEM" |
|
77 ;; |
|
78 s) |
|
79 SYSTEM_MODE="true" |
|
80 ;; |
|
81 \?) |
|
82 usage |
|
83 ;; |
|
84 esac |
|
85 done |
|
86 |
|
87 shift $(($OPTIND - 1)) |
|
88 |
|
89 |
|
90 # args |
|
91 |
|
92 [ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; } |
|
93 |
|
94 |
|
95 ## main |
|
96 |
|
97 isabelle_admin_build jars || exit $? |
|
98 |
|
99 declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)" |
18 declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)" |
100 |
19 |
101 mkdir -p "$ISABELLE_TMP_PREFIX" || exit $? |
20 mkdir -p "$ISABELLE_TMP_PREFIX" || exit $? |
102 OPTIONS_FILE="$ISABELLE_TMP_PREFIX/options$$" |
|
103 |
21 |
104 if [ "$LOGIC" = "RAW_ML_SYSTEM" ]; then |
22 "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@" |
105 "$ISABELLE_TOOL" options -x "$OPTIONS_FILE" |
|
106 else |
|
107 "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build_Console \ |
|
108 "$LOGIC" "$NO_BUILD" "$SYSTEM_MODE" "$OPTIONS_FILE" \ |
|
109 "${INCLUDE_DIRS[@]}" $'\n' "${SYSTEM_OPTIONS[@]}" || { |
|
110 rm -f "$OPTIONS_FILE" |
|
111 exit "$?" |
|
112 } |
|
113 ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-m" |
|
114 ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="ASCII" |
|
115 fi |
|
116 |
|
117 ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-O" |
|
118 ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTIONS_FILE" |
|
119 |
|
120 if type -p "$ISABELLE_LINE_EDITOR" > /dev/null |
|
121 then |
|
122 exec "$ISABELLE_LINE_EDITOR" "$ISABELLE_PROCESS" "${ISABELLE_OPTIONS[@]}" -- "$LOGIC" |
|
123 else |
|
124 echo "### No line editor: \"$ISABELLE_LINE_EDITOR\"" |
|
125 exec "$ISABELLE_PROCESS" "${ISABELLE_OPTIONS[@]}" -- "$LOGIC" |
|
126 fi |
|