author | wenzelm |
Wed, 14 May 2008 11:05:10 +0200 | |
changeset 26882 | 9e824d8f4512 |
parent 17820 | 9822a7755ad4 |
permissions | -rwxr-xr-x |
17759 | 1 |
#!/usr/bin/env bash |
2 |
# |
|
3 |
# $Id$ |
|
4 |
# Author: Makarius |
|
5 |
# |
|
6 |
# Poplog/PML startup script (version 15.6/2.1). |
|
7 |
||
8 |
export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE |
|
9 |
||
10 |
||
11 |
## diagnostics |
|
12 |
||
13 |
function fail_out() |
|
14 |
{ |
|
15 |
echo "Unable to create output heap file: \"$OUTFILE\"" >&2 |
|
16 |
exit 2 |
|
17 |
} |
|
18 |
||
19 |
function check_mlhome_file() |
|
20 |
{ |
|
21 |
if [ ! -f "$1" ]; then |
|
22 |
echo "Unable to locate $1" >&2 |
|
23 |
echo "Please check your ML_HOME setting!" >&2 |
|
24 |
exit 2 |
|
25 |
fi |
|
26 |
} |
|
27 |
||
28 |
function check_heap_file() |
|
29 |
{ |
|
30 |
if [ ! -f "$1" ]; then |
|
31 |
echo "Expected to find ML heap file $1" >&2 |
|
32 |
return 1 |
|
33 |
else |
|
34 |
return 0 |
|
35 |
fi |
|
36 |
} |
|
37 |
||
38 |
||
39 |
## prepare databases |
|
40 |
||
41 |
if [ -z "$INFILE" ]; then |
|
42 |
EXIT="fun exit (i: int) = OS.execve \"/bin/sh\" [\"sh\", \"-c\", \"exit \" ^ makestring i] (OS.envlist());" |
|
17794 | 43 |
USE='pop11 |
44 |
section $-ml; |
|
45 |
||
46 |
ml_exception Use of string; |
|
47 |
||
48 |
ml_val use : string -> unit = |
|
49 |
procedure(name) with_props use; |
|
50 |
lvars name, path; |
|
51 |
lconstant UseExn = exception("Use"); |
|
52 |
||
53 |
define dlocal pop_exception_handler(n, msg, idstring, severity); |
|
54 |
returnunless(severity == `E` or severity == `R`)(false); |
|
55 |
erasenum(n); |
|
56 |
raise(UseExn(name)); |
|
57 |
enddefine; |
|
58 |
||
59 |
unless sourcefile(name) ->> path then raise(UseExn(name)) endunless; |
|
60 |
ml_load(path); |
|
61 |
ml_unit; |
|
62 |
endprocedure; |
|
63 |
||
64 |
ml_val use_string : string -> unit = |
|
65 |
procedure(str) with_props use_string; |
|
66 |
lvars str; |
|
67 |
lconstant UseExn = exception("Use"); |
|
68 |
||
69 |
define dlocal pop_exception_handler(n, msg, idstring, severity); |
|
17820 | 70 |
[n ^n msg ^msg idstring ^idstring severity ^severity] ==> |
17794 | 71 |
returnunless(severity == `E` or severity == `R`)(false); |
72 |
erasenum(n); |
|
73 |
raise(UseExn(str)); |
|
74 |
enddefine; |
|
75 |
||
76 |
ml_compile(stringin(str)); |
|
77 |
ml_unit; |
|
78 |
endprocedure; |
|
79 |
||
80 |
endsection; |
|
81 |
ml' |
|
17759 | 82 |
DB="" |
83 |
else |
|
84 |
EXIT="" |
|
17794 | 85 |
USE="" |
17759 | 86 |
DB="+$INFILE" |
87 |
fi |
|
88 |
||
89 |
if [ -z "$OUTFILE" ]; then |
|
90 |
COMMIT='fun commit () = (StdIO.output (StdIO.std_err, "Error - Database is not opened for writing.\n"); false);' |
|
91 |
else |
|
17805 | 92 |
ML_OPTIONS="$ML_OPTIONS -nort" |
17759 | 93 |
if [ -z "$NOWRITE" ]; then |
94 |
COMMIT="fun commit () = if System.make {image =\"$OUTFILE\", lock = false, share = false, banner = false, init = false} then System.restart() else true;" |
|
95 |
else |
|
96 |
COMMIT="fun commit () = if System.make {image =\"$OUTFILE\", lock = true, share = true, banner = false, init = false} then System.restart() else true;" |
|
97 |
fi |
|
17794 | 98 |
[ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
17759 | 99 |
fi |
100 |
||
101 |
||
102 |
## run it! |
|
103 |
||
104 |
POPLOG="$ML_HOME/poplog" |
|
105 |
check_mlhome_file "$POPLOG" |
|
106 |
||
17807
cc5dbc24e561
get rid of feeder -- at the cost of batch-only commit-at-exit;
wenzelm
parents:
17805
diff
changeset
|
107 |
INIT="$ISABELLE_TMP/init.ml" |
cc5dbc24e561
get rid of feeder -- at the cost of batch-only commit-at-exit;
wenzelm
parents:
17805
diff
changeset
|
108 |
echo 'pop11 |
cc5dbc24e561
get rid of feeder -- at the cost of batch-only commit-at-exit;
wenzelm
parents:
17805
diff
changeset
|
109 |
section $-ml; |
cc5dbc24e561
get rid of feeder -- at the cost of batch-only commit-at-exit;
wenzelm
parents:
17805
diff
changeset
|
110 |
false -> ml_quiet; |
cc5dbc24e561
get rid of feeder -- at the cost of batch-only commit-at-exit;
wenzelm
parents:
17805
diff
changeset
|
111 |
endsection; |
cc5dbc24e561
get rid of feeder -- at the cost of batch-only commit-at-exit;
wenzelm
parents:
17805
diff
changeset
|
112 |
ml' > "$INIT" |
17759 | 113 |
|
17807
cc5dbc24e561
get rid of feeder -- at the cost of batch-only commit-at-exit;
wenzelm
parents:
17805
diff
changeset
|
114 |
echo "$EXIT $USE $COMMIT $MLTEXT" >> "$INIT" |
cc5dbc24e561
get rid of feeder -- at the cost of batch-only commit-at-exit;
wenzelm
parents:
17805
diff
changeset
|
115 |
|
cc5dbc24e561
get rid of feeder -- at the cost of batch-only commit-at-exit;
wenzelm
parents:
17805
diff
changeset
|
116 |
if [ -n "$TERMINATE" ]; then |
cc5dbc24e561
get rid of feeder -- at the cost of batch-only commit-at-exit;
wenzelm
parents:
17805
diff
changeset
|
117 |
ML_OPTIONS="$ML_OPTIONS -nostdin" |
cc5dbc24e561
get rid of feeder -- at the cost of batch-only commit-at-exit;
wenzelm
parents:
17805
diff
changeset
|
118 |
echo "commit();" >> "$INIT" |
17759 | 119 |
fi |
120 |
||
17807
cc5dbc24e561
get rid of feeder -- at the cost of batch-only commit-at-exit;
wenzelm
parents:
17805
diff
changeset
|
121 |
"$POPLOG" pml "$DB" $ML_OPTIONS -load "$INIT" 2>&1 |
17759 | 122 |
RC="$?" |
123 |
||
17807
cc5dbc24e561
get rid of feeder -- at the cost of batch-only commit-at-exit;
wenzelm
parents:
17805
diff
changeset
|
124 |
rm -f "$INIT" |
17759 | 125 |
|
17820 | 126 |
if [ -n "$OUTFILE" ] && check_heap_file "$OUTFILE"; then |
17794 | 127 |
[ -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
17820 | 128 |
rm -f "$OUTFILE-" |
129 |
fi |
|
17759 | 130 |
|
131 |
exit "$RC" |