author | wenzelm |
Wed, 16 Apr 2014 13:28:21 +0200 | |
changeset 56603 | 4f45570e532d |
parent 45778 | df6e210fb44c |
child 72004 | 913162a47d9f |
permissions | -rw-r--r-- |
39348 | 1 |
(* ========================================================================= *) |
2 |
(* PROCESSING COMMAND LINE OPTIONS *) |
|
39502 | 3 |
(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *) |
39348 | 4 |
(* ========================================================================= *) |
5 |
||
6 |
structure Options :> Options = |
|
7 |
struct |
|
8 |
||
9 |
open Useful; |
|
10 |
||
11 |
(* ------------------------------------------------------------------------- *) |
|
12 |
(* One command line option: names, arguments, description and a processor *) |
|
13 |
(* ------------------------------------------------------------------------- *) |
|
14 |
||
15 |
type proc = string * string list -> unit; |
|
16 |
||
17 |
type ('a,'x) mkProc = ('x -> proc) -> ('a -> 'x) -> proc; |
|
18 |
||
19 |
type opt = {switches : string list, arguments : string list, |
|
20 |
description : string, processor : proc}; |
|
21 |
||
22 |
(* ------------------------------------------------------------------------- *) |
|
23 |
(* Option processors may raise an OptionExit exception *) |
|
24 |
(* ------------------------------------------------------------------------- *) |
|
25 |
||
26 |
type optionExit = {message : string option, usage : bool, success : bool}; |
|
27 |
||
28 |
exception OptionExit of optionExit; |
|
29 |
||
30 |
(* ------------------------------------------------------------------------- *) |
|
31 |
(* Wrappers for option processors *) |
|
32 |
(* ------------------------------------------------------------------------- *) |
|
33 |
||
34 |
fun beginOpt f p (s : string, l : string list) : unit = f (p s) (s,l); |
|
35 |
||
36 |
fun endOpt () (_ : string, [] : string list) = () |
|
37 |
| endOpt _ (_, _ :: _) = raise Bug "endOpt"; |
|
38 |
||
39 |
fun stringOpt _ _ (_ : string, []) = raise Bug "stringOpt" |
|
40 |
| stringOpt f p (s, (h : string) :: t) : unit = f (p h) (s,t); |
|
41 |
||
42 |
local |
|
43 |
fun range NONE NONE = "Z" |
|
44 |
| range (SOME i) NONE = "{n IN Z | " ^ Int.toString i ^ " <= n}" |
|
45 |
| range NONE (SOME j) = "{n IN Z | n <= " ^ Int.toString j ^ "}" |
|
46 |
| range (SOME i) (SOME j) = |
|
47 |
"{n IN Z | " ^ Int.toString i ^ " <= n <= " ^ Int.toString j ^ "}"; |
|
48 |
fun oLeq (SOME x) (SOME y) = x <= y | oLeq _ _ = true; |
|
49 |
fun argToInt arg omin omax x = |
|
50 |
(case Int.fromString x of |
|
51 |
SOME i => |
|
52 |
if oLeq omin (SOME i) andalso oLeq (SOME i) omax then i else |
|
53 |
raise OptionExit |
|
54 |
{success = false, usage = false, message = |
|
55 |
SOME (arg ^ " option needs an integer argument in the range " |
|
56 |
^ range omin omax ^ " (not " ^ x ^ ")")} |
|
57 |
| NONE => |
|
58 |
raise OptionExit |
|
59 |
{success = false, usage = false, message = |
|
60 |
SOME (arg ^ " option needs an integer argument (not \"" ^ x ^ "\")")}) |
|
61 |
handle Overflow => |
|
62 |
raise OptionExit |
|
63 |
{success = false, usage = false, message = |
|
64 |
SOME (arg ^ " option suffered integer overflow on argument " ^ x)}; |
|
65 |
in |
|
66 |
fun intOpt _ _ _ (_,[]) = raise Bug "intOpt" |
|
67 |
| intOpt (omin,omax) f p (s:string, h :: (t : string list)) : unit = |
|
68 |
f (p (argToInt s omin omax h)) (s,t); |
|
69 |
end; |
|
70 |
||
71 |
local |
|
72 |
fun range NONE NONE = "R" |
|
73 |
| range (SOME i) NONE = "{n IN R | " ^ Real.toString i ^ " <= n}" |
|
74 |
| range NONE (SOME j) = "{n IN R | n <= " ^ Real.toString j ^ "}" |
|
75 |
| range (SOME i) (SOME j) = |
|
76 |
"{n IN R | " ^ Real.toString i ^ " <= n <= " ^ Real.toString j ^ "}"; |
|
77 |
fun oLeq (SOME (x:real)) (SOME y) = x <= y | oLeq _ _ = true; |
|
78 |
fun argToReal arg omin omax x = |
|
79 |
(case Real.fromString x of |
|
80 |
SOME i => |
|
81 |
if oLeq omin (SOME i) andalso oLeq (SOME i) omax then i else |
|
82 |
raise OptionExit |
|
83 |
{success = false, usage = false, message = |
|
84 |
SOME (arg ^ " option needs an real argument in the range " |
|
85 |
^ range omin omax ^ " (not " ^ x ^ ")")} |
|
86 |
| NONE => |
|
87 |
raise OptionExit |
|
88 |
{success = false, usage = false, message = |
|
89 |
SOME (arg ^ " option needs an real argument (not \"" ^ x ^ "\")")}) |
|
90 |
in |
|
91 |
fun realOpt _ _ _ (_,[]) = raise Bug "realOpt" |
|
92 |
| realOpt (omin,omax) f p (s:string, h :: (t : string list)) : unit = |
|
93 |
f (p (argToReal s omin omax h)) (s,t); |
|
94 |
end; |
|
95 |
||
96 |
fun enumOpt _ _ _ (_,[]) = raise Bug "enumOpt" |
|
97 |
| enumOpt (choices : string list) f p (s : string, h :: t) : unit = |
|
98 |
if mem h choices then f (p h) (s,t) else |
|
99 |
raise OptionExit |
|
100 |
{success = false, usage = false, |
|
101 |
message = SOME ("follow parameter " ^ s ^ " with one of {" ^ |
|
102 |
join "," choices ^ "}, not \"" ^ h ^ "\"")}; |
|
103 |
||
104 |
fun optionOpt _ _ _ (_,[]) = raise Bug "optionOpt" |
|
105 |
| optionOpt (x : string, p) f q (s : string, l as h :: t) : unit = |
|
106 |
if h = x then f (q NONE) (s,t) else p f (q o SOME) (s,l); |
|
107 |
||
108 |
(* ------------------------------------------------------------------------- *) |
|
109 |
(* Basic options useful for all programs *) |
|
110 |
(* ------------------------------------------------------------------------- *) |
|
111 |
||
112 |
val basicOptions : opt list = |
|
113 |
[{switches = ["--"], arguments = [], |
|
114 |
description = "no more options", |
|
115 |
processor = fn _ => raise Fail "basicOptions: --"}, |
|
116 |
{switches = ["-?","-h","--help"], arguments = [], |
|
117 |
description = "display option information and exit", |
|
118 |
processor = fn _ => raise OptionExit |
|
119 |
{message = SOME "displaying option information", |
|
120 |
usage = true, success = true}}, |
|
121 |
{switches = ["-v", "--version"], arguments = [], |
|
122 |
description = "display version information", |
|
123 |
processor = fn _ => raise Fail "basicOptions: -v, --version"}]; |
|
124 |
||
125 |
(* ------------------------------------------------------------------------- *) |
|
126 |
(* All the command line options of a program *) |
|
127 |
(* ------------------------------------------------------------------------- *) |
|
128 |
||
129 |
type allOptions = |
|
130 |
{name : string, version : string, header : string, |
|
131 |
footer : string, options : opt list}; |
|
132 |
||
133 |
(* ------------------------------------------------------------------------- *) |
|
134 |
(* Usage information *) |
|
135 |
(* ------------------------------------------------------------------------- *) |
|
136 |
||
137 |
fun versionInformation ({version, ...} : allOptions) = version; |
|
138 |
||
139 |
fun usageInformation ({name,version,header,footer,options} : allOptions) = |
|
140 |
let |
|
141 |
fun listOpts {switches = n, arguments = r, description = s, |
|
142 |
processor = _} = |
|
143 |
let |
|
144 |
fun indent (s, "" :: l) = indent (s ^ " ", l) | indent x = x |
|
145 |
val (res,n) = indent (" ",n) |
|
146 |
val res = res ^ join ", " n |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
147 |
val res = List.foldl (fn (x,y) => y ^ " " ^ x) res r |
39348 | 148 |
in |
149 |
[res ^ " ...", " " ^ s] |
|
150 |
end |
|
151 |
||
152 |
val alignment = |
|
153 |
[{leftAlign = true, padChar = #"."}, |
|
154 |
{leftAlign = true, padChar = #" "}] |
|
155 |
||
42102 | 156 |
val table = alignTable alignment (List.map listOpts options) |
39348 | 157 |
in |
158 |
header ^ join "\n" table ^ "\n" ^ footer |
|
159 |
end; |
|
160 |
||
161 |
(* ------------------------------------------------------------------------- *) |
|
162 |
(* Exit the program gracefully *) |
|
163 |
(* ------------------------------------------------------------------------- *) |
|
164 |
||
165 |
fun exit (allopts : allOptions) (optexit : optionExit) = |
|
166 |
let |
|
167 |
val {name, options, ...} = allopts |
|
168 |
val {message, usage, success} = optexit |
|
169 |
fun err s = TextIO.output (TextIO.stdErr, s) |
|
170 |
in |
|
171 |
case message of NONE => () | SOME m => err (name ^ ": " ^ m ^ "\n"); |
|
172 |
if usage then err (usageInformation allopts) else (); |
|
173 |
OS.Process.exit (if success then OS.Process.success else OS.Process.failure) |
|
174 |
end; |
|
175 |
||
176 |
fun succeed allopts = |
|
177 |
exit allopts {message = NONE, usage = false, success = true}; |
|
178 |
||
179 |
fun fail allopts mesg = |
|
180 |
exit allopts {message = SOME mesg, usage = false, success = false}; |
|
181 |
||
182 |
fun usage allopts mesg = |
|
183 |
exit allopts {message = SOME mesg, usage = true, success = false}; |
|
184 |
||
185 |
fun version allopts = |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
186 |
(TextIO.print (versionInformation allopts); |
39348 | 187 |
exit allopts {message = NONE, usage = false, success = true}); |
188 |
||
189 |
(* ------------------------------------------------------------------------- *) |
|
190 |
(* Process the command line options passed to the program *) |
|
191 |
(* ------------------------------------------------------------------------- *) |
|
192 |
||
193 |
fun processOptions (allopts : allOptions) = |
|
194 |
let |
|
195 |
fun findOption x = |
|
196 |
case List.find (fn {switches = n, ...} => mem x n) (#options allopts) of |
|
197 |
NONE => raise OptionExit |
|
198 |
{message = SOME ("unknown switch \"" ^ x ^ "\""), |
|
199 |
usage = true, success = false} |
|
200 |
| SOME {arguments = r, processor = f, ...} => (r,f) |
|
201 |
||
202 |
fun getArgs x r xs = |
|
203 |
let |
|
204 |
fun f 1 = "a following argument" |
|
205 |
| f m = Int.toString m ^ " following arguments" |
|
206 |
val m = length r |
|
207 |
val () = |
|
208 |
if m <= length xs then () else |
|
209 |
raise OptionExit |
|
210 |
{usage = false, success = false, message = SOME |
|
211 |
(x ^ " option needs " ^ f m ^ ": " ^ join " " r)} |
|
212 |
in |
|
213 |
divide xs m |
|
214 |
end |
|
215 |
||
216 |
fun process [] = ([], []) |
|
217 |
| process ("--" :: xs) = ([("--",[])], xs) |
|
218 |
| process ("-v" :: _) = version allopts |
|
219 |
| process ("--version" :: _) = version allopts |
|
220 |
| process (x :: xs) = |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
221 |
if x = "" orelse x = "-" orelse hd (String.explode x) <> #"-" then |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
222 |
([], x :: xs) |
39348 | 223 |
else |
224 |
let |
|
225 |
val (r,f) = findOption x |
|
226 |
val (ys,xs) = getArgs x r xs |
|
227 |
val () = f (x,ys) |
|
45778 | 228 |
|
229 |
val (xys,xs) = process xs |
|
39348 | 230 |
in |
45778 | 231 |
((x,ys) :: xys, xs) |
39348 | 232 |
end |
233 |
in |
|
234 |
fn l => |
|
45778 | 235 |
let |
236 |
val (a,b) = process l |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
237 |
|
45778 | 238 |
val a = List.foldl (fn ((x,xs),ys) => x :: xs @ ys) [] (List.rev a) |
239 |
in |
|
240 |
(a,b) |
|
241 |
end |
|
242 |
handle OptionExit x => exit allopts x |
|
39348 | 243 |
end; |
244 |
||
245 |
end |