equal
deleted
inserted
replaced
24 echo " Options are:" |
24 echo " Options are:" |
25 echo " -e MLTEXT pass MLTEXT to the ML session" |
25 echo " -e MLTEXT pass MLTEXT to the ML session" |
26 echo " -m MODE add print mode for output" |
26 echo " -m MODE add print mode for output" |
27 echo " -q non-interactive session" |
27 echo " -q non-interactive session" |
28 echo " -r open heap file read-only" |
28 echo " -r open heap file read-only" |
|
29 echo " -u pass 'use\"ROOT.ML\";' to the ML session" |
29 echo " -w reset write permissions on OUTPUT" |
30 echo " -w reset write permissions on OUTPUT" |
30 echo |
31 echo |
31 echo " INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps." |
32 echo " INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps." |
32 echo " These are either names to be searched in the Isabelle path, or actual" |
33 echo " These are either names to be searched in the Isabelle path, or actual" |
33 echo " file names (then containing at least one /)." |
34 echo " file names (then containing at least one /)." |
51 MODES="" |
52 MODES="" |
52 TERMINATE="" |
53 TERMINATE="" |
53 READONLY="" |
54 READONLY="" |
54 NOWRITE="" |
55 NOWRITE="" |
55 |
56 |
56 while getopts "e:m:qrw" OPT |
57 while getopts "e:m:qruw" OPT |
57 do |
58 do |
58 case "$OPT" in |
59 case "$OPT" in |
59 e) |
60 e) |
60 MLTEXT="$MLTEXT $OPTARG" |
61 MLTEXT="$MLTEXT $OPTARG" |
61 ;; |
62 ;; |
69 q) |
70 q) |
70 TERMINATE=true |
71 TERMINATE=true |
71 ;; |
72 ;; |
72 r) |
73 r) |
73 READONLY=true |
74 READONLY=true |
|
75 ;; |
|
76 u) |
|
77 MLTEXT="$MLTEXT use\"ROOT.ML\";" |
74 ;; |
78 ;; |
75 w) |
79 w) |
76 NOWRITE=true |
80 NOWRITE=true |
77 ;; |
81 ;; |
78 \?) |
82 \?) |