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());" |
|
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); |
|
70 [n ^n msg ^msg idstring ^idstring severity ^severity] ==> |
|
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' |
|
82 DB="" |
|
83 else |
|
84 EXIT="" |
|
85 USE="" |
|
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 |
|
92 ML_OPTIONS="$ML_OPTIONS -nort" |
|
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 |
|
98 [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
|
99 fi |
|
100 |
|
101 |
|
102 ## run it! |
|
103 |
|
104 POPLOG="$ML_HOME/poplog" |
|
105 check_mlhome_file "$POPLOG" |
|
106 |
|
107 INIT="$ISABELLE_TMP/init.ml" |
|
108 echo 'pop11 |
|
109 section $-ml; |
|
110 false -> ml_quiet; |
|
111 endsection; |
|
112 ml' > "$INIT" |
|
113 |
|
114 echo "$EXIT $USE $COMMIT $MLTEXT" >> "$INIT" |
|
115 |
|
116 if [ -n "$TERMINATE" ]; then |
|
117 ML_OPTIONS="$ML_OPTIONS -nostdin" |
|
118 echo "commit();" >> "$INIT" |
|
119 fi |
|
120 |
|
121 "$POPLOG" pml "$DB" $ML_OPTIONS -load "$INIT" 2>&1 |
|
122 RC="$?" |
|
123 |
|
124 rm -f "$INIT" |
|
125 |
|
126 if [ -n "$OUTFILE" ] && check_heap_file "$OUTFILE"; then |
|
127 [ -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
|
128 rm -f "$OUTFILE-" |
|
129 fi |
|
130 |
|
131 exit "$RC" |
|